Des Références Ferroviaires

Produit

Contexte

Notre intervention

Urbalis Evolution

Nouveau produit logiciel

Modélisation, réalisation et preuve formelle (méthode B) du logiciel embarqué : contrôle d'énergie et localisation

Réalisation d'un outil sécuritaire de génération des données ferroviaires qui paramètrent le logiciel embarqué

Calculateurs de sécurité

Vérification

Modélisation et décomposition d'une architecture redondante de calculateurs devant respecter des exigences de sécurité (matériel, logiciel et communication).  Production d'un document (HTML) explicitant les règles de sécurités et leur inter-dépendance à des fins de validation.

ATO

Réalisation de l'ATO MF200

Spécification d'un automate de contrôle de vitesse embarqué (système hybride) (ATO), mise au point par simulation sous Matlab et production du code logiciel embarqué

Meteor Phase 3

Développement de l'extension de la ligne 14 du métro de Paris

Validation des données topologiques des voies

Meteor New York

Développement  d un logiciel SIL4 de pilote automatique pour une ligne du Métro de New York

Validation du logiciel par preuves mathématiques

Val  de Roissy

Développement des logiciels sécuritaires des automatismes fixes : Unité de Contrôle des Alarmes (UCA) et les Pilotes Automatiques De Section (PADS).

Développement selon la méthode B des logiciels : réalisation de la conception générale formelle (exigences) et de la conception détaillée formelle (algorithmes et code) ; preuve mathématique de cohérence, de  raffinement et de codage.

ATP Métro de Lyon

Transformation d'une logique câblée en logique programmée. Les bugs présents dans la version hard-codée ont dû être réintroduits dans la version logicielle afin de ne pas perturber les conducteurs.

Vérification du cycle de développement des fonctions logicielles de sécurité (audit).

ATP Métro de Hong-Kong 

Validation des logiciels sécuritaires Bord.

ATP Métro de Singapour 

Validation des logiciels sécuritaires Bord.

ERTMS 

ERTMS est un standard en cours de développement, qui permet l'interopérabilité des trains sur les réseaux internationaux l'implémentant

Validation du logiciel LEU.

MF2000

Validation pour RATP/AQL délivrant une accréditation COFRAC.

Validation de certaines fonctions de l'informatique de sécurité embarquée de ce matériel roulant.

MF2000

Validation pour RATP/AQL délivrant une accréditation COFRAC.

Vérification des conditions de test de l'informatique de confort embarquée (climatisation, venti-lation, éclairage, annonces sonores.) de ce matériel roulant.

ASIFER

Homologation du poste de paramétrage des PIPC Alcatel (niveau demandé : SIL4).

Le poste de paramétrage produit, à partir d'une représentation graphique de l'installation à équiper (gare, .), le paramétrage du poste de signalisation PIPC qui coordonne tous les équipements de signalisation impliqués. Ce paramétrage, binaire, est de sécurité. Pour réduire la durée des essais de 20 jours à 1 jour, RATP a demandé un niveau SIL4, qui doit être obtenu grâce à des comparateurs inverses qui, à partir du paramétrage binaire, doivent revenir à la description graphique. Deux comparateurs utilisant des technologies différentes doivent être capables de reproduire les informations d'entrée.

Vérification complète des logiciels sécuritaires développés (vérificateurs directs et inverses) :

- revue des règles de codage

- analyse des specs et conception

- lecture critique de code.

Logiciel Codeur et extension 

Logiciel équipant les équipements de signalisation sol pour émission vers les trains.

Homologation du logiciel de codage des informations balise à destination des trains (niveau demandé : SIL4).

Logiciel CRTC 

Logiciel installé à bord des trains et recevant les informations codées (voir Logiciel codeur) en provenance du sol. Ce logiciel décode les informations reçues et les envoie à l'ATP.

Développement du logiciel recevant les informations codées de la signalisation sol (niveau demandé : SIL4).

BKL/TIVD 

Equipement de signalisation sol devant déterminer si un signal est ouvert ou non et envoyer cette information au signal précédent afin d'avertir le conducteur s'il doit freiner ou pas (niveau demandé : SIL4).

Assistance au développement et Management de la sécurité du produit.

Ventilation des stations 

Validation des spécifications (fonctionnelles et de sécurité) de la fonction ventilation des stations, en fonction des exigences de sécurité et de la norme en vigueur (accréditation COFRAC).

Analyse des specs et des normes. Vérification de la traçabilité.

Urbalis 200

Traduction du logiciel de l'ATP Bord Urbalis 200 pour le métro de Shanghai du langage Modula2 vers les langages B (partie sécuritaire) et ADA (partie fonctionnelle), puis validation de l'exécutable ADA-PSC sur un banc de test hôte. Rétro-spécification formelle de la partie sécuritaire en vue d'une validation par la preuve. Préparation du logiciel en vue d'une intégration sur une cible de type mono processeur codé.

Portage d'une application sécuritaire (SIL4), validation et intégration.

Chaîne de production de logiciels sécuritaires

Dans le cadre de projets de développement de logiciels de sécurité avec la méthode B, plusieurs environnements de traduction du langage B vers le langage ADA ont été développés.

Maintenance des différents outils constituant la chaîne de  compilation et de traduction.