Lecture 8: Reactive and Real-time System Modelling
(Nov. 5th afternoon)
(Make sure you have downloaded Uppaal to your computer before the
lecture day!)
Topics:
-
Introduction to Reactive Real-time Systems and Model-Based Development
-
-
High-level FSM languages
-
Modelling untimed systems using Uppaal
-
Timed Automata (TA)
-
Modelling timed systems using Uppaal
-
Verification using Uppaal
Slides:
Lecture 8: An Introduction to Reactive
and Real-time System Modelling (pdf)
Exercises:
Lecture 8: An Introduction to Reactive
and Real-time System Modelling (pdf) (solutions)
Literature:
on
- Gerard
J. Holzmann. Design and Validation of Computer Protocols, Chapter
8 (skip sections 8.6 and 8.10)
on
Timed Automata (TA):
-
Gerd Behrmann, Alexandre David, Kim G. Larsen. A tutorial on Uppaal. (read sections
1, 2.1, 2.2, 3.1, 4, 7)
Modelling
tools:
- for
FSM: The Finite State Machine
Explorer
- for TA: Uppaal