For supporting the analysis of railway interlocking systems in the early stage of their design we propose the use of model checking. We investigate the use of the formal modelling language CSP and the corresponding model check FDR. In this paper, we describe the basics of this formalism and introduce our formal model of a railway interlocking system. Checking this model against the given safety requirements, the signalling principles, we get useful counter-examples that help to debug the given interlocking design. This work provides a successful example of how formal methods can be used to support the industrial development process. |
| Cite as: Winter, K. (2002). Model Checking Railway Interlocking Systems. In Proc. Twenty-Fifth Australasian Computer Science Conference (ACSC2002), Melbourne, Australia. CRPIT, 4. Oudshoorn, M. J., Ed. ACS. 303-310. |
 (from crpit.com)
(local if available)
|