Provably Correct Software, Autumn -13

Refer to the Student Portal for news announcements regarding the course.

The instructor is Lars-Henrik Eriksson.

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 10:15 on Monday, October 28th, in room 1245.

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 part of the course, we will cover the textbook and students will do small assignments to familiarise themselves with the B-method and the tools. During the second part, students will carry out a project involving the writing of a formal specification in B, the development a program from it and use the B method to prove its correctness. There is a list of previous and suggested projects There may 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 7 credit points and the seminars 3 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 informal 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) 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, version 4.1.0, which runs on Linux, Windows and Mac systems.

We are in the process of upgrading the software. More information on how to run it and access documentation will shortly be available here shortly.

It is installed on the department Linux systems and is also available for download here.

You will find a description about how to get started with Atelier B here.

There is extensive on-line documentation about Atelier B. Here are direct links to the Atelier B User's Manual and B Language Reference Manual.

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

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

The other tool we will use in the course is ProB. You will find a description about how to get started with ProB here. ProB runs on Linux, Windows and Mac OS systems.

On the ProB web site you will find documentation. You can download ProB to your own computer if you wish.

The version of the B language used by ProB is the same as that of Atelier B, so it has the same differences compared to the language in the textbook. However, there are some features of B which ProB does not (yet) support. See this list.

• Slides from the formal methods in software development lecture.
• Slides from the course lectures
• Answers to the exercises in the textbook will be accessible to registred students in the Student Portal after each seminar where we discuss the exercises in question.
• 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 slide presentation about work by Siemens on a train control system for 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.

• ClearSy's resource page.
• ClearSy's link page.
• The Grenoble B-site. It hasn't been updated for some years, but still has useful information.
• B on The Formal Methods wiki
• Wikipedia about the B-method
• The Formal Methods wiki