A Formal Approach for a Railway Level Crossing Using the Event-B Method

Accidents at level crossings often cause dramatic material and human damages that seriously affect the reputation of rail safety. Research on Level Crossing (LC) safety has attracted considerable attention in recent years. In this paper, we rely on formal methods, based on mathematical rigour, which provide real help for the designer to evaluate the behaviour of a system and avoid errors before its implementation. Thereby, we propose a railway LC system that suggests a new architecture which prevents very risky situations causing several accidents. To do so, we adopted the Event-B formal method to specify the safety requirements of our system and verify its correctness. Event-B is based on the refinement technique which allows a problem decomposition and then reduces modelling and verification effort.