Title :
Specification and Verification of UML2.0 Sequence Diagrams Using Event Deterministic Finite Automata
Author :
Chen, Zhang ; Zhenhua, Duan
Author_Institution :
Inst. of Comput. Theor. & Technol., Xidian Univ., Xi´´an, China
Abstract :
A key challenge in software development process is to detect errors in earlier phases of the software life cycle. For this purpose, the verification of UML diagrams plays an important role in detecting flaws at the analysis and design phase. To enhance the correctness of one of the most popular UML diagrams: sequence diagram (SD), model checking propositional projection temporal logic (PPTL) is adopted. With this method, event deterministic finite automata are used to describe the formal models of an SD, and PPTL is selected to describe a desired property. Experimental result shows that the proposed approach is useful for verifying the properties of SDs and hence for improving the correctness of SDs.
Keywords :
Unified Modeling Language; deterministic automata; finite automata; formal specification; formal verification; temporal logic; UML diagram specification; UML diagram verification; UML2.0 sequence diagram; event deterministic finite automata; model checking propositional projection temporal logic; sequence diagram; software development process; software life cycle; Automata; Least squares approximation; Object oriented modeling; Optimized production technology; Semantics; Software; Unified modeling language; ETDFA; Model checking; PPTL; UML2.0 sequence diagrams;
Conference_Titel :
Secure Software Integration & Reliability Improvement Companion (SSIRI-C), 2011 5th International Conference on
Conference_Location :
Jeju Island
Print_ISBN :
978-1-4577-0781-0
Electronic_ISBN :
978-0-7695-4454-0
DOI :
10.1109/SSIRI-C.2011.17
