一种UML状态图模型检测方法

• 作者: 刘刚 吕天阳 张涛 黄宏涛 黄少滨
• 来源期刊: 哈尔滨工程大学学报
• 学科: 工学
• 关键词: 模型检测 迁移系统 操作语义 UML 状态图
• 年，卷（期）: 2011,（8）
• 页码范围: 1035-1039
• 分类号: TP311.5
• 字数: 5231字
• 语种: 中文
• DOI: 10.3969/j.issn.1006-7043.2011.08.013

摘要

为在开发过程早期发现系统设计的各种错误与不一致,提出一种UML状态图模型检测方法,用于验证设计模型与需求规约间的一致性.该方法通过元组定义UML状态图的主要元素,给出状态图的中间表示形式SC.基于SC上定义的操作语义,该方法将状态图转换为具有KRIPKE语义结构的状态迁移系统,并将系统需满足的性质表示为线性时序逻辑公式,用模型检测技术验证状态迁移系统对线性时序逻辑公式的满足性.该方法可以转换更多的状态图元素,缩减状态图迁移系统的状态空间及提高模型检测效率.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	刘刚	哈尔滨工程大学计算机科学与技术学院	82	575	12.0	20.0
2	张涛	哈尔滨工程大学计算机科学与技术学院	85	1098	19.0	31.0
3	黄少滨	哈尔滨工程大学计算机科学与技术学院	55	319	10.0	15.0
4	吕天阳	哈尔滨工程大学计算机科学与技术学院	23	103	6.0	9.0
5	黄宏涛	哈尔滨工程大学计算机科学与技术学院	5	28	3.0	5.0