%0 Conference Paper
%A Lopez-Miguel, Ignacio D.
%A Adiego, Borja Fernández
%A Salinas, Matias
%A Betz, Christine
%Y Dutle, Aaron
%Y Humphrey, Laura
%Y Titolo, Laura
%T Formal Verification of PLCs as a Service: A CERN-GSI Safety-Critical Case Study
%V 15682
%C Cham
%I Springer Nature Switzerland
%M GSI-2026-00321
%@ 978-3-031-93705-7 (print)
%B Lecture Notes in Computer Science
%P 227 - 235
%D 2025
%< NASA Formal Methods / Dutle, Aaron (Editor) [https://orcid.org/0000-0002-8503-5514] ; Cham : Springer Nature Switzerland, 2025, Chapter 13 ; ISSN: 0302-9743=1611-3349 ; ISBN: 978-3-031-93705-7=978-3-031-93706-4 ; doi:10.1007/978-3-031-93706-4
%X 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.
%B 17th International Symposium on NASA Formal Methods-NFM, VA
%C 11 Jun 2025 - 13 Jun 2025, Virgina (usa)
Y2 11 Jun 2025 - 13 Jun 2025
M2 Virgina, usa
%F PUB:(DE-HGF)8 ; PUB:(DE-HGF)7
%9 Contribution to a conference proceedingsContribution to a book
%R 10.1007/978-3-031-93706-4_13
%U https://repository.gsi.de/record/364952