A metamodel-based approach to integrate object-oriented graphical and formal specification techniques

The Unified Modeling Language (UML) is a standard object-oriented modeling language that can be used to visualize, specify, construct and document the artifacts of a software system. Considering the important role of UML as a standard modeling language, it is essential that the language should have a well-defined syntax and semantics for its notation and modeling concepts, and allow rigorous analysis of its models. Current UML, however, has several drawbacks in the following areas. The UML metamodel serves as a conceptual model of UML defining the abstract syntax and semantics of the modeling concepts provided by UML. In the metamodel, the definition of the modeling constructs is described from three distinct views: abstract syntax in UML class diagrams, static semantics in Object Constraint Language (OCL), finally dynamic semantics mainly in English. As a result of this approach, the abstract syntax, static semantics, and dynamic semantics are defined primarily in distinct structures and representations with many redundancies and inconsistencies. Therefore, when a modeling construct is enhanced, each of these three structures also must be extended. This lack of modularity and extensibility in the semantic presentation of the UML results in the UML metamodel being not-well structured. The other significant problem of the current UML metamodel is a lack of precision for defining the semantics of modeling constructs. For instance, none of the three meta-languages used to define the UML metamodel has a precise, standardized and widely accepted syntactic and semantic basis. Finally, current UML does not provide a systematic mechanism to analyze its models. To overcome these identified problems of UML, this thesis develops a two-level formalization approach. For the language-level formalization, this thesis adopts an objectoriented approach to encapsulate the abstract syntax and the static and dynamic semantics of each distinct modeling construct into a single Object-Z class. This results not only in improved precision but also modularity and extensibility of the UML metamodel presentation. For the specification-level formalization, this thesis provides a metamodel-based formal mapping between UML and Object-Z, which is precise, consistent and complete. As a consequence, this thesis outlines a rigorous basis for checking consistency and completeness of UML models with the metamodel and for proving properties captured in the UML models using reasoning techniques provided for Object-Z.