|Thesis abstract: |
The Unified Modeling Language (UML) has gone from a relatively basic descriptive tool (i.e., a tool that serves to document software systems) to a sophisticated prescriptive one, that is, a tool that can be used to specify, analyze and implement complex software systems. Despite some good results in this field some fundamental problems hamper the actual adoption of UML models for the analysis of the systems in a real production environment.
First, a unified and coherent semantics of UML must be developed. In the last ten years researchers have been trying to ascribe UML with many different semantics, but all these attempts have been partial. While there seems to be a general consensus on the semantics of some individual diagrams, the composite semantics of the different views is still an open problem. The wide spectrum of the notation and the heterogeneity and overlapping of the different modeling elements have played against its complete formalization; as a matter of fact most of the existing approaches only focus on a limited number of diagrams (oftentimes they only consider a single type) and neglect the interdependencies with the other views of the system. However multiple views mean better quality since different UML diagrams emphasize different aspects of the system.
Second, to spread the use of UML model verification at large scale the inherent complexity of formal methods in terms of usability must be decreased. For example in the classical approach to formal analysis the user is required to manually construct the formal model of the system in the language that is accepted by the verification tool. The construction of such model typically requires good knowledge of both the application domain and of the verification technology. In turn this activity requires mastering techniques like abstraction and refinement, model checking, or theorem proving that require a dedicated background. To avoid the manual construction of the formal model different tools have been developed to transform the UML models to a variety of formal notations, but the vast majority of them neglet the difficulty of hiding the underlying formal notations and tools to the UML user. Without a dedicated expertise in this field the user is not able neither to enact the verification phase, or to understand the verification results. Oftentimes a formal verification expert is required, making the UML formal verification a niche activity.
This thesis presents a significant step towards solving these problems by means of an advanced verification framework made of the following elements:
¿ A significant and consistent subset of UML, called MADES UML, where timed- related properties can be modeled carefully. MADES UML supports different behavioral views connected by means of a shared set of events.
¿ A formal semantics based on metric temporal logic which others the exibility and scalability we need to formalize a wide and rich notation like MADES UML. The formal semantics is used to feed a bounded model/satisfiability checker to allow users to verify their systems, even from the initial phases of the design.
¿ An advanced prototype verification tool called Corretto. Using Corretto UML engineers can exploit both a well-known modeling notation and advanced verification capabilities seamlessly. Properties are expressed using a high-level notation, and verification results produced by the underlying verification tool are linked back to the corresponding UML elements in the model.