UML状态机的模型检验方法  

Model Checking of UML State Machines

作　　者：董威[1] 王戟[1,2] 郑延平[1] 齐治昌[1] 

机构地区：[1]国防科技大学计算机学院,湖南长沙410073 [2]武汉通信指挥学院,湖北武汉430001

出　　处：《计算机工程与科学》2001年第6期7-11,共5页Computer Engineering & Science

基　　金：国家自然科学基金项目 (69973 0 5 1);国家863计划资助项目 (863 -3 0 6-ZT0 6-0 4-1);武汉大学软件工程国家重点实验室访问学者基金;霍英东青年教师基金资助项目(710 64 )

摘　　要：模型检验是一种确保设计规范正确性的形式化自动验证技术 ,本文提出了对 UML状态机进行模型检验的方法。文中首先对 UML状态机的语法和语义进行描述 ,然后基于语义中的 RTC步给出生成状态机全局可达状态迁移图的方法 ,方法的核心是在当前格局下根据使能条件确定所有的最大无冲突迁移集。文章最后给出算法以验证 UML状态机是否满足用计算树逻辑 ( CTL)Model checking is a very important method of automatic formal verification to ensure the correctness of design specifications.We give a method for the model checking of UML state machines in this paper.First,we describe the syntax and semantics of UML state machines.Based on the RTC step in the semantics,we give a method to construct the global transition graph of reachable states.The core of the method is to determine all maximal non conflict transition sets.Finally,we give algorithms to verify if the UML state machine satisfies the properties described in compute tree logic(CTL).

关 键 词：UML 状态机 模型检验 计算树逻辑 软件质量 软件工程 

分 类 号：TP311.5[自动化与计算机技术—计算机软件与理论]