FORMAL DEVELOPMENT OF OPEN DISTRIBUTED SYSTEMS: INTEGRATION OF UML AND PVS
Demissie B. Aredo · 2004
In this thesis, a research work conducted on formalization of the Unified Modeling Language (UML) notations is reported. Formal semantic definitions for UML modeling constructs are provided by systematically transforming them into suitable and well-defined entities in the specification language of the Prototype Verification System (PVS). As UML is an industry standard modeling language consisting of several aspects of object-oriented modeling techniques, it is not feasible to cover all semantic aspects of the UML notations. Static structural models (class diagrams), and dynamic behavioral models (sequence and statecharts diagrams) are the main focus of the thesis. A strategy for deriving semantic models directly from UML graphical models, and a framework for integrating the UML modeling techniques with formal analysis techniques of the PVS environment is proposed. Transformation of UML graphical models into PVS specifications results in semantic models that are amenable to rigorous analysis, thereby overcoming limitations inherent in the semi-formal UML notations. This paves a way for developing formal techniques that support rigorous development of distributed systems through transformation and enhancement of OO modeling techniques. Integrating semi-formal graphical modeling techniques with a mathematically based development method(s) results in a development framework that supports rigorous model analysis, while useful features of the graphical modeling techniques are preserved. Automation of the derivation of formal specifications from graphical UML models based on the proposed semantics is vital as model analysis usually involves manipulation of large volume of information. In this regard, we have developed a prototype of a CASE tool that integrates the general-purpose PVS tool set with a UML CASE tool. The tool supports formal development of distributed systems from requirement capture to code generation and allows developers to deal with the graphical models they have developed while the rigorous analysis is performed at the back-end. This work contributes to the ongoing effort to provide formal semantics for the UML notations, with the aim of clarifying and disambiguating the language as well as supporting development of semantically-based CASE tools. Moreover, it allows exploitation of the synergy between formal methods (FM) and semi-formal modeling languages, which in turn improves the use of FMs in industrial settings.