基于状态约简的顺序图和状态图一致性检测

摘要：

为了解决系统设计过程中模型一致性问题，提出了一种对UML顺序图和状态图的语义一致性检测方法。该方法对顺序图和状态图一致性进行符号化描述，为一致性检测提供理论基础；提出状态约简规则和状态约简算法，能够减少冗余状态和迁移，证明了状态约简不影响一致性检测；提出改进的UML模型到PROMELA的转换方法并使用SPIN进行验证。实验表明上述方法能够有效地检测顺序图和状态图的一致性，在验证过程中减少冗余状态和迁移，转换后的代码结构简单、执行效率高。

关键词：统一建模语言、顺序图、状态图、状态约简、模型一致性验证

所属期刊栏目：31

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

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

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

页数：共4页

页码：1452-1455