# Provably Correct Software, Spring -11

## News

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

- (2010-05-20) Updated information about Atelier B version 4.0.2.
- (2010-05-04) I've added download links for the latest version of Atelier B.
- (2010-02-11) Schedule change: The seminar om Monday, February 14, is moved to Wednesday, February 16, 10-12, in room 1146. The lecture on Wednesday, February 16 is moved to Monday, February 21, 10-12, in room 1245. The lecture slides have been updated to reflect the change.

## Teachers

The principal instructor is Lars-Henrik Eriksson.

## About the course

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.

## Course plan

The first meeting will be a lecture at 13:15 on Tuesday, January 18th, 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 half 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 half, 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 if previous and suggested projects 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.

## Examination

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.

## Atelier B

The principal tool we will use in the course is Atelier B, version 4.0.2, which runs on SPARC Solaris, Linux, Windows and Mac systems. It is installed on the department Unix (Solaris) systems and also available for download here.

Presently, only the copy installed on the department Unix systems is able to properly access libraries and generate executable code, so to do these things, you must run Atelier B on the department computers. You will find a description about how to get started with Atelier B on the department systems 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.

An older version of Atelier B, 3.7.1, is available on the department Unix systems only. See this link for instructions on how to run the system and this link for on-line documentation.

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.

## ProB

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.

## Handouts, slides and other course material

- 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.

## Literature

- "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.

## Web resources about the B-method and formal methods in general