Tool support for checking railway interlocking designs
Kirsten Winter, Wendy Johnston, Peter Robinson, Paul A. Strooper, Lionel van den Berg · 2006
The development of railway interlocking systems is currently very labour-intensive. Specialists develop the interlocking de-sign for a particular area and manually check for completeness and consistency. The interlocking is implemented in either soft-ware or using electrical relays. The interlocking has to be tested against the safety requirements for signalling systems, i.e., the signalling principles. The whole process can be supported by various tools, rang-ing from editors to animators. In this paper we focus on ex-ploiting model checking to automatically check the design with respect to safety. The main concerns of this technique are the problem size and the eciency of available tools. We have in-vestigated both of these problems: seeking to work with a min-imal model of the interlocking design and to improve eciency of the model-checking process by exploiting domain knowledge of our particular application.