UML状态机的模型检验方法

Model Checking of UML State Machines

模型检验是一种确保设计规范正确性的形式化自动验证技术 ,本文提出了对 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).