Practical Verification of Railway Signalling Programs

This is the authors' abstract. We don't add key points for this paper.

SafeCap is a modern toolkit for modelling, simulation and formal verification of railway networks. This paper discusses the use of SafeCap for formal analysis and automated scalable safety verification of solid state interlocking (SSI) programs – a technology at the heart of many railway signalling solutions around the world. The main driving force behind SafeCap development was to make it easy for signalling engineers to use the technology and thus to ensure its smooth industrial deployment. The unique qualities and the novelty of SafeCap are in making the use of formal notations and proofs fully transparent for the engineers. In this paper we explain the formal foundations of the proposed method, its tool support, and its successful application by railway companies in developing industrial signalling projects.