The B method is a method of formal specification capable of rigorously re-transcribing the requirements of a set of specifications, by means of mathematical proofs, in order to prove their data consistency. This process is especially useful for removing any ambiguity in the properties initially expressed in natural language. The B language can be used in protocols as well as in embedded computing. Moreover, the B method encompasses all modelling by the proof of a system, from the writing of its model to the installation of its software.
Although the uses of the B method are diverse (modelling of a system, formalisation of specifications …) the aim is the same: to use mathematical proofs to ensure the reliability and security of a system and to make sure that there are no computer bugs in the system.
The B method draws its legitimacy from the development of approved tools, which are used on a large scale both in the world of industry and in the university sphere, such as Atelier B. ClearSy is the holder of Atelier B and is responsible for its development and for the maintenance of its development platform. Atelier B therefore constitutes a reference for the development of proven software.