Railway Services

Val de Roissy

Siemens Transportation Systems (STS) has subcontracted with ClearSy for the realization with B of the safety software for the automatisms of the future VAL de ROISSY.

Development of SIL4 safety software for the fixed automatisms of the future Val de Roissy

> REALIZATION OF THE SAFETY SOFTWARE WITH THE B METHOD

Siemens Transportation Systems (STS) has subcontracted with ClearSy for the realization with B of the safety software for the automatisms of the future VAL de ROISSY: alarm control unit (UCA) and automatic section drivers (PADS) for Siemens.

This software represents approximately 150,000 ADA lines once completed.

The software is classified as SIL4, according to standards IEC61508: EN50126, EN50128, EN50129.

A few figures

On the L1 VAL line inaugurated on 4th April 2007, 2 computers have been installed: the UCA and PADS (as many PADS as required – S for Section).

FOR THE PADS SOFTWARE:

  • 186,440 lines for the AS Ada safety code (AS – Safety Application)
  • 30,632 lines for the AS non safety-critical Ada code
  • number of mathematical Proofs: 62,056
  • number of B lines: 256,653 lines

FOR THE UCA SOFTWARE:

  • 50,085 lines for the AS Ada safety code
  • 11,662 lines for the AS non safety-critical Ada code
  • number of mathematical Proofs: 12,811
  • number of B lines: 65,722 lines

The number of effective B lines is smaller than that announced as comments are taken into account, including remarks which guide refinement.

Publications and feedback

Introduction document :

Article “Using B as a High Level Programming Language in an Industrial Project”

Conférence ZB2005 :

Présentation (transparents) “Using B as a High Level Programming Language in an Industrial Project”

Météor :

a Successful Application of B in a Large Project”, FM’99, Toulouse, France, 1999 – Behm P., Benoît P., Faivre A., Meynadier J.-M.

vitalSoftware :

Formal method and coded processor – ERTS 2006 – 25-27 January 2006 – Toulouse – Dollé D.

Formal Methods in Industry :

Achievements, Problems, Future – Jean Raymond Abrial Swiss Federal Institute of Technology Zurich