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

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

作　　者：雷博[1] 裴磐洁 

机构地区：[1]92493部队88分队

出　　处：《信息技术》2014年第8期183-186,共4页Information Technology

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

关 键 词：UML2 0 状态图 顺序图 一致性 模型检测 

分 类 号：TP311.52[自动化与计算机技术—计算机软件与理论]