VVZ API is not affiliated with ETH Zurich. Data might be outdated or incorrect. Please view the official ETHZ Vorlesungsverzeichnis for binding information.
System Development in Event-B
Last Updated: 2026-02-05 15:24:47
Abstract
The participants of this course learn ways of specifying, designing, and implementing computerized systems so that the outcome is correct by construction. We introduce Event-B, a language for modeling (infinite state) discrete transition systems and proving them correct. An important principle is refinement.
Objective
The main objective of the course is to make you familiar with the following: * applying logics and discrete transition systems to real world problems, * the Rodin Platform, * refinement.
Content
The participants of this course learn ways of specifying, designing, and implementing computerized systems so that the outcome is correct by construction. We introduce Event-B, a language for modeling (infinite state) discrete transition systems and proving them correct. An important principle is refinement: it allows to leave out complicated details in the beginning and to introduce them later in a step-by-step manner. Properties that have been proved in the beginning also hold, in a sense, after introducing new details. The Rodin Platform allows to write Event-B models, and generates proof obligations, i.e., conditions that are sufficient for correctness of the model. The platform also assists the user in proving these proof obligations. In the lecture we will mainly discuss examples. In the tutorials we give you an introduction to the Rodin Platform and then mainly assist you with the semester project: your own Rodin development.
Resources
Lecture Notes
Complete course material will be distributed to the students in the form of written lecture notes accompanying each lecture, slides accompanying each lecture. A modeling tool (Rodin) will be used in the labs.
General Information
- Language
- English
- Levels
- BSC , DS , MSC , WBZ
- Frequency
- Yearly recurring
Examination
- Type
- end-of-semester examination
Course Components
| Type | Title | Time & Place | Hours |
|---|---|---|---|
| lecture | System Development in Event-B |
|
2 h weekly |
| exercise | System Development in Event-B |
|
2 h weekly |