System Development in Event-B

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

Announcements

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:

• applying logics and discrete transition systems to real world problems,
• the Rodin Platform,
• refinement.

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

• Slides, exercise sheets, solution sheets, ... can be found on the course material page.
• Informations about the Rodin Platform can be found here.

Lectures

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

Tutorials

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

Grading

6 ECTS credits

• 50% Project (Final Presentation on 11.12.2008)
• 50% Exam (18.12.2008 from 10h00-12h00)