This video isn’t available to you right now
Login to check your access and watch the full session
About the session
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.
