Formal Verification of PLCs as a Service: A CERN-GSI Safety-Critical Case Study (extended version)

TL;DR

The paper addresses the need for reliable verification of safety-critical PLC software by offering formal verification as a service that leverages independent expert teams and formal specifications aligned with IEC safety standards. It introduces a collaboration model, formal specification techniques, and a verification workflow that combines simulation with PLCverif to handle time-dependent know-how-protected functions, demonstrated on a CERN-GSI case study. Key contributions include the three-way collaboration framework, formalization of requirements via CEM/I-O matrices/state machines, and the extension of PLCverif to cover additional protected functions, enabling verification of a complete safety-critical PAS PLC project. The results show early error detection, increased confidence for regulators, and a practical path for safety-critical organizations to adopt formal methods without extensive internal training; the work also outlines future automation toward correct-by-construction code generation and broader tooling support.

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.

Figures (20)

• Figure 1: Diagram with the roles of the collaboration, shared information and used tools.
• Figure 2: Example of a state machine.
• Figure 3: Example of a logic diagram.
• Figure 4: Proposed diagram to model a know-how-protected built-in function.
• Figure 5: Example of a timing diagram for a simplified version of the FDBACK function.