Lecture 10: More on Timed Automata
In this second lecture on modelling and verification of real time systems
using the tool UPPAAL, Gerd Behrmann will first give a more precise account of the timed
automata based modelling language underlying UPPAAL, illustrated by the
train-gate example. The various verification options of UPPAAL will be
In the second half of the lecture, I will present the mini projects.
- [JPK] Chapter 4 until section 4.3.
- [UPPAAL] and [UPPAAL2k]
- [JPK] Reread Chaper 1 (optional)
- Joost-Pieter Katoen: Concepts, Algorithms, and Tools for Model
Checking. (Lecture Notes)
- Larsen, Pettersson, Yi: UPPAAL
in a Nutshell In Journal for Software Tools for Technology Transfer,
vol 1, 1997./dd>
- Alexandre David: UPPAAL2K: Small Tutorial. PostScript version is here.
The exercises will be added later.