基于Spin的SysML活动图验证框架

摘要：

系统建模语言（systems modeling language，SysML）缺乏精确的形式化分析和验证手段，造成模型存在死锁、活锁等诸多问题，可以通过形式化验证方法来提高模型的正确性。然而，受制于传统的形式化方法需要复杂的公式推理，并且不易理解等方面局限性，大多数验证仅限专家使用并且很耗时。为了克服SysML模型中存在的问题，提出了一种针对SysML多层次活动图的分析验证框架。它可以根据已构建的模型，将多层次活动图分解转换为Spin的输入模型，并对相关子图进行重组和验证。实验表明，该方法可以有效识别多层次活动图，并准确实施转换，为模型验证的演化提供支持。

关键词：系统建模语言(SysML)、活动图、模型验证、Spin、Promela

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

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

页数：共12页

页码：836-847