UML状态机的模型检验方法

• 作者: 王戟 董威 郑延平 齐治昌
• 来源期刊: 计算机工程与科学
• 学科: 工学
• 关键词: UML state chart 状态机 模型检验 计算树逻辑
• 年，卷（期）: 2001,（6）
• 所属期刊栏目: 算法研究
• 页码范围: 7-11
• 页数: 5页
• 分类号: TP311.5
• 字数: 5942字
• 语种: 中文
• DOI: 10.3969/j.issn.1007-130X.2001.06.003

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	王戟	国防科技大学计算机学院	41	880	14.0	29.0
3	齐治昌	国防科技大学计算机学院	42	432	12.0	19.0
4	董威	国防科技大学计算机学院	25	165	6.0	12.0
7	郑延平	国防科技大学计算机学院	1	30	1.0	1.0