Speaker
Description
Reliable particle accelerators require reliable control systems to operate and protect the different subsystems of the accelerator. The software reliability of these critical control systems is crucial to guarantee a safe and optimal operation.
Software reliability is a very challenging aspect of the overall reliability analysis. Formal methods and formal verification are well-proven techniques to verify that critical software components meet the specification requirements. These techniques are very popular in critical industries like aeronautics or aerospace, however less common in the particle accelerators domain.
At CERN, we have developed an open-source tool, called PLCverif (www.cern.ch/plcverif), which allows to apply model checking (a formal verification technique) to PLC (Programmable Logic Controller) programs. PLCs are one of the most popular control devices in the process industry and therefore we can find many of them in the industrial facilities of particle accelerators (e.g. access control systems, cryogenics plants, cooling and ventilation systems, etc.).
PLCverif has been applied to many critical PLC programs at CERN and other international organizations and companies from the private sector.
This presentation discusses about the benefits and challenges of using formal methods and formal verification. It shows how PLCverif improves the reliability of the PLC programs of the accelerators subsystems. Finally, it concludes by presenting some of the results of real-life use cases at CERN.
