| 摘要: |
| 统一建模语言UML已广泛应用于软件开发中,验证UML模型是否满足某些关键性质成为一个重要问题.提出了对UML Statecharts进行模型检验的方法.首先用扩展层次自动机结构化地表示UML Statecharts,然后给出其操作语义,通过寻找最大无冲突迁移集可以保证语义的正确性.对于具有无穷运行的系统,该操作语义可以映射到一个Büchi自动机.使用基于自动机理论的模型检验方法来验证UML Statecharts的线性时态逻辑性质,并给出方法验证由Statecharts和协同图建模的复杂多对象系统. |
| 关键词: UML(unified modeling language) Statecharts 模型检验 ω自动机 |
| DOI： |
| 分类号: |
| 基金项目:Supported by the National Natural Science Foundation of China under Grant Nos.69973051, 60233020, 90104007 (国家自然科学基金); the National High-Tech Research and Development Plan of China under Grant No.2001AA113202 (国家高技术研究发展计划(863)); the Huo Ying-Dong Education Foundation of China under Grant No.71064 (霍英东青年教师基金) |
|
| An Approach of Model Checking UML Statecharts |
|
DONG Wei,WANG Ji,QI Zhi-Chang
|
| Abstract: |
| UML (unified modeling language) has been widely used in software development. Verifying if a UML model meets the required properties has become a key issue. An approach of model checking UML Statecharts is given in this paper. At first, the UML Statecharts is structurally expressed by extended hierarchical automata. Then, the deduction rules of operational semantics are defined. The correctness of operational semantics can be ensured through finding the maximal non-conflict transition set. For the system with infinite runs, the operational semantics can be mapped to a Büchi automaton. Linear temporal logic properties of the system can be verified based on the automata theory of model checking. The method of verifying a complex multi-object system modeled by Statecharts and collaboration diagram is also presented in this paper. |
| Key words: UML (unified modeling language) Statecharts model checking ω-automata |
