الفهرس Only 14 pages are availabe for public view
 |  | from | 146 |  |  |
| | | from | 146 | | |
Abstract
The Unified Modeling Language (UML) is an evolutionary step in the development of Object-Oriented analysis and design (OOA&D) methods that appeared in the late ’80s and early ’90s.
Unfortunately, the UML is a semi-formal language which lacks precisely defined constructs. Z language is a formal specification language based on first-order logic and set-theory.
Various attempts have been made to formally define the syntax of the UML notations and to represent its models in a formal notation. The purpose of these attempts is to allow UML models to be rigorously checked.
In this work, some recent UML formalization models were analyzed and a formal model for formalizing the syntax of (a sub-set of) the popular UML diagrams (Use Case diagram, Class diagram, and State Machine diagram) using Z specifications was proposed. Also, a Formal Model Checker CASE tool (FMC) that implements the proposed model was developed.
A case study is implemented using the proposed model and its tool. Finally, the proposed model was compared with other recent UML formal models. The comparison result shows that the proposed model and its implementing tool provide an efficient, easy to use, and user friendly tool for checking UML diagrams.