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

fYear

2011

fDate

27-29 June 2011

Firstpage

41

Lastpage

46

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;

fLanguage

English

Publisher

ieee

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

Type

conf

DOI

10.1109/SSIRI-C.2011.17

Filename

6004501