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)
|