web analytics
Contact me 
Orange D inside a circle
Educational details
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.