Val de Roissy

Développement des logiciels sécuritaires SIL4 des automatismes fixes du futur Val de Roissy

Réalisation du logiciel sécuritaire avec la Méthode B

Siemens Transportation Systems (STS) sous-traite avec CLEARSY la réalisation avec B des logiciels sécuritaires des automatismes du futur VAL de ROISSY : Unité de Contrôle des Alarmes (UCA) et les Pilotes Automatiques De Section (PADS), pour le compte de Siemens.

Ces logiciels représentent environ 150 000 ligne d’ADA au final. Ces logiciels sont classés SIL4 selon la norme IEC61508 : EN50126, EN50128, EN50129.

Quelques chifres

Sur la ligne L1 du VAL inaugurée le 4 Avril 2007, 2 calculateurs ont été installés : l’UCA et le PADS (autant de PADS que de besoin – S pour Section).

Pour le logiciel PADS :

• 186 440 lignes pour le code Ada sécuritaire de l’AS (AS – Application de Sécurité)
• 30 632 lignes pour le code Ada non-sécuritaire de l’AS
• nombre de Preuves mathématiques : 62 056
• nombre de lignes B : 256 653 lignes

Pour le logiciel UCA :

• 50 085 lignes pour le code Ada sécuritaire de l’AS
• 11 662 lignes pour le code Ada non-sécuritaire de l’AS
• nombre de Preuves mathématiques : 12 811
• nombre de lignes B : 65 722 lignes

Le nombre de lignes de B effectives est moindre que celui annoncé car il y a prise en compte des commentaires, dont des commentaires qui guident les raffinements.

Publications et retours d’expérience

• Document d’introduction : réalisation des logiciels sécuritaires SIL4 du Val de Roissy
• 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
• MetroPole : un article sur le Val de Roissy