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

摘要：

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

关键词：系统建模语言、模型检测、时序图、活动图

分类号：TP311(计算技术、计算机技术)

资助基金：国防科工局“十二五”重大基础科研项目c0420110005

在线出版日期：2015-10-13（万方平台首次上网日期，不代表论文的发表时间）

页数：共6页

页码：31-36