VVZ API is not affiliated with ETH Zurich. Data might be outdated or incorrect. Please view the official ETHZ Vorlesungsverzeichnis for binding information.
Model Checking of Reactive Systems
Last Updated: 2026-02-05 15:24:38
Abstract
Reactive Systems are software systems that undergo a continuous stimuli-response interaction with their environment. The course will introduce into explicit state model checking for reactive systems, an algorithmic, automated technique for the correctness analysis of such systems. We will illustrate the algorithmic foundations of this technique, present the SPIN tool, and address advanced topics.
Content
Reactive Systems are software systems that undergo a continuous stimuli-response interaction with their environment. In practice, they often occur as embedded systems, such as in telecommunications or in automotive systems. The course will introduce into explicit state model checking for reactive systems, an algorithmic, automated technique for the correctness analysis of such systems. We will illustrate the algorithmic foundations of this technique, present the SPIN tool, and address advanced topics. The accompanying project will address the modeling and analysis of a VoIP protocol.
General Information
- Language
- English
- Levels
- BSC , MSC
Examination
- Type
- end-of-semester examination
Course Components
| Type | Title | Time & Place | Hours |
|---|---|---|---|
| lecture | Model Checking of Reactive Systems |
|
2 h weekly |
| exercise | Model Checking of Reactive Systems |
|
2 h weekly |