Formal Methods and Unified Modeling Language (UML)
Nov 25-27, 2015
Dictated by Alexander Knapp at INCO - FING UY
The Unified Modeling Language (UML) provides a wealth of sub-languages for specifying and documenting software systems, but only offers a rather weak linkage between these sub-languages through a common abstract syntax and an informal semantical description. In order to open up the perspective of integrating the UML also in the development of safety-critical systems, we propose a heterogeneous modelling approach that represents the semantics of the several sub-languages in their own, appropriate semantic domain and provides flexible links between the different formalisms. The approach is based on the algebraic theory of institutions for describing logical theories and institution (co-)morphisms for expressing relationships. We illustrate the approach by some examples for UML class diagrams, OCL, interactions, and state machines.
- Part I: UML Different elements of the family of UML languages are discussed: class diagrams, state machines and interactions, as well as the Object Constraint Language (OCL). using the translation tool Hugo/RT models for verification of design properties based on UML study using SPIN and UPPAAL model checkers.
- Part II: Model checking Two basic approaches are presented: symbolic model checking based on Binary Decision Diagrams (BDDs) for Computation Tree Logic (CTL), and cheking model based on Linear Temporal Logic automata (LTL) as is done in SPIN. It also presents temporal model checking using timed automata as is done in UPPAAL.
- Part III: UML as a heterogeneous language It provides a brief introduction to the theory of institutions for the representation of the semantics of UML models and institutions are discussed for various UML diagrams: class diagrams, state machines and OCL.
