10.3778/j.issn.1673-9418.1401023
基于Spin的SysML活动图验证框架
系统建模语言(systems modeling language,SysML)缺乏精确的形式化分析和验证手段,造成模型存在死锁、活锁等诸多问题,可以通过形式化验证方法来提高模型的正确性。然而,受制于传统的形式化方法需要复杂的公式推理,并且不易理解等方面局限性,大多数验证仅限专家使用并且很耗时。为了克服SysML模型中存在的问题,提出了一种针对SysML多层次活动图的分析验证框架。它可以根据已构建的模型,将多层次活动图分解转换为Spin的输入模型,并对相关子图进行重组和验证。实验表明,该方法可以有效识别多层次活动图,并准确实施转换,为模型验证的演化提供支持。
系统建模语言(SysML)、活动图、模型验证、Spin、Promela
TP311(计算技术、计算机技术)
2014-07-23(万方平台首次上网日期,不代表论文的发表时间)
共12页
836-847