基于Spin的SysML时序图与活动图一致性检测

• 作者: 孙博 胡良文 马金晶
• 来源期刊: 计算机技术与发展
• 学科: 工学
• 关键词: 系统建模语言 模型检测 时序图 活动图
• 年，卷（期）: 2015,（9）
• 所属期刊栏目: 智能、算法、系统工程
• 页码范围: 31-36
• 页数: 6页
• 分类号: TP311
• 字数: 5177字
• 语种: 中文
• DOI: 10.3969/j.issn.1673-629X.2015.09.007

摘要

系统建模语言( Systems Modeling Language,SysML)对复杂系统多视角建模时,容易造成多视图描述语义冲突、矛盾等不一致问题,可以通过形式化验证方法,来提高模型的一致性。然而,受制于传统的形式化检测方法不能做到完全自动化,并且需要繁杂的公式推理,导致多数验证方法仅限少数专家使用并且非常耗时。为了解决SysML时序图与活动图模型之间存在的一致性问题,提出一种自动转换验证框架。首先基于已构建的模型和转换规则,将时序图进行分解转换为活动图,然后分别映射为Spin的输入模型,并对模型的交互一致性执行自动化验证。实验结果表明,该方法可以有效识别和转换时序图,并能准确地向Promela实施映射和验证,为一致性验证的演化提供支持。

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	孙博	南京航空航天大学计算机科学与技术学院	7	150	4.0	7.0
2	马金晶	南京航空航天大学计算机科学与技术学院	8	31	4.0	5.0
3	胡良文	南京航空航天大学计算机科学与技术学院	2	10	2.0	2.0