Presentation og the B Method

B, for the design of proven systems and software

B is a formal specification method which, thanks to an adequate language, allows for highly accurate expressions of the properties required by specifications. One can then prove in a fully automated fashion that these properties are unambiguous, coherent and are not contradictory. This then allows us to mathematically prove that these properties are taken into account as the design stages progress.

Therefore, this method and its associated proof allow for:

• Clear technical specifications and system specifications to be reached that are structured, coherent and unambiguous,
• The development of software that is contractually guaranteed to be fault-free,

in areas such as real time, industrial automatisms, communication protocols, cryptographic protocols, onboard IT…

The B Method

B Method usually refers to the set that includes: B language, refinement, proof and related tools.

B development starts with the writing of a concrete model that includes all of the defined needs. The main data processed by the system is described, as well as the fundamental properties of this data. Services ensure the processing of this data while preserving its properties. The B model thus obtained is a specification of what the system should create.

The B model is then transformed (refined with B vocabulary) until a complete software installation of the software is obtained.

Finally, we arrive at a concrete model, proven and fault-free, that can be coded into C or Ada language.

B Method is therefore: “a proven construction approach (referred to as correct) based on B Language, refinement and proof."

B Method Objectives

Invented by Jean-Raymond Abrial, the B Method is first and foremost a new approach for the specification and design of software that ensures its safety and reliability. All of the specification, design and coding processes are therefore fully based on the realization of a certain number of mathematical proofs.

It is only once a model has been mathematically proven that it is considered coherent and fault-free.

The main objectives of this method are therefore:

• To create correct software by construction
• To model systems in their environment
• To formalize specifications
• To simplify programming

B Method Distribution

Renowned for its effectiveness, the B Method is widely distributed and well known in the industry and universities. It can be used in a variety of sectors, such as rail transport, aeronautics, defence and R&D.

The success of the B Method is constantly growing, primarily because of the distribution of major tools such as Atelier B, an industrial tool that allows for the operational use of the B Method in developing proven software.

Clearsy is responsible for development with tools such as Atelier B in collaboration with industry, research centres and Jean Raymond ABRIAL.

B Method Users

B Method users come from diverse and varied fields including,

• Industry: Seeking safe systems that use formal methods, as well as new technologies that meet industry’s needs.
• Originators: Seeking answers to functional questions and relying on the B Method as a sustainable solution.
• Experts and specialists: Individuals who seek information on formal methods at a very high technical level.
• Specialized R&D researchers: Working towards the sustainable development of formal methods in order to develop new solutions for the future.
• University professors and researchers: Who teach B in an academic environment and study potential changes to formal methods.
• Students: Composed of researchers or simply students wanting to use B tools.

The B Method and its Tools

The following are some of the major B tools:

	Atelier B An industrial tool that allows for the operational use of the B Method in the development of proven software. Training is available to understand and use B.
	B4Free An academic tool that allows for the operational use of the B Method in the development of proven software.
	CompoSys Formal design tool for system architectures.
	Brama Formal design tool for system architectures.

B Documentation
ClearSy : Industrial Use of B