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 described.

In the second half of the lecture, I will present the mini projects.

Reading Material

• [JPK] Chapter 4 until section 4.3.
• [UPPAAL] and [UPPAAL2k]
• [JPK] Reread Chaper 1 (optional)

where

[JPK]

Joost-Pieter Katoen: Concepts, Algorithms, and Tools for Model Checking. (Lecture Notes)

[UPPAAL]

Larsen, Pettersson, Yi: UPPAAL in a Nutshell In Journal for Software Tools for Technology Transfer, vol 1, 1997./dd>

[UPPAAL2k]

Alexandre David: UPPAAL2K: Small Tutorial. PostScript version is here.

Exercises

The exercises will be added later.