JACoW logo

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.

Title Applying Model Checking to Critical PLC Applications: An ITER Case Study
  • B. Fernández Adiego, E. Blanco Viñuela, D. Darvas
    CERN, Geneva, Switzerland
  • B. Avinashkrishna, Y.C. Gaikwad, S. Sreekuttan
    Tata Consultancy Services, Pune, India
  • G.S. Lee
    Mobiis Co., Ltd., Seoul, Republic of Korea
  • R. Pedica
    Vitrociset s.p.a, Roma, Italy
  • I. Prieto Diaz
    IBERINCO, Madrid, Spain
  • Gy. Sallai
    BUTE, Budapest, Hungary
Abstract 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.
Paper download THPHA161.PDF [0.161 MB / 5 pages]
Poster download THPHA161_POSTER.PDF [0.457 MB]
Export download ※ BibTeX LaTeXText/WordRISEndNote
Conference ICALEPCS2017, Barcelona, Spain
Series International Conference on Accelerator and Large Experimental Control Systems (16th)
Proceedings Link to full ICALEPCS2017 Proccedings
Session Poster Session
Date 12-Oct-17   16:45–19:00
Main Classification Software Technology Evolution
Keywords ion, PLC, SCADA, controls, software
Publisher JACoW, Geneva, Switzerland
Editors Volker RW Schaa (GSI, Darmstadt, Germany); Isidre Costa (ALBA-CELLS, Cerdanyola del Vallès, Spain); David Fernández (ALBA-CELLS, Cerdanyola del Vallès, Spain); Óscar Matilla (ALBA-CELLS, Cerdanyola del Vallès, Spain)
ISBN 978-3-95450-193-9
Published January 2018
Copyright © 2018 by JACoW, Geneva, Switzerland     CC-BY Creative Commons License
cc Creative Commons Attribution 3.0