Démonstration de la sécurité d’une application ferroviaire de signalisation en mode nominal et en modes dégradés par la preuve formelle. – PROOFER

Dans le domaine ferroviaire, l'exploitation des systèmes de transport fait intervenir des systèmes temps réels dits critiques en interaction avec un environnement indéterministe. Cet environnement comporte notamment une composante humaine constituée des opérateurs qualifiés appliquant le règlement d'exploitation.

La sécurité globale d'un système de transport repose donc à la fois sur :
• la correction et l'adéquation du règlement d'exploitation,
• et l'absence de défaillance contraire à la sécurité des systèmes temps réels (automatismes locaux et poste de commande centralisé) qu'il intègre.

La correction et l'adéquation du règlement d'exploitation doivent intégrer :
• les nouvelles technologies utilisées pour concevoir les systèmes temps réel,
• les modes dégradés de ces automatismes,
• les fautes humaines des opérateurs.

L'absence de défaillances contraire à la sécurité des systèmes temps réels a déjà fait l'objet de démonstration par des preuves formelles (Météor, systèmes d'enclenchements)

Le projet proposé vise à étendre ces démarches de démonstration de la sécurité par la preuve formelle à la globalité du système en intégrant les automatismes, le règlement d'exploitation et les opérateurs.