|
Development of SIL4 safety software for the fixed
automatisms of the future Val de Roissy
The simplified system

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.
A second line for Charles de Gaulles airport is due to be inaugurated in June 2007.
Publications and Feedback
-
Introduction document: realization of SIL4 safety
software for the Val de Roissy: download
-
Conférence ZB2005 : Article "Using B as a High Level Programming Language in an Industrial Project" : download
-
Conférence ZB2005 : "Using B as a High Level Programming Language in an Industrial Project" (slides) : download
-
Meteor: "A Successful Application of B in a Large
Project", FM'99, Toulouse, France, 1999 - Behm P., Benoît P., Faivre
A., Meynadier J.-M. SpringerLink.com
-
Vital software: Formal method and coded processor - ERTS 2006 - 25-27 January 2006 - Toulouse -
Dollé D. download the article
- Formal Methods in Industry: Achievements, Problems, Future - JeanRaymond Abrial Swiss Federal Institute of Technology Zurich : Portal.acm.org
- MetroPole : download the article
|