Contribution to a conference proceedings/Contribution to a book

GSI-2026-00321

http://join2-wiki.gsi.de/foswiki/pub/Main/Artwork/join2_logo100x88.png Formal Verification of PLCs as a Service: A CERN-GSI Safety-Critical Case Study

Dutle, A. (Editor) ; Humphrey, L. (Editor) ; Titolo, L. (Editor) ; Lopez-Miguel, I. D. ; Adiego, B. F. ; Salinas, M.GSI* ; Betz, C.GSI*

2025
Springer Nature Switzerland Cham
ISBN: 978-3-031-93705-7 (print), 978-3-031-93706-4 (electronic)

Please use a persistent id in citations: doi:10.1007/978-3-031-93706-4_13

Abstract: 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.

---

Contributing Institute(s):

1. Accelerator Controls (ACO)

Research Program(s):

1. 6G14 - GSI-MU Ion Facilities (POF4-6G14) (POF4-6G14)

Experiment(s):

1. (Facility Altdaten therefore no facility)

---

Database coverage:
Nationallizenz ; SCOPUS

---