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:14:30
Abstract
This course introduces ways of specifying, designing, and implementing computerized systems so that the outcome will be correct by construction. It is essentially made of a large number of examplesexplaining how to write and prove formal models of discrete systemsusing abstraction and refinement.
Objective
The main goal of this course is to provide students with knowledge of: - Modeling of discrete transition systems - Mathematical techniques to be used to construct and validate such models - Different areas where such modeling techniques can be used
Content
The course is organized around examples. General topics are introduced together with the examples and summarized at the end of each example presentation. 1. Introduction: Modeling and requirements. 2. Example: Managing cars on a bridge. 3. Example: File transfer protocol. 4. Example: Leader election on a ring-shaped network. 5. Example: Process synchronization on a tree-shaped network. 6. Example: Mobile object routing protocol. 7. Example: The IEEE-1394 leader election protocol. 8. Refresher in First Order Predicate Calculus and Natural Deduction
Resources
Lecture Notes
Complete course material will be distributed to the students in theform of written lecture notes accompanying each lecture, slidesaccompanying each lecture. A modeling tool (Rodin) will be usedin the labs.
General Information
- Language
- English
- Levels
- BSC , DS , MSC
- 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 |