JACoW is a publisher in Geneva, Switzerland that publishes the proceedings of accelerator conferences held around the world by an international collaboration of editors.
@inproceedings{lopez-miguel:icalepcs2023-tupdp001,
author = {I.D. Lopez-Miguel and C. Betz and E. Blanco Viñuela and B. Fernández Adiego and M. Salinas},
title = {{Working Together for Safer Systems: A Collaboration Model for Verification of PLC Code}},
% booktitle = {Proc. ICALEPCS'23},
booktitle = {Proc. 19th Int. Conf. Accel. Large Exp. Phys. Control Syst. (ICALEPCS'23)},
eventdate = {2023-10-09/2023-10-13},
pages = {467--472},
paper = {TUPDP001},
language = {english},
keywords = {PLC, software, controls, operation, GUI},
venue = {Cape Town, South Africa},
series = {International Conference on Accelerator and Large Experimental Physics Control Systems},
number = {19},
publisher = {JACoW Publishing, Geneva, Switzerland},
month = {02},
year = {2024},
issn = {2226-0358},
isbn = {978-3-95450-238-7},
doi = {10.18429/JACoW-ICALEPCS2023-TUPDP001},
url = {https://jacow.org/icalepcs2023/papers/tupdp001.pdf},
abstract = {{Formal verification techniques are widely used in critical industries to minimize software flaws. However, despite the benefits and recommendations of the functional safety standards, such as IEC 61508 and IEC 61511, formal verification is not yet a common practice in the process industry and large scientific installations. This is mainly due to its complexity and the need for formal methods experts. At CERN, the PLCverif tool was developed to verify PLC programs formally. Although PLCverif hides most of the complexity of using formal methods and removes barriers to formally verifying PLC programs, engineers trying to verify their developments still encounter different obstacles. These challenges include the formalization of program specifications or the creation of formal models. This paper discusses how to overcome these obstacles by proposing a collaboration model that effectively allows the verification of critical PLC programs and promotes knowledge transfer between organizations. By providing a simpler and more accessible way to carry out formal verification, tools like PLCverif can play a crucial role in achieving this goal. The collaboration model splits the specification, development, and verification tasks between organizations. This approach is illustrated through a case study between GSI and CERN. }},
}