Formal Modeling and Verification of Train ...
Document type :
Thèse
Title :
Formal Modeling and Verification of Train Control Systems
English title :
Modélisation et Vérification Formelles de Systèmes de Contrôle de Trains
Author(s) :
Xie, Yuchen [Auteur]
Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]
Centre de Recherche en Informatique, Signal et Automatique de Lille - UMR 9189 [CRIStAL]
Thesis director(s) :
Armand Abdoul Karim Toguyeni
Manel Khlif
Manel Khlif
Defence date :
2019-02-14
Jury president :
Jean-François Pétin [Président]
Audine Subias [Rapporteur]
Pascal Berruet
Thomas Bourdeaud'huy
Audine Subias [Rapporteur]
Pascal Berruet
Thomas Bourdeaud'huy
Jury member(s) :
Jean-François Pétin [Président]
Audine Subias [Rapporteur]
Pascal Berruet
Thomas Bourdeaud'huy
Audine Subias [Rapporteur]
Pascal Berruet
Thomas Bourdeaud'huy
Accredited body :
Ecole Centrale de Lille
Doctoral school :
École doctorale Sciences pour l'ingénieur (Lille)
NNT :
2019ECLI0001
Keyword(s) :
Systèmes à évenements discrets
Réseaux de Petri colorés
Modélisation formelle
Vérification formelle
Systèmes ferroviaires
Système de contrôle automatique des trains
Réseaux de Petri colorés
Modélisation formelle
Vérification formelle
Systèmes ferroviaires
Système de contrôle automatique des trains
English keyword(s) :
Discrete event systems (DES)
Colored Petri Nets (CPN)
Formal modeling
Formal verification
Railway systems
Automatic train control
Colored Petri Nets (CPN)
Formal modeling
Formal verification
Railway systems
Automatic train control
HAL domain(s) :
Informatique [cs]/Autre [cs.OH]
French 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 ...
Show more >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 tailleShow less >
Show more >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 tailleShow less >
English abstract : [en]
The automation degree of railway control systems is constantly increasing. Railway industry needs the enhanced level of safety and reliability guarantee to replace the drivers by Automatic Train Control (ATC) systems. ...
Show more >The automation degree of railway control systems is constantly increasing. Railway industry needs the enhanced level of safety and reliability guarantee to replace the drivers by Automatic Train Control (ATC) systems. However, the system complexity is also heavily increased by the integration of automatic functions, which has caused the difficulty to analyze these systems.Different modeling methods can be used to build the system models at the appropriate level of abstraction. Formal modeling methods and formal verification methods can provide crucial support to ensure safety and reliability properties. Petri Nets are a suitable tool for modeling and verifying critical systems such as automatic train control systems. In this thesis, we use more specifically Colored Petri Nets (CPNs) to exploit modularity and hierarchization for the modeling and verification of a large-scale system.Show less >
Show more >The automation degree of railway control systems is constantly increasing. Railway industry needs the enhanced level of safety and reliability guarantee to replace the drivers by Automatic Train Control (ATC) systems. However, the system complexity is also heavily increased by the integration of automatic functions, which has caused the difficulty to analyze these systems.Different modeling methods can be used to build the system models at the appropriate level of abstraction. Formal modeling methods and formal verification methods can provide crucial support to ensure safety and reliability properties. Petri Nets are a suitable tool for modeling and verifying critical systems such as automatic train control systems. In this thesis, we use more specifically Colored Petri Nets (CPNs) to exploit modularity and hierarchization for the modeling and verification of a large-scale system.Show less >
Language :
Anglais
Collections :
Source :
Files
- https://tel.archives-ouvertes.fr/tel-02507447/document
- Open access
- Access the document
- https://tel.archives-ouvertes.fr/tel-02507447/document
- Open access
- Access the document
- https://tel.archives-ouvertes.fr/tel-02507447/document
- Open access
- Access the document
- document
- Open access
- Access the document
- Xie_Yuchen_DLE.pdf
- Open access
- Access the document