Modelling Large Railway Interlockings and Model Checking Small Ones

Winter, K. and Robinson, N.J.

This paper describes the results to date of a feasibility study on model checking applied to railway interlockings. Our approach, in contrast to others, targets a high-level description of interlocking systems, namely the logical view of its operation. The result is a formal model that can be discussed with and validated by our industry partners and, moreover, provides a formal semantics for the notation that is used in practice. We suggest optimisations on the formal model and a decomposition technique for large railway layouts that is easy to apply. This renders oru approach feasible for use in industrial practice.

Cite as: Winter, K. and Robinson, N.J. (2003). Modelling Large Railway Interlockings and Model Checking Small Ones. In Proc. Twenty-Sixth Australasian Computer Science Conference (ACSC2003), Adelaide, Australia. CRPIT, 16. Oudshoorn, M. J., Ed. ACS. 309-316.

(from crpit.com) (local if available)