Concepts
The B language and the B method provide a means for developing mathematically proven software and systems, complying with requirements, through the use of rigorous mathematical reasoning. However B doesn’t impose a particular way to perform a development, as well as C++ or ADA do not impose a dedicated method for designing and analysing. Gathering B design patterns and modelling solutions would help any development team to define its own development method. This document aims at providing hints, by examining a number of typical problems and by providing solutions.
To read this document, it is better to have a basic understanding of the B language (abstract machine, refinement, implementation, main mathematical constructs).
Let start with a general schema of a project making use of B. The B method is composed of :
- the B language, mathematical and structured notation used to write specification and programs
- a collection of rules, defining what the proof of a project is.
A typical B project is made of the phases described below.
This analysis has to be completed before any modelling. It is not possible, as for other kind of project, to start a B project without having a clear understanding of what has to be otianed at the end.
Once the problem is well understood, a new formulation of the initial requirements needs to be obtained. The objective is to remove as far as possible ambiguities (we are not yet dealing with mathematical stuff at this stage).
This phase is aimed at producing the B specification of the system. Several methods may be used:
- “Flat” specification enumeration of the requirements, than allocation to a B structure. The main difficulty is to find a formulation which is compatible with its structuring in B.
- Specification focusing on the main requirements first. Specification details are introduced with succesive refinements and importations. The main difficulty is to eventually obtain the complete specification while being distributed over several B components.
Design and development are backed by proof all along the development cycle. Process ends when all design details have been introduced, leading to a program written in a subset, implementable, of the B language: the B0 language. Atelier B code generators then transform this B0 modelling into compilable source code
Last modified 1yr ago