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

• URL: http://arxiv.org/abs/2502.19150v1
• Date: Wed, 26 Feb 2025 14:08:58 GMT
• Title: Formal Verification of PLCs as a Service: A CERN-GSI Safety-Critical Case Study (extended version)
• Authors: Ignacio D. Lopez-Miguel, Borja Fernández Adiego, Matias Salinas, Christine Betz,
• Abstract summary: This paper introduces a formal verification service for PLC (programmable logic controller) programs compliant with functional safety standards.<n>It offers a cost-effective solution to meet the rising demands for formal verification processes.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• Multi-Stage Retrieval for Operational Technology Cybersecurity Compliance Using Large Language Models: A Railway Casestudy [1.1010026679581653]
  This paper proposes a novel system that leverages Large Language Models (LLMs) and multi-stage retrieval to enhance the compliance verification process. We first evaluate a Baseline Compliance Architecture (BCA) for answering OTCS compliance queries, then develop an extended approach called Parallel Compliance Architecture (PCA) We demonstrate that the PCA significantly improves both correctness and reasoning quality in compliance verification.
  arXiv  Detail & Related papers  (2025-04-18T19:24:17Z)
• Qualitative Analysis for Validating IEC 62443-4-2 Requirements in DevSecOps [0.8874671354802572]
  This paper focuses on the automated validation of ISA/ IEC 62443-4-2 standard component requirements. Our analysis demonstrates the coverage established by the currently available tools and sheds light on current gaps to achieve full automation.
  arXiv  Detail & Related papers  (2023-10-13T10:24:58Z)
• Klever: Verification Framework for Critical Industrial C Programs [0.0]
  We present the Klever software verification framework, designed to reduce the effort of applying automatic software verification tools to large and critical industrial C programs. Existing tools do not provide widely adopted means for environment modeling, specification of requirements, verification of many versions and configurations of target programs, and expert assessment of verification results.
  arXiv  Detail & Related papers  (2023-09-28T13:23:59Z)
• A General Framework for Verification and Control of Dynamical Models via Certificate Synthesis [54.959571890098786]
  We provide a framework to encode system specifications and define corresponding certificates. We present an automated approach to formally synthesise controllers and certificates. Our approach contributes to the broad field of safe learning for control, exploiting the flexibility of neural networks.
  arXiv  Detail & Related papers  (2023-09-12T09:37:26Z)
• Rethinking Certification for Trustworthy Machine Learning-Based Applications [3.886429361348165]
  Machine Learning (ML) is increasingly used to implement advanced applications with non-deterministic behavior. Existing certification schemes are not immediately applicable to non-deterministic applications built on ML models. This article analyzes the challenges and deficiencies of current certification schemes, discusses open research issues, and proposes a first certification scheme for ML-based applications.
  arXiv  Detail & Related papers  (2023-05-26T11:06:28Z)
• Recursively Feasible Probabilistic Safe Online Learning with Control Barrier Functions [60.26921219698514]
  We introduce a model-uncertainty-aware reformulation of CBF-based safety-critical controllers. We then present the pointwise feasibility conditions of the resulting safety controller. We use these conditions to devise an event-triggered online data collection strategy.
  arXiv  Detail & Related papers  (2022-08-23T05:02:09Z)
• Joint Differentiable Optimization and Verification for Certified Reinforcement Learning [91.93635157885055]
  In model-based reinforcement learning for safety-critical control systems, it is important to formally certify system properties. We propose a framework that jointly conducts reinforcement learning and formal verification.
  arXiv  Detail & Related papers  (2022-01-28T16:53:56Z)
• Pointwise Feasibility of Gaussian Process-based Safety-Critical Control under Model Uncertainty [77.18483084440182]
  Control Barrier Functions (CBFs) and Control Lyapunov Functions (CLFs) are popular tools for enforcing safety and stability of a controlled system, respectively. We present a Gaussian Process (GP)-based approach to tackle the problem of model uncertainty in safety-critical controllers that use CBFs and CLFs.
  arXiv  Detail & Related papers  (2021-06-13T23:08:49Z)
• Evaluating the Safety of Deep Reinforcement Learning Models using Semi-Formal Verification [81.32981236437395]
  We present a semi-formal verification approach for decision-making tasks based on interval analysis. Our method obtains comparable results over standard benchmarks with respect to formal verifiers. Our approach allows to efficiently evaluate safety properties for decision-making models in practical applications.
  arXiv  Detail & Related papers  (2020-10-19T11:18:06Z)
• A Survey of Algorithms for Black-Box Safety Validation of Cyber-Physical Systems [30.638615396429536]
  Motivated by the prevalence of safety-critical artificial intelligence, this work provides a survey of state-of-the-art safety validation techniques for CPS. We present and discuss algorithms in the domains of optimization, path planning, reinforcement learning, and importance sampling. A brief overview of safety-critical applications is given, including autonomous vehicles and aircraft collision avoidance systems.
  arXiv  Detail & Related papers  (2020-05-06T17:31:51Z)
• Certified Reinforcement Learning with Logic Guidance [78.2286146954051]
  We propose a model-free RL algorithm that enables the use of Linear Temporal Logic (LTL) to formulate a goal for unknown continuous-state/action Markov Decision Processes (MDPs) The algorithm is guaranteed to synthesise a control policy whose traces satisfy the specification with maximal probability.
  arXiv  Detail & Related papers  (2019-02-02T20:09:32Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.