首页 | 本学科首页   官方微博 | 高级检索  
     

UML Statecharts的模型检验方法
引用本文:董威,王戟,齐治昌.UML Statecharts的模型检验方法[J].软件学报,2003,14(4):750-756.
作者姓名:董威  王戟  齐治昌
作者单位:国防科学技术大学,计算机学院,湖南,长沙,410073
基金项目: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 (霍英东青年教师基金)
摘    要:统一建模语言UML已广泛应用于软件开发中,验证UML模型是否满足某些关键性质成为一个重要问题.提出了对UML Statecharts进行模型检验的方法.首先用扩展层次自动机结构化地表示UML Statecharts,然后给出其操作语义,通过寻找最大无冲突迁移集可以保证语义的正确性.对于具有无穷运行的系统,该操作语义可以映射到一个Büchi自动机.使用基于自动机理论的模型检验方法来验证UML Statecharts的线性时态逻辑性质,并给出方法验证由Statecharts和协同图建模的复杂多对象系统.

关 键 词:UML(unified  modeling  language)  Statecharts  模型检验  ω自动机
收稿时间:2002/3/22 0:00:00
修稿时间:2002年3月22日

An Approach of Model Checking UML Statecharts
DONG Wei,WANG Ji and QI Zhi-Chang.An Approach of Model Checking UML Statecharts[J].Journal of Software,2003,14(4):750-756.
Authors:DONG Wei  WANG Ji and 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.
Keywords:UML (unified modeling language)  Statecharts  model checking  w-automata  
本文献已被 CNKI 维普 万方数据 等数据库收录!
点击此处可从《软件学报》浏览原始摘要信息
点击此处可从《软件学报》下载全文
设为首页 | 免责声明 | 关于勤云 | 加入收藏

Copyright©北京勤云科技发展有限公司  京ICP备09084417号