Presenter
Xaver Fink
CERN
Authors
Xaver Fink, Borja Fernandez Adiego
Abstract
The CERN BE-ICS group is integrating formal methods into the engineering and validation of safety-relevant control systems for particle accelerators and their industrial installations. In this talk we cover our recent activities and ongoing real-world applications of formal verification for programmable logic controller (PLC) programs, neural network controllers, and industrial C++ code. For PLC program verification our group has invested substantial resources over the last decade to develop the PLCverif platform for model checking based PLC verification. We give an overview over the framework and share recent experience reports of applying it to CERN projects. On neural networks we present recent works and challenges: how to evaluate and verify robustness against perturbations under real-world conditions, and the challenge of verifying stability of neural-network based approximate MPC for closed-loop controls of industrial installations. Finally, we present early-stage work on applying model checking to C++ code for the validation of a critical control system.
Slides
TBA