The main theme of this course is formal modeling and verification of real time systems.  It will introduce the theories, algorithms and data structures behind UPPAAL, an international leading tool for verification of timed systems,  and TIMES, a tool for schedulability analysis of timed systems and code generation.

The course will cover models for finite state systems and introduction to temporal logics and model checking. The focus will be put on the theory of timed automata covering the syntax, semantics, verification problems, (un)decidability results, and techniques for symbolic reachability analysis which is the core of the UPPAAL tool. The course will provide also a tutorial on UPPAAL and TIMES: the modeling and specification languages, and the construction of their verification engine.