The increasing complexity of modern interlocking poses a major challenge to ensuring railway safety. This calls for application of formal methods for assurance and verification of their safety. We have developed an industry-strength toolset, called SafeCap, for formal verification of interlockings. Our aim was to overcome the main barriers in deploying formal methods in industry. The approach proposed verifies interlocking data developed by signalling engineers in the ways they are designed by industry. It ensures fully-automated verification of safety properties using the state of the art techniques (automated theorem provers and solvers), and provides diagnostics in terms of the notations used by engineers. In the last two years SafeCap has been successfully used to verify 26 real-world mainline interlockings, developed by different suppliers and design offices. SafeCap is currently used in an advisory capacity, supplementing manual checking and testing processes by providing an additional level of verification and enabling earlier identification of errors. We are now developing a safety case to support its use as an alternative to some of these activities.

翻译：现代联锁的日益复杂对确保铁路安全提出了重大挑战。这要求采用正式的保证和核查安全的方法。我们开发了一种工业强度工具,称为“SafeCap”,用于正式核查互锁。我们的目标是克服在工业中采用正式方法的主要障碍。拟议的方法以行业设计的方式核查信号工程师开发的相互连接的数据。它用最新技术(自动的Theorem验证器和解答器)确保对安全特性进行完全自动化的核查,并提供工程师使用的批注方面的诊断。过去两年中,“SafeCap”成功地用于核查由不同供应商和设计办公室开发的26个真实世界主线互闭装置。目前,在咨询能力中使用“SafeCap”补充了人工检查和测试过程,提供了更高水平的核查,并能够更早地查明错误。我们现在正在开发一个安全案例,以支持将其用作某些活动的替代办法。