Title :
Validation of a New Functional Design of Automatic Protection Systems at Level Crossings with Model-Checking Techniques
Author :
Mekki, Ahmed ; Ghazel, Mohamed ; Toguyeni, Armand
Author_Institution :
French Inst. of Sci. & Technol. for Transp., Dev. & Networks, Villeneuve d´´Ascq, France
fDate :
6/1/2012 12:00:00 AM
Abstract :
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.
Keywords :
automata theory; formal verification; railway accidents; railway safety; automatic protection systems; formal notation; functional design; global safety; level crossings; model checking; railway accident; railway transportation; safety black spot; timed automata; transportation authorities; Accidents; Delay; Europe; Rail transportation; Roads; Safety; Sensors; Level crossing (LC); model checking; safety; specification; timed automata (TA); verification and validation;
Journal_Title :
Intelligent Transportation Systems, IEEE Transactions on
DOI :
10.1109/TITS.2011.2178238