Application of formal methods to critical control systems at CERN

CERN, the European Organization for Nuclear Research, is a leading international centre for particle physics research. This organization operates the world’s largest particle accelerator complex, enabling the experiments to answer fundamental questions about our universe. CERN relies on hundreds of control and safety systems to ensure the autonomous and reliable operation of its accelerator complex and industrial installations. Programmable Logic Controllers (PLCs) are one of the most extensively deployed control devices at CERN, playing a critical role in the automation, monitoring, and protection of industrial facilities such as cryogenics, gas handling systems, cooling and ventilation, as well as various safety-critical systems. Their robustness and deterministic behaviour make them a standard solution not only at CERN but also in other industries like nuclear power plants, chemical processing, pharmaceuticals, and advanced manufacturing. A flaw in a PLC program could have severe consequences for CERN, ranging from significant damage to accelerator equipment, resulting in substantial financial costs, to potentially compromising the safety of personnel and visitors. Over the past decade, CERN engineers have incorporated formal methods into the PLC development lifecycle to complement traditional testing techniques. In particular, model checking has become a key approach for verifying critical PLC programs against rigorously defined formal specifications. In this talk, we will present our methodology, implemented in the PLCverif tool, for applying formal methods and verification techniques to PLC programs—highlighting both the benefits and the practical challenges encountered in real-world scenarios. We will also outline our roadmap for addressing current limitations and extending formal verification to future control systems incorporating neural network architectures.

Borja Fernández Adiego

Last modified: Tue May 13 2025