Provably Correct Software, Spring -09

Below this headline, you'll find important updated information about the course. Make it a habit to check the News regularly!

• (2009-05-19) There is a new web page about the string machine.
• (2009-04-29) There is a new web page about bugs and restrictions in Atelier B.
• (2009-04-01) The Formal Methods Wiki added to the links section of this web page. This wiki replaces the Formal Methods Virtual Library.
• (2009-03-27) There is now a page with answers to exercies from the textbook. (Only available to registred students.)

The principal instructor is Lars-Henrik Eriksson and Jesper Bengtson will be teaching assistant.

When developing software with very high demands on quality, e.g. in safety-critical systems, formal methods are often used to create software that (at least in principle) can be proven to satisfy its requirements specification. The course will cover specification and development of software using formal methods. The B-method will be used in the course.

Also read the formal course plan.

Buy the textbook now. You will not make it through the course without a textbook.

There is a discussion forum for the course on Studentportalen.

The first meeting will be a lecture at 08:15 on Thursday, Match 19rd, in room 1145.

Attendance is compulsory as the students will be registred and important practical information about how the course will be given. Someone who -- for any reason -- is unabled to attend, must contact Lars-Henrik.

The teaching will consist of lectures and seminars. The lectures will outline the material and point out important issues. Students are expected pick up the details from reading the textbook and other material provided! At the seminars, participants will be asked to make small presentations of the reading material and of their ongoing projects. We will then discuss the presented material.

During the first half of the course, we will cover the textbook, students will decide upon a project and write a formal specification in B. During the second half of the course, students will develop a program and use the B method to prove its correctness. There will also be some scientific papers to read.

The division of course meetings between lectures and seminars can be found on the schedule page.

There will be no proper exam on this course. Students will be rated based on 1) their projects and 2) their participation in the seminars. The projects are worth 3 credit points and the seminars 2 credit points. To pass the course you must have done an "acceptable" project, have participated actively in the seminars and there demonstrated at least a basic understanding of the course material. (You can see the seminars as partly being an ongoing oral examination if you wish.)

An acceptable project involves an essentially complete formal program development from specification to implementation. Each proof obligation should either be formally proved or there should be a convincing argument that it is true. There should be a project report which describes the problem which your program solves as well as the specification, implementation and refinements. The subject and scope of the project must be approved by the principal instructor.

The exact pass grade (3/4/5 or A/B/C/D/E) depends on how well you have mastered the course contents above the minimum level. If you aim at some specific grade, talk to Lars-Henrik and he will give you hints as the course goes on about what you should do to earn that grade.

The principal tool we will use in the course is Atelier B. You will find a description about how to get started with Atelier B here. You can only run Atelier B on the department Unix systems. The tool is licensed software which only runs on designated computers. There is a web site for Atelier B, but it describes a newer version of the software which was released too late to be used in the course this year.

There is extensive on-line documentation about Atelier B.

The textbook uses another tool -- the B-toolkit. The differences in the B language are minor and mainly concerns implementation machines. Important differences are described here.

There some known bugs and restrictions in Atelier B, which are described here.

• A library machine for string manipulation.
• Slides from the industrial use of formal methods lecture.
• Slides from the lectures
• Answers to the exercises in the textbook (only accessible to registred students).
• Reference sheets with the B notation symbols.
• The paper about MÉTÉOR. This is a link to the Springer-Verlag web site. For copyright reasons, it does not work outside the university.
• A paper about the use of B with railway safety systems.
• A paper about automatic train operation system on the New York subway.

• "The B-method: An Introduction" by Steve Schneider, Palgrave, 2001, ISBN 0-333-79284-X. This is the textbook of the course. There is a resource web page for the book, including source code for the examples.
• "The B-book" by Jean-Raymond Abrial, Cambridge University Press, 2005, ISBN 0-521-02175-8. This is the definitive description of B by its inventor.

• The Grenoble B site
• B on The Formal Methods wiki
• Wikipedia about the B-method
• The Formal Methods wiki