A model pattern of railway interlocking system by Petri nets

The railway interlocking system (RIS) is one of the crucial parts of the railway transit safety. In the French railway domain, the computer-controlled relay-based interlocking systems are the dominant practice. Their complex sequences and consequent actions make it difficult to formally validate their safety properties. For such a system, detailed verification and validation of its specifications should be done at the end of the design phase. In practice, each station or yard in a railway line has its own interlocking system, which respects the same national standard but has a different facility formation. In order to effectively accomplish the validation tasks and reduce the error probability, this paper introduces a modelling pattern of the French railway interlocking system, which is a parameterized model respects the French national rules. It is a general reusable solution to this kind of problem and can be used in many different given contexts.