Model Checking for Interlocking Safety
Andrew C. Simpson · 1998
We describe how the technique of model checking has been applied to the verification of geographic databases which are associated with Solid State Interlocking railway signalling systems. We represent such databases in terms of Communicating Sequential Processes (CSP) and verify their safety using the refinement checker FDR2. The approach to compositionality and refinement which is employed by CSP allows us to reduce the analysis of safety invariants for geographic databases to a number of small mechanical tests. Keywords: railways signalling, safety, model checking, CSP, refinement 1 Introduction Solid State Interlocking (SSI) railway signalling systems (see, for example, [Cri87]) control a large percentage of the railway networks of many countries, including Great Britain, Australia, Belgium, and South Africa. It is also in competition for use in other markets because of the ease with which its data language can be customised to generic programs with minimal maintenance. SSI is a c...