A reachability analysis for verification of safety properties of railway infrastructures.

Summary The work presented in this paper aims to model a railway infrastructure composed of tracks, switches and signal lights to verify certain safety properties related to the exploitation of this infrastructure. The modeling will be done using statecharts formalism. The verification approach of the safety properties will be carried out by simulating the operation of the infrastructure. This approach is based on a reachability analysis of dangerous states related to the operation of the infrastructure. The reachability analysis of dangerous states allows to detecting a near accident. Finally, the Statechart model is used to simulate a scenario of a near accident between two trains.