Lecture: System Development in Event-B

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.

Prerequisites

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

Objectives

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 a number of examples. General topics are introduced together with these examples and are summarized at the end of each example presentation.

Grading

• 50% Project (Final Project Presentation: 13.12.2007)
• 50% Exam (20.12.2007)

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.

Lectures

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.

Tutorials

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.

Project

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.