Specification and verification of a railway level crossing

Le domaine d’intérêt est la modélisation et la vérification formelle des spécifications de la logique de sécurité d’un passage à niveau ferroviaire. En effet, Infrabel, le gestionnaire de l’infrastructure ferroviaire belge, souhaite renouveler son système de passage à niveau et que les spécifications du nouveau système soient validées par une approche scientifique. Un passage à niveau est un endroit où une ligne de chemin de fer et une route se rencontrent au même niveau. Un passage à niveau appartient à la catégorie des systèmes de sécurité et doit être conçu selon les normes de sécurité les plus élevées (IEC61508). L’objectif de cette thèse est de développer un modèle de passage à niveau à partir des spécifications fonctionnelles, et de vérifier les propriétés de sécurité liées à son comportement. Le document de base supportant la modélisation est écrit en langage semi-formel (machines à états et expressions booléennes). Un modèle du système de passage à niveau est donc réalisé en Event-B. Les propriétés de sécurité sont encodées dans le modèle. Certaines de ces propriétés sont prouvées. Et d’autres propriétés sont démontrées comme étant fausses. Ce document reprend la façon dont le système a été modélisé avec les choix de modélisation. Il reprend également les méthodes de preuve utilisées pour vérifier ou réfuter une propriété.