Title :
An approach to check the consistency between the UML 2.0 dynamic diagrams
Author :
Gongzheng, Lu ; Guangquan, Zhang
Author_Institution :
Sch. of Comput. Eng. & Sci., Shanghai Univ., Shanghai, China
Abstract :
Nowadays, UML is applied to modeling in the analysis and design of software systems widely. However, modeling the system by different UML diagrams certainly will introduce inconsistency between UML diagrams. A method model checking the consistency between Statechart Diagram and Sequence Diagram in UML 2.0 is given. Firstly, XYZ/E can express the mechanism of state transformation and formal semantics, so it can characterize Statechart Diagram directly. Secondly, XYZ/E and Promela are similar in many aspects; an algorithm transforms the XYZ/E code into promela is proposed. In the follow, the rules which describe how to use LTL to express the interaction fragments in UML2.0 sequence diagram are given. Finally, the consistency between the two diagrams is verified by checking whether the LTL formula is the property of the model described by Promela.
Keywords :
Unified Modeling Language; formal languages; formal verification; programming language semantics; Promela; UML 2.0 dynamic diagram; XYZ/E; formal semantic; model checking; sequence diagram; software system design; software systems analysis; state transformation; statechart diagram; Automata; Computational modeling; Object oriented modeling; Optimized production technology; Semantics; Unified modeling language; Sequence diagram; Statechart diagram; UML 2.0; consistency; model checking;
Conference_Titel :
Computer Science and Education (ICCSE), 2010 5th International Conference on
Conference_Location :
Hefei
Print_ISBN :
978-1-4244-6002-1
DOI :
10.1109/ICCSE.2010.5593823
