June 20, 2011
Ryma Metnani (LACL / RATP)La RATP a entrepris des projets de modernisation, d’améliorations et d’automatisation du métro. Parmi ces projets, celui de remplacer les anciens postes de manœuvres (PML) électromécaniques qui permettaient la gestion des trains en terminus (garage/dé garage, retournements, formations destructions itinéraires) par des postes de manœuvre informatisé (PMI).
Le cœur fonctionnel et sécuritaire du système PMI est implémenté dans le module d’enclenchement (MEI) qui est chargé d’exécuter les commandes d’opérateur, gérer les appareils de voie et les signaux et assure la sécurité des déplacements des trains dans les zones de garages. Ce module est donc classé SIL-4 (Safety Integrity Level), le niveau le plus élevé selon les normes CENELEC pour les systèmes ferroviaires. Pour atteindre ce niveau de confiance dans la sécurité, la RATP et THALES ont choisi d’utiliser une méthode de validation basée sur les techniques de model-checking en utilisant l’assistant de preuve ProverSL développé par la société Prover Technology. Après une première expérimentation avec les postes de manœuvre de la ligne 3bis, cette méthode a été utilisée pour la validation des postes de la ligne 1, mais sans réussir à couvrir la totalité de la validation qui a donc été complétée par des tests.
L’objet de la thèse est donc d’étudier les difficultés techniques rencontrées lors de la validation des PMI et d’y apporter des solutions techniques pour étendre le champs d’application de la preuve aux cas complexes (traitement de « gros » postes, modélisation des interfaces, définition et preuve des propriétés de sécurité propres aux interfaces, etc.).