Provably Correct Software, Spring -10
Below this headline, you'll find important updated information about the course. Make it a habit to check the News regularly!
- (2010-06-02) The course evaluation is now open.
- (2010-02-17) I've updated the lecture slides again. There is also an updated version of my Industrial use of formal methods slides.
- (2010-02-16) I have made a list of previous student projects and suggested projects.
- (2010-02-13) Added information on ProB.
- (2010-02-12) Atelier B can only be run on Unix machines with SPARC architecture. The section on running Atelier B now includes a link to a list of machines and their architectures.
- (2010-02-11) Schedule change: The lecture on Tuesday, February 16 is moved to Wednesday, February 17, in room 2145 (not 1245), same time 13-15.
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.
The first meeting will be a lecture at 08:15 on Wednesday, January 20th, 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 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 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 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 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. The version of Atelier B which we will only run on the department Unix systems with SPARC achitecture. There is newer version which will run on Linux, Windows and Mac systems but which has some problems which makes it unsuitable for this course. If these problems are corrected during the course we may switch versions. There is a web site describing the new version of Atelier B.
There is extensive on-line documentation about Atelier B.
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.
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.
- "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