摘要
为了解决系统设计过程中模型一致性问题,提出了一种对UML顺序图和状态图的语义一致性检测方法。该方法对顺序图和状态图一致性进行符号化描述,为一致性检测提供理论基础;提出状态约简规则和状态约简算法,能够减少冗余状态和迁移,证明了状态约简不影响一致性检测;提出改进的UML模型到PROMELA的转换方法并使用SPIN进行验证。实验表明上述方法能够有效地检测顺序图和状态图的一致性,在验证过程中减少冗余状态和迁移,转换后的代码结构简单、执行效率高。
The proposed a new method for model checking the consistency of the semantics of sequence diagram and state ma- chine in the process of design. The method formalized the description of the consistency of sequence and state machine to es- tablish the theoretical basis of model checking. This paper presented some state reduction rules and a state reduction algorithm which proved not affect the consistency to decrease the redundancy of states and transitions. Moreover, it translated the UML model to PROMELA which was the specification language of the model checker SPIN which was used to verify the consistency. Experiments indicate that, consistency of sequence diagram and state machine diagram is effectively verified, states and transi- tions are decreased during the model checking process, and the codes generated are simpler and more effective.
出处
《计算机应用研究》
CSCD
北大核心
2014年第5期1452-1455,共4页
Application Research of Computers
基金
国防科工局"十二五"重大基础科研资助项目(c0420110005)
