2025/02/26 by Ignacio D. Lopez-Miguel, Lopez-Miguel, Ignacio D., Borja Fernández Adiego +4 · 1 citation
Computer Science · Engineering · #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Petri Nets in System Modeling #Radiation Effects in Electronics #Safety Systems Engineering in Autonomy #Software Engineering (cs.SE)
paper · pdf · doi:10.48550/arxiv.2502.19150
openalex publication_date 2025/02/26 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.