ETH Zuerich - Homepage
Information Security

Lecture: System Development in Event-B

Master in Information Security

For more information about the Information Security Master Track visit:

251-1421-00 (2V2U)

Autumn Semester 2007

Prof. David Basin, Thai Son Hoang, Farhad Mehta

Course Description

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.


An interest in logic and discrete mathematics, and its possible applications in solving practical problems.


The main goal of this course is to provide students with knowledge of:


The course is organized around a number of examples. General topics are introduced together with these examples and are summarized at the end of each example presentation.


Course Material

The course material is available online for students of this course on a separate page. Please note that you will have to use your n-ethz username and password for access.


Time : Every Thursday (starting 27.09.2007), 10h00 - 12h00

Place : IFW B42

Slides and notes for the lectures can be found on the course material page.


Time: Every Thursday (starting 27.09.2007), 13h00-15h00

Place: IFW A36

Exercises and solutions for the lectures can be found on the course material page.


The project will involve modelling an elevator system and the correct construction of its controller using refinement and proof.
More details on the project ca be found on the course material page.


Wichtiger Hinweis:
Diese Website wird in älteren Versionen von Netscape ohne graphische Elemente dargestellt. Die Funktionalität der Website ist aber trotzdem gewährleistet. Wenn Sie diese Website regelmässig benutzen, empfehlen wir Ihnen, auf Ihrem Computer einen aktuellen Browser zu installieren. Weitere Informationen finden Sie auf
folgender Seite.

Important Note:
The content in this site is accessible to any browser or Internet device, however, some graphics will display correctly only in the newer versions of Netscape. To get the most out of our site we suggest you upgrade to a newer browser.
More information

© 2011 ETH Zurich | Imprint | Disclaimer | 22 October 2007