基于模型检测的UML状态图和顺序图一致性检测

用户可使用UML从不同角度对系统进行建模,但不同视图间存在信息冗余,会导致视图不一致的问题。文中提出形式化与可视化UML互补建模的方法,探讨用模型检测验证UML模型中的状态图和顺序图的一致性问题。针对具有复合片段的顺序图提出分析方法,将复杂层次结构的状态图转换为有限状态机,再用模型检测工具NuSMV对建立的模型进行验证。最后通过实例对此转换方法进行验证,实验结果表明了此方法的有效性。

Consistency Check Between UML State Chart and Sequence Chart Based on Model Checking

UML can be used to accomplish the system modeling from different views.There may be some redundancy in different views,so that the views may be inconsistent.This paper proposes modeling methods based on the formalization method and the UML.It focuses mainly on using the model checking to check the consistency between the UML statechart and the sequence chart.The method to deal with the composite sequence chart is proposed and the hierarchy structure of the statechart is translated into the finite automata machine.Then the NuSMV is used to verify them.Experimental results show the effectiveness of the converting methods.