PLC 形式化验证即服务：来自 CERN-GSI 安全关键场景的案例研究（扩展版）
软件工程
2025-02-27 v1 计算机科学中的逻辑
摘要
技术复杂性的增加和对软件可靠性的需求要求组织进行形式化设计和验证其安全关键程序，以最小化系统性故障。形式化方法被功能安全标准推荐（例如 IEC 61511 用于过程工业，IEC 61508 用于通用标准），在其中发挥着关键作用。其结构化方法减少了系统需求的歧义，促进了早期错误检测。本文介绍了一种针对符合功能安全标准的 PLC（可编程逻辑控制器）程序的形式化验证服务，为组织提供外部专业知识，同时消除需进行大量内部培训的需求。它提供了一种成本效益高的解决方案，以满足日益增长的形式化验证需求。该方法扩展包括建模时间依赖、受知识产权保护的组件，使其能够对真实的安全关键应用进行形式化验证。案例研究表明，CERN 在 GSI 粒子加速器设施的安全关键安装中提供的 PLC 形式化验证即服务的实际应用。
引用
@article{arxiv.2502.19150,
title = {Formal Verification of PLCs as a Service: A CERN-GSI Safety-Critical Case Study (extended version)},
author = {Ignacio D. Lopez-Miguel and Borja Fernández Adiego and Matias Salinas and Christine Betz},
journal= {arXiv preprint arXiv:2502.19150},
year = {2025}
}
备注
Extended version of NFM 2025 paper