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

Fiche Technique

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

Val de Roissy
Val de Roissy

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 lignes d’ADA au final.

Ces logiciels sont classés SIL4 selon la norme IEC61508 : EN50126, EN50128, EN50129.

Le système simplifié

Schéma du Val de Roissy
Schéma du Val de Roissy

Quelques chiffres…

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.

Une seconde ligne pour l’aéroport Charles de Gaulles devrait être inaugurée en Juin 2007.

Publications et retours d’expérience

  • Document d’introduction : réalisation des logiciels sécuritaires SIL4 du Val de Roissy : téléchargez
  • Conférence ZB2005 : Article “Using B as a High Level Programming Language in an Industrial” : téléchargez
  • Conférence ZB2005 : Présentation (transparents) “Using B as a High Level Programming Language in an Industrial Project”: téléchargez
  • 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 – Dollé D. téléchargez l’article
  • Formal Methods in Industry: Achievements, Problems, Future – Jean Raymond Abrial Swiss Federal Institute of Technology Zurich : Portal.acm.org
  • MetroPole : un article sur le Val de Roissy