Model checking railway interlocking systems

摘要

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 checker 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.