一种UML2．0模型动态特性的一致性验证方法

近年来，UML已经被广泛应用于软件的分析和设计，然而，由于软件系统的复杂性，在UML模型中，难免会引入不同图表间特别是动态视图之间的不一致性。提出了一种用于验证UML2．0模型状态图和顺序图一致性的方法。首先，用XYZ／E来形式化描述状态图并将其转化为Promela输入语言；然后，用LTL来表示顺序图间的相互作用；最后利用模型检测工具Spin通过检查Promela描述的状态图是否满足LTL公式来达到检测模型一致性的目的。

An approach to check the consistency between the UML2.0 dynamic diagrams

Nowadays, UML has been applied to analysis and design ot soitware wlaety, however,modeling the system by different UML diagrams certainly will introduce inconsistency between UMLdiagrams. A method model checking the consistency between State diagram and Sequence diagram inUML2.0 is given out. First, it uses XYX/E to express the State diagram and translate it to Prometalanguage. Second, it uses LTL to describe the interaction fragments between sequence diagrams inUML2.0. Finally, the consistency between the two diagrams is verified by checking whether the LTLformula is the property of the property of the model described by Promela.