.png){kind=icon}
返回
Configurable Interlocking Verification
.png){kind=icon}
PRE
AI
DOI：10.1007/978-3-032-10762-6_16.png)
.png){kind=icon}
原文求助.png){kind=icon}
分享.png){kind=icon}
收藏
摘要
En 中文
本文探讨了在工业应用中精确界定形式化验证范围的挑战，以避免无意遗漏验证需求和重复验证。该文借鉴了我们在英国多个实际铁路信号项目中使用名为SafeCap的形式化验证技术的经验，以及我们目前正在开发的解决方案。SafeCap利用安全不变量（安全属性）通过专用的符号定理证明器对铁路联锁的现场特定配置进行形式化且全自动的安全验证。这种形式化验证的范围是现场特定联锁配置验证总体的一个子集，而后者本身又是信号系统验证总体的一个子集。在我们的工作中，还明显需要开发并实际使用不同（通常重叠）的属性集。这有多种原因：不同的铁路采用不同的安全标准，这些属性由此发展而来；标准本身也在演变；属性在工具持续改进过程中需要进行版本控制和变更管理。为此，本文提出了定义验证范围（称为方言）的想法，并提出了一种机制，将范围引入为一组带有唯一范围名称标记的验证属性。本文利用我们在部署SafeCap时面临的各种工业场景，展示了该机制如何在商业部署中发挥作用。
Keyword:
formal verification
railway signalling
safety invariants
verification scope
SafeCap
.png){kind=icon}
