Driving Efficiency & Resilience to Human Error: SafeCap Automated Verification of Signalling Data

Conference Day Two
session Human Factors

Lead author: Dominic Taylor
Co authors: Alexei Iliasov, Alexander Romanovsky, Karl King

Resilience to human error is a fundamental requirement of any signalling system: signalling interlockings were first deployed to provide resilience against signaller error. The move to relay and then computer based interlockings has progressively expanded the role of interlockings to automate, once manual, actions performed by signallers. As a result of this and the increasing functionality of today’s interlockings, resilience against designer error is essential to prevent errors in commissioned interlockings instigating unsafe signalling states. This resilience is becoming increasingly hard to achieve owing to the increasing complexity of computer based interlockings.
Computer science formal methods offers a solution. Already well established for safety critical software development in a range of industries, formal methods are mathematical techniques for automatically proving that complex systems comply with key safety requirements. Whereas earlier attempts to apply formal methods to signalling interlockings have struggled with limited scalability and high upfront costs before benefits can be realised, SafeCap offers an alternative approach. By working within existing signalling design processes and using the highly scalable ‘symbolic theorem proving’ approach to formal verification, SafeCap provides a demonstrably practical way to realise the benefits of formal verification with minimal upfront costs.