Titre :

Validation of a New Functional Design of Automatic Protection Systems at Level Crossings with Model-Checking Techniques

Auteur(s) :

Mekki, Ahmed [Auteur correspondant]
Systèmes Tolérants aux Fautes [STF]
Ghazel, Mohamed [Auteur]
Évaluation des Systèmes de Transports Automatisés et de leur Sécurité [IFSTTAR/ESTAS]
Université de Lille, Sciences et Technologies
Toguyeni, Armand [Auteur]
Systèmes Tolérants aux Fautes [STF]

Titre de la revue :

IEEE Transactions on Intelligent Transportation Systems

Pagination :

714-723

Éditeur :

IEEE

Date de publication :

2012-01-18

ISSN :

1524-9050

Discipline(s) HAL :

Informatique [cs]/Automatique

Résumé en anglais : [en]

Level crossings (LCs) are considered to be a safety black spot for railway transportation since LC accidents/incidents dominate the railway accident landscape in Europe, thus considerably damaging the reputation of railway ...
Lire la suite >Level crossings (LCs) are considered to be a safety black spot for railway transportation since LC accidents/incidents dominate the railway accident landscape in Europe, thus considerably damaging the reputation of railway transportation. LC accidents cause more than 300 fatalities every year throughout Europe, which represents up to 50% of all deaths for railways. That is why LC safety is a major concern for railway stakeholders in particular and transportation authorities in general. LCs with an important traffic moment1 are generally equipped with automatic protection systems (APSs). Here, we focus on two main risky situations, which have caused several accidents at LCs. The first is the short opening duration between successive closure cycles relative to trains passing in opposite directions. The second is the long LC closure duration relative to slow trains. In this paper, we suggest a new APS architecture that prevents these kinds of scenarios and therefore increases the global safety of LCs. To validate the new architecture, a method based on well-formalized means has been developed, allowing us to obtain sound and trustworthy results. Our method uses a formal notation, i.e., timed automata (TA), for the specification phase and the model-checking formal technique for the verification process. All the steps are progressively discussed and illustrated.Lire moins >

Langue :

Anglais

Comité de lecture :

Oui

Audience :

Internationale

Vulgarisation :

Non

Collections :

• Centre de Recherche en Informatique, Signal et Automatique de Lille (CRIStAL) - UMR 9189

Source :

Harvested from HAL