Formal system validation

The formal system verification, obtained with the B-method, is an element of the demonstration of the safety of a critical system.

CLEARSY uses the detailed description of the design and algorithms used in the system under analysis in its procedure. The B models developed from these elements contain

• the mathematical formulation of the desired properties,
• the mathematical formulation of all necessary assumptions and
• the elements for conducting the proof.

Once these models are proven with Workshop B, we are guaranteed that the desired properties are mathematically derived from the selected assumptions. These assumptions therefore constitute all the conditions sufficient to logically guarantee the desired properties. These conditions concern the design, the material and the context.

This process requires a detailed understanding of the real “why” of security, thus requiring strong exchanges with the relevant business experts.

For example, CLEARSY conducted a system verification with proof of the New York 7 line CBTC, using the B method.

The proven system properties were:
> No collision between trains
> Impossibility of derailment on an unlocked switch
> Impossibility of overspeed