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