Tool Support for Checking Railway Interlocking Designs

Winter, K., Johnston, W., Robinson, P., Strooper, P. and van den Berg, L.

The development of railway interlocking systems is currently very labour-intensive. Specialists develop the interlocking design for a particular area and manually check for completeness and consistency. The interlocking is implemented in either software 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, ranging from editors to animators. In this paper we focus on exploiting model checking to automatically check the design with respect to safety. The main concerns of this technique are the problem size and the efficiency of available tools. We have investigated both of these problems: seeking to work with a minimal model of the interlocking design and to improve efficiency of the model-checking process by exploiting domain knowledge of our particular application.

Cite as: Winter, K., Johnston, W., Robinson, P., Strooper, P. and van den Berg, L. (2005). Tool Support for Checking Railway Interlocking Designs. In Proc. Tenth Australian Workshop on Safety-Related Programmable Systems (SCS 2005), Sydney, Australia. CRPIT, 55. Cant, T., Ed. ACS. 101-107.

(from crpit.com) (local if available)