Please visit Jefferson Lab Event Policies and Guidance before planning your next event:

Oct 16 – 21, 2022
Marriott Newport News at City Center
US/Eastern timezone

PLCverif: a tool to formally verify critical PLC programs

Oct 18, 2022, 1:30 PM
1h 30m
Poster Poster Poster Session




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 (, 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.

Primary author

Presentation materials