Learned lessons
  • 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.