TY  - CONF
AU  - Lopez-Miguel, Ignacio D.
AU  - Adiego, Borja Fernández
AU  - Salinas, Matias
AU  - Betz, Christine
A3  - Dutle, Aaron
A3  - Humphrey, Laura
A3  - Titolo, Laura
TI  - Formal Verification of PLCs as a Service: A CERN-GSI Safety-Critical Case Study
VL  - 15682
CY  - Cham
PB  - Springer Nature Switzerland
M1  - GSI-2026-00321
SN  - 978-3-031-93705-7 (print)
T2  - Lecture Notes in Computer Science
SP  - 227 - 235
PY  - 2025
AB  - The increased technological complexity and demand for software   reliability require organizations to formally design and verify their   safety-critical programs to minimize systematic failures. Formal methods   are recommended by functional safety standards (e.g., by IEC 61511 for   the process industry and by the generic IEC 61508) and play a crucial   role. Their structured approach reduces ambiguity in system   requirements, facilitating early error detection. This paper introduces   a formal verification service for PLC (programmable logic controller)   programs compliant with functional safety standards, providing external   expertise to organizations while eliminating the need for extensive   internal training. It offers a cost-effective solution to meet the   rising demands for formal verification processes. The approach is   extended to include modeling time-dependent, know-how-protected   components, enabling formal verification of real safety-critical   applications. A case study shows the application of PLC formal   verification as a service provided by CERN in a safety-critical   installation at the GSI particle accelerator facility.
T2  - 17th International Symposium on NASA Formal Methods-NFM, VA
CY  - 11 Jun 2025 - 13 Jun 2025, Virgina (usa)
Y2  - 11 Jun 2025 - 13 Jun 2025
M2  - Virgina, usa
LB  - PUB:(DE-HGF)8 ; PUB:(DE-HGF)7
DO  - DOI:10.1007/978-3-031-93706-4_13
UR  - https://repository.gsi.de/record/364952
ER  -