The B-Method

Steve Schneider and Helen Treharne
Royal Holloway, University of London

Overview
Successful large-scale formal development of software relies on
approaches which have effective tool support. The B-Method develops
the ideas of the specification languages Z and VDM, and combines them
with ideas from Dijkstra's guarded command language and from
refinement.  It is currently the most complete formal development
method which supports all stages of the software lifecycle from
specification through design through to automatic code generation,
providing a unified approach to specification, design and programming.
It is particularly used in sectors of industry where safety is a
concern---for example, it was recently used in the development of the
control software for the automatic driverless trains on the new Meteor
line of the Paris metro, and the subsequent testing of the system
revealed no bugs in over 80,000 lines of code!

The method is supported by industrial strength CASE tools: suites of
packages providing support for all aspects of the method.

Aims
----

At the end of this course, students should have an understanding of
how the B-Method is used to support formal specification, refinement,
and implementation, and provable correctness.  The course will also
introduce the B-Toolkit, which supports the formal aspects of
development including theorem proving.  Emphasis will be placed on the
underlying theory, and on its practical application.  It will also
include some practical time with the B-Toolkit.


Provisional syllabus
--------------------

General Substitution Language and Abstract Machine Notation;

Specification: Machines, operations, states, preconditions,
invariants; conditionals, nondeterminism;

Refinement: Data refinement, operation elaboration;

Implementation: Concrete state, library machines, BASE machines, code
generation, loops, structuring developments;

Structuring Machine Descriptions: Inclusion, seeing, using, promotion,
extension;

The B Toolkit: Analysis, animation, code generation, library machines,
automated proof, proof assistance, markup generation;

Case studies and practical examples.


References


1. S. Schneider:  The B-Method: an Introduction

2. J-R Abrial, "The B Book", Cambridge University Press

3. J.B. Wordsworth, "Software Development with B: An introduction",
Addison Wesley

4. K. Lano and H. Haughton, "Specification in B, an introduction using the
B Toolkit", Imperial College Press