Approach to Check the Consistency between the UML2.0 Dynamic Diagrams
Nowadays,UML is applied to modeling in the analysis and design of software system widely.However,because of the complexity of the software system,in the UML model,the inevitable will introduce different chart especially inconsistencies between the dynamic view.This paper proposes a method to verify UML2.0 model consistency of state diagram and sequence diagram.First,XYZ/E can express the mechanism of state conversion and formal semantics,so it can characterize State Diagram directly.Second,XYZ/E and Promela are similar in many aspects,an algorithm transforms the XYZ/E code into Promela is proposed.Rules are designed which describe how to use the LTL to express the interaction fragments in UML2.0 Sequence diagram are given in the paper.Finally using the model checking tool Spin,to examine the Promela described system specifications,to test whether the system meets the LTL formulas,to achieve the goal of detection model consistency.
UML2.0 StateDiagram SequenceDiagram Consistency Formal Verification Model Checking
Quanzhu Yao Xiaodan Cui
Computer Technology, Graduate School of Xian University of Technology Xian, China
国际会议
秦皇岛
英文
1115-1119
2015-09-18（万方平台首次上网日期，不代表论文的发表时间）