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
Link to this offer
Linked to this offer
- Why does the Baseline 3.6.0 ETCS standard require a SIL2 DMI (train display)?
- A certified version of ATELIER B is planned for 2024
- CLEARSY is partnering with UIC to define safety demonstration methods for innovative systems
- Formal activities through the V cycle
- CLEARSY realizes the formal proof of the Control – Command – Signalling system of the HPMV project.
- The new formal tool Atelier B 4.7 is available.
- CLEARSY participates in the conference ISOLA 2021
- Formal methods in action in the railways
- CLEARSY participated in the prestigious International Conference on Formal Methods, FM 2015