Analysis of the safety critical software of the PARIS CBTC line 1

Système automatique d’exploitation des trains, ligne 1 (SAET L1)

The SAET L1 (CBTC) project makes part of the global project of paris metro Line 1 automation, same as line 14.

  • DATE : 2009
  • LOCATION : Line 1, Paris Metro

A particular feature of the project is that it must take place without incurring any downtime and with a mixed operating phase (automatic and manual) on an already existing line.

The SAET L1 is a CBTC (Communication Based Train Control) controlling various automatic pilots and supervision modules. The CBTC is developed in B by Siemens Transportation Systems (identical to line 14).

Our actions

The activities performed focus on the safety aspect of the SIL4 software and are said to be a second look. They comprise:

  • Analysis and critical rereading of the various B models, the Ada code as well as the various documents supplied (design files, specifications, safety analyses, etc),
  • Verification of the rules added within the context of the formal software proof,
  • Validation of the tests,
  • Replay of the formal proofing performed with Atelier B.
Link to this référence

Need a custom-made system ?

We are safety software and systems designers.  Contact us and let's discuss your project together!