Know-how

Formal Methods


B METHOD
FORMAL VERIFICATION OF SPECIFICATIONS

B METHOD


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

Formal verification of specifications


Due to our experience in modeling and our ability to understand and abstract our clients’ needs, we are able to support operators, industry and originators in verifying specifications for systems and software.
The B Method, associated with other formalisms, is used to analyze, validate, reorganize and provide elements that may complete specifications. This approach is applicable to every industrial sector. Today, it is used successfully in the automotive, bank, space and nuclear sectors.

ADVANTAGES OF THE FORMAL VERIFICATION

The advantages observed are :
> A more rapid focus on difficult areas
> Reliable and justifiable summary
> Direct and precise questionning
> Proof of coherence
> Achievable completeness
> Elimination of professional “unsaids requirements”
> Consideration of functional and dysfunctional aspects

For a return on investment that is positive in terms of :
> Decrease iin delayed features
> Gains in validation (Improved testability)
> More rapid convergence (Realization quality)
> Greater capitalization of knowledge