Department of Information Technology

Provably Correct Software, Spring -07

News

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

  • (2007-03-06) The seminar on Thursday, March 8, is replaced by individual group meetings according to an e-mailed schedule.
  • (2007-03-01) No lecture Monday, March 5 or Tuesday, March 6. Individual group meetings on Monday March 5.

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.

The course is given for the first time which means that many details are left open at the beginning and decided as the course goes on. It also means that the students will have a great opportunity to influence the course.

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

Course plan

The first meeting will be a lecture at 10:15 on Monday, January 22nd, 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, 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.

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 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 (G/VG 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.

Atelier B

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

Handouts, slides and other course material

  • Slides from the industrial use of formal methods lecture.
  • Slides from the lectures
  • 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 slide presentation about work by Siemens on a train control system for 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.

Updated  2007-03-06 13:36:41 by Lars-Henrik Eriksson.