Formal Modeling and Verification of Train Control Systems

Abstract

Le degré d'automatisation des systèmes de contrôle ferroviaire est en constante augmentation. Les industriels ferroviaires ont besoin d'un niveau accru de sécurité et de fiabilité pour remplacer les conducteurs par des systèmes de contrôle automatique des trains (ATC). Cependant, la complexité du système est également fortement augmentée par l'intégration des fonctions automatiques, ce qui rend difficile l'analyse de ces systèmes.Différentes méthodes de modélisation peuvent être utilisées pour construire les modèles du système au niveau d'abstraction approprié. Les méthodes de modélisation formelles et les méthodes de vérification formelles fournissent un cadre crucial pour assurer les propriétés de sécurité et de fiabilité. Les Réseaux de Petri constituent un outil formel approprié à la modélisation et à la vérification de systèmes critiques comme les systèmes de contrôle automatique du ferroviaire. Dans cette thèse, nous utilisons plus particulièrement les réseaux de Pétri colorés (CPNs) de Jensen pour exploiter la modularité et la hiérarchisation pour la modélisation et la vérification d’un système de grande taille