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


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.