At the end of the lecture period

Exercises and written or oral exam

Introduction to formal methods of the specification and verification of time sensitive systems and their combinations.

Professional competence
The students:

• Learn about different models of time and real-time properties
• Specify and verify real-time systems
• Model real-time systems using Timed Automata and PLC-Automata
• Apply the model checker UPPAAL for the verification of real-time properties
• Specify real-time systems using the Duration Calculus
• Learn about decidability and undecidability results for real-time systems

Methodological competence
The students:

• Recognize logic and automata as adequate forms for describing real-time systems

Social competence
The students:

• Work together in small groups to solve problems
• Present their solutions to groups of other students 

 
Self-competence
The students:

• Learn persistence in pursuing difficult tasks
• Learn precision in specifying problems