Applying Model Checking to Critical PLC Applications: An ITER Case Study

Fernández Adiego, Borja; Avinashkrishna, Bhimavarapu; Blanco Viñuela, Enrique; Darvas, DÃ¡niel; Gaikwad, Yogesh; Lee, Gisik; Pedica, Riccardo; Prieto Diaz, Ignacio; Sallai, Gyula; Sreekuttan, Sailaraj

doi:10.18429/JACoW-ICALEPCS2017-THPHA161

Joint Accelerator Conferences Website

The Joint Accelerator Conferences Website (JACoW) is an international collaboration that publishes the proceedings of accelerator conferences held around the world.

RIS citation export for THPHA161: Applying Model Checking to Critical PLC Applications: An ITER Case Study

TY - CONF
AU - Fernández Adiego, B.
AU - Avinashkrishna, B.
AU - Blanco Viñuela, E.
AU - Darvas, D.
AU - Gaikwad, Y.C.
AU - Lee, G.S.
AU - Pedica, R.
AU - Prieto Diaz, I.
AU - Sallai, Gy.
AU - Sreekuttan, S.
ED - Schaa, Volker RW
ED - Costa, Isidre
ED - FernÃ¡ndez, David
ED - Matilla, Ãscar
TI - Applying Model Checking to Critical PLC Applications: An ITER Case Study
J2 - Proc. of ICALEPCS2017, Barcelona, Spain, 8-13 October 2017
C1 - Barcelona, Spain
T2 - International Conference on Accelerator and Large Experimental Control Systems
T3 - 16
LA - english
AB - The development of critical systems requires the application of verification techniques in order to guarantee that the requirements are met in the system. Standards like IEC 61508 provide guidelines and recommend the use of formal methods for that purpose. The ITER Interlock Control System has been designed to protect the tokamak and its auxiliary systems from failures of the components or incorrect machine operation. ITER has developed a method to assure that some critical operator commands have been correctly received and executed in the PLC (Programmable Logic Controller). The implementation of the method in a PLC program is a critical part of the interlock system. A methodology designed at CERN has been applied to verify this PLC program. The methodology is the result of 5 years of research in the applicability of model checking to PLC programs. A proof-of-concept tool called PLCverif implements this methodology. This paper presents the challenges and results of the ongoing collaboration between CERN and ITER on formal verification of critical PLC programs.
PB - JACoW
CP - Geneva, Switzerland
SP - 1792
EP - 1796
KW - ion
KW - PLC
KW - SCADA
KW - controls
KW - software
DA - 2018/01
PY - 2018
SN - 978-3-95450-193-9
DO - 10.18429/JACoW-ICALEPCS2017-THPHA161
UR - http://jacow.org/icalepcs2017/papers/thpha161.pdf
ER -