工业级固态联锁程序验证
软件工程
2022-01-17 v2
摘要
现代联锁日益复杂，对确保铁路安全构成重大挑战。这要求应用形式化方法对其安全性进行保证与验证。我们开发了一套称为SafeCap的工业级工具集，用于联锁的形式化验证。我们的目标在于克服形式化方法在工业部署中的主要障碍。所提出的方法验证由信号工程师以工业界设计方式开发的联锁数据。它利用最先进技术（自动定理证明器与求解器）确保安全性性质的完全自动化验证，并以工程师所用符号提供诊断信息。在过去两年中，SafeCap已成功用于验证由不同供应商和设计办公室开发的26个真实世界干线联锁。SafeCap目前以咨询能力使用，补充人工检查与测试流程，提供额外验证层级并支持更早识别错误。我们现正开发安全论证，以支持其作为其中部分活动的替代方案。
引用
@article{arxiv.2108.10091,
title = {Industrial-Strength Verification of Solid State Interlocking Programs},
author = {Alexei Iliasov and Dominic Taylor and Linas Laibinis and Alexander Romanovsky},
journal= {arXiv preprint arXiv:2108.10091},
year = {2022}
}
备注
16 pages