VVZ API is not affiliated with ETH Zurich. Data might be outdated or incorrect. Please view the official ETHZ Vorlesungsverzeichnis for binding information.
Practical System Modelling using Discrete Mathematics
Last Updated: 2026-02-05 14:55:12
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 examples explaining how to write and prove formal models of discrete systems using abstraction and refinement.
Content
In a first part, this course will survey the mathematical background under which discrete system modeling can be envisaged: - A refresher on system development methods and their practical applications in Industry - Why modeling? - Why distinguishing models of systems and models of programs from systems and programs themselves? - A refresher on predicate logic and deductive proofs (with examples) - A refresher on set theory (with examples) - Proof tools presentation (with demonstrations) - A development framework for discrete transition model construction: - Some simple linguistic structures for describing discrete transition models - Some simple linguistic structures for describing and developing discrete transition models - Some semantics for the previous linguistic structures (proof obligations) In the second (and far more important) part, a large number of applied developments will be presented as an illustration of this approach - Development of sequential programs (Simple array algorithms, More elaborate graph algorithms, Garbage collector algorithm - Development of distributed programs (Simple file transmission protocol, Process synchronization on a tree network, Distributed mutual exlusion, Routing algorithm for a mobile agent, Leader election in a network) - Development of concurrent programs (Various non-blocking concurrent queue algorithms - Development of hardware systems (A complex traffic light system) - Development of complete systems (equipment and controller) (A building control system, A mechanical press controller) - System failure analysis (A simple chemical plant)
General Information
- Language
- English
- Frequency
- Yearly recurring
Examination
- Type
- session examination
- Mode
- oral 30 minutes
Course Components
| Type | Title | Time & Place | Hours |
|---|---|---|---|
| lecture | Practical System Modelling using Discrete Mathematics |
|
2 h weekly |
| exercise | Practical System Modelling using Discrete Mathematics |
|
1 h weekly |