Vérification formelle pour la sécurité de l'exploitation ferroviaire fondée sur les cantons mobiles – 4RaiMBO

Dans le contexte des systèmes ferroviaires, le mode de transport qui émet le moins de CO2, la demande de transport de passagers devrait augmenter de 40 % d'ici à 2050. Pour répondre à cette demande, la construction de nouvelles lignes ferroviaires est très coûteuse et parfois irréalisable en raison des contraintes urbaines et du manque d'espace. Une solution alternative consiste à mettre en œuvre la prochaine génération de systèmes de signalisation, basée sur le concept du système Moving Block (MB), et capable d'optimiser la gestion du trafic ferroviaire. Le principe du système MB est de séparer les trains en utilisant une distance de freinage absolue (la distance nécessaire pour atteindre un point d'arrêt) couplée à une marge de sécurité. Il promet donc des avantages significatifs en termes de capacité des lignes, de coûts d'installation et d'exploitation, de fiabilité et d'interopérabilité [2]. Cependant, les spécifications complètes du système MB sont encore en cours de développement et devront être affinées avant qu'il puisse être considéré comme une solution viable et, surtout, sûre pour les chemins de fer européens. Dans le cadre de ce projet, nous contribuerons à la vérification et à la validation des spécifications du système MB. L'idée est de générer une ontologie pour le système MB à partir des spécifications du système et de proposer une approche de modélisation pour le développement de modèles formels utilisant l'ontologie définie.
Les objectifs du projet sont :
Objectif 1 : Définir une ontologie pour ETCS L3 sur la base d'une analyse des spécifications du système.
Objectif 2 : développer une méthodologie pour générer des modèles formels à partir de l'ontologie de l'ETCS L3.
Objectif 3 : Représenter les scénarios opérationnels à l'aide de la modélisation formelle et/ou de la simulation.