Validation of a New Functional Design of an Automatic Protection System at Level-Crossing with Model-Checking Techniques
MEKKI ; GHAZEL ; TOGUYENI
Type de document
ARTICLE A COMITE DE LECTURE REPERTORIE DANS BDI (ACL)
Langue
anglais
Auteur
MEKKI ; GHAZEL ; TOGUYENI
Résumé / Abstract
Level Crossings (LCs) are considered as 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. Actually, 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 moment are generally equipped with Automatic Protection Systems (APS). 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 which prevents these kinds of scenarii and, therefore, increases the global safety of LCs. In order 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, namely Timed Automata (TA), for the specification phase and the model-checking formal technique for the verification process. All the steps are discussed and illustrated progressively.
Source
IEEE Transactions on Intelligent Transportation Systems, num. Vol13,issue 2, p714 - 723 p.
Editeur
IEEE
