SigLink Project - Verification of Large-Scale Railway Interlockings

Contributors:

Paul Strooper, Kirsten Winter, Peter Robinson, Wendy Johnston, Lionel van den Berg
(See the team)

Description:

This project, jointly funded by Queensland Rail (QR) and an Arc Linkage Grant, is investigating The verification of tabular specifications called Control Tables produced by QR that define the safety and operational requirements for Railway Interlockings. Errors in these Control Tables can be extremely expensive to fix, particularly when discovered late in the signalling project life-cycle. During the SigTools project a model-checking approach was developed for checking Control Tables against safety properties. However, the approach is currently only suitable for application to less than 10% of the interlockings on the QR network, and can only check simple safety properties. This project proposes to optimise and extend the model checking so that it can be applied to most of the interlockings on the QR network, and check complex safety properties.

A complication of model checking is that the models used are not easily understandable to the target users of the tool. Therefore, another key challenge is to integrate the model checker into a verification environment that allows users to test the model in a graphical tool and to play back counter-examples from the model checker possibly through an animator.

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 Critical Systems and Software (SCS 2005), Sydney, Australia. CRPIT, 55. Cant, T., Ed. ACS. 101-107.
W. Johnston, K. Winter, L. van den Berg, P. Strooper, P. Robinson, Model-based Variable and Transition Orderings for efficient Symbolic Model Checking, In J. Misra, T. Nipkow, E. Sekerinski, editors, 14th International Symposium on Formal Methods (FM 2006) volume 4085 of Lecture Notes in Computer Science, pages 524 - 540. Springer-Verlag, 2006. (electronically available at Springer)
L. van den Berg, P. Strooper, W. Johnston, An Automated Approach for the Interpretation of Counter-Examples, 1st Workshop on Verification and Debugging, Seattle, August 21, 2006.
L. van den Berg and P. Strooper and K. Winter, Introducing Time in an Industrial Application of Model Checking, In Proc. of 12th Int. ERCIM Workshop on Formal Methods for Industrial Critical Systems (FMICS'07) , volume 4916 of Lecture Notes in Computer Science, pages 56-67. Springer-Verlag, 2008.