ETH Zuerich - Homepage
Information Security

System Development in Event-B

Master in Information Security

For more information about the Information Security Master Track visit:

251-1421-00 (2V2U)
Fall Semester 2008
D. Basin, J.-R. Abrial, T. S. Hoang, M. Schmalz


04.12.2008 Our advertisement for positions and interships
04.12.2008 The past exam is available on the course material page
03.12.2008 This week tutorial (04.12.2008) is a dedicated Q&A Session on the project.
20.11.2008 I published a first version of the Flash animation framework.
I will give a demo in the tutorial today.
19.11.2008 The course evaluation will take place on November 27 during the lecture.
13.11.2008 The tutorial today will be a Question & Answer session about Event-B and the Rodin Platform
06.11.2008 Do not use the new Rodin release (0.9.0)!
29.10.2008 Information: the deliverables "initial development" and "preliminary version of final model" are not graded.

Please come to Matthias' office to get some feedback.
22.10.2008 Concurrent Program Development Lecture: Updated version of the slides and the chapter of the book are available from the course material page.
20.10.2008 The next tutorial (23.10.) will be about the refinement strategy.
10.10.2008 The Animation Interface Description has been published.
09.10.2008 The Reference Card has been updated.
08.10.2008 You may also work on the project in groups of 3 persons.
However, we do not recommend it, because Rodin does not support team development at all.
01.10.2008 The Reference Card is available on the course material page
18.09.2008 I fixed some typos in Exercise Sheet 2, Assignment 1.
15.09.2008 For the tutorials, if you have your own laptop, it would be useful to bring it along.

Course Description

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.

We assume that you are interested in applying formal modeling and proofs to practical problems. It is an advantage if (but not necessary that) you have participated in the course "Formal Methods and Functional Programming".
The main objective of the course is to make you familiar with the following:

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.

Course Material


Time : Thursday (starting 18.09.2008), 10h00 - 12h00
Place : IFW B42


Time: Thursday (starting 18.09.2008), 16h00-18h00
Place: IFW A32.1


6 ECTS credits


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 | 18 September 2009