Modeling and verification of safety properties of a railway infrastructure using Statecharts.

Summary The objective of the work presented in this article is to model a railway infrastructure composed of tracks, switches and traffic lights in order to verify some safety properties related to the operation of this infrastructure. The modeling will be done using the Statecharts formalism and the Stateflow tool. The approach to verify the safety properties will be done by simulating the operation of the infrastructure. This approach is based on an attainability research of the dangerous states related to the operation of the infrastructure. The attainability analysis of the dangerous states allows the detection of a near miss. Finally, the Statechart model will be used for the simulation of a near miss scenario between two trains.