Formal Verification of Railway Signalling - from Academia to Industry

Railway signalling is essential for the safe operation of trains.  Formal verification offers more rigorous and cost-effective demonstration of the safety of signalling logic than traditional manual checking.  However, making the transition from Academia to practical industrial application proved challenging.  SafeCap emerged as a practical, automated, and scalable approach to formal verification of signalling through collaboration between Academia and Industry.
This presentation provides an introduction to railway signalling, from the Steam Age to the Information Age, and to the Computer Science discipline of Formal Verification.  It tells the story of how SafeCap developed from initial prototype to trials with real-world data, approval for industrial application and thence to commercial verification of more than 75 signalling interlockings.  It explains how this experience also enriched the academic field of Computer Science Formal Verification, the benefits brought to Industry and the path to the end-goal of fully substituting traditional manual verification activities.