Speaker
Description
Programmable Logic Controllers (PLC) are one of the most popular control devices used 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.).
A bug in a PLC program can have catastrophic consequences in terms of personnel safety, machine protection or even the availability of the particle accelerators. For that reason, it is essential to apply methods that improve the reliability of these PLC programs.
Model checking is a well-proven technique to verify that critical software components meet the specification requirements. Despite these techniques are very popular in critical industries like aeronautics or aerospace, they are not in the process industry and particle accelerators domain.
At CERN, we have developed an open-source tool, called PLCverif (www.cern.ch/plcverif), which allows to apply model checking to PLC programs. This poster presents the benefits of using model checking compared to the traditional testing techniques. It also introduces the PLCverif methodology and how it can improve the reliability of the PLC programs of the accelerators subsystems. Finally, it presents some of the results of real-life use cases at CERN.
