摘要：

模型检验是一种确保设计规范正确性的形式化自动验证技术，本文提出了对UML状态机进行模型检验的方法。文中首先对UML状态机的语法和语义进行描述，然后基于语义中的 RTC步给出生状态机全局可达状态迁移图的方法，方法的核心是在当前格局下根据使能条件确定所有的最大无冲突迁移集。文章最后给出算法以验证UML状态机是否满足用计算树逻辑（CTL）公式表示的性质。

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