Home - News - The Worldwide Railway Sector - Our Systems and Software - Offer - Resources - Know-How - Signals and Indicators - Documents - About Us - Clients & Partners - Fairs - Links - Contacts


Development of SIL4 Safety Software for the Fixed Automatisms of the Future Val de Roissy

Technical sheet

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 4 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" : téléchargez
  • Conférence ZB2005: "Using B as a High Level Programming Language in an Industrial Project" (slides): download
  • 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. SpringerLink.com
  • Vital software: Formal method and coded processor - ERTS 2006 - 25-27 January 2006 - Toulouse -
  • Formal Methods in Industry: Achievements, Problems, Future - Jean Raymond Abrial Swiss Federal Institute of Technology Zurich : Portal.acm.org
  • MetroPole : an article on the Val de Roissy

Contact us : Tel : 04 42 37 12 70 - Fax : 04 42 37 12 71 - contact@fersil.fr