TITLE:
State Based Static and Dynamic Formal Analysis of UML State Diagrams
AUTHORS:
Fahad Alhumaidan
KEYWORDS:
UML; State Diagram; Formal Methods; Z Notation; Validation and Verification
JOURNAL NAME:
Journal of Software Engineering and Applications,
Vol.5 No.7,
June
15,
2012
ABSTRACT: Design and specification is a serious issue in software engineering because of the semantics involved in transforming the real world problems to computer software systems. Unified Modeling Language (UML) has been accepted as a de facto standard for design and specification of object oriented systems. Unfortunately, UML structures lack defining semantics of a system. Formal methods are proved powerful, particularly, at requirement specification and design level. For a moment, formal methods are not welcomed because of much use of mathematics in formal languages. Therefore, a linkage between UML and formal methods is required to overcome the above deficiencies. In this paper, a new approach is developed by integrating UML and Z specification focusing on state diagram considering both the syntax and semantics. It is believed that this new approach will be effective and useful both at academics and industrial level. The resultant formal models of the approach are analyzed and validated using Z/Eves tool.