ICALEPCS2017 - List of Authors (Darvas, D.)

Paper	Title	Page
THPHA159	What is Special About PLC Software Model Checking?	1781
	D. Darvas, I. Majzik BUTE, Budapest, Hungary E. Blanco Viñuela CERN, Geneva, Switzerland
	Model checking is a formal verification technique to check given properties of models, designs or programs with mathematical precision. Due to its high knowledge and resource demand, the use of model checking is restricted mainly to core parts of highly critical systems. However, we and many other authors have argued that automated model checking of PLC programs is feasible and beneficial in practice. In this paper we aim to explain why model checking is applicable to PLC programs even though its use for software in general is too difficult. We present an overview of the particularities of PLC programs which influence the feasibility and complexity of their model checking. Furthermore, we list the main challenges in this domain and the solutions proposed in previous works.
	Poster THPHA159 [0.444 MB]
DOI •	reference for this paper ※ https://doi.org/10.18429/JACoW-ICALEPCS2017-THPHA159
Export •	reference for this paper using ※ BibTeX, ※ LaTeX, ※ Text/Word, ※ RIS, ※ EndNote (xml)

THPHA161	Applying Model Checking to Critical PLC Applications: An ITER Case Study	1792
	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
	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.
	Poster THPHA161 [0.457 MB]
DOI •	reference for this paper ※ https://doi.org/10.18429/JACoW-ICALEPCS2017-THPHA161
Export •	reference for this paper using ※ BibTeX, ※ LaTeX, ※ Text/Word, ※ RIS, ※ EndNote (xml)

Paper

Title

Page

What is Special About PLC Software Model Checking?

1781

D. Darvas, I. Majzik
BUTE, Budapest, Hungary
E. Blanco Viñuela
CERN, Geneva, Switzerland

Model checking is a formal verification technique to check given properties of models, designs or programs with mathematical precision. Due to its high knowledge and resource demand, the use of model checking is restricted mainly to core parts of highly critical systems. However, we and many other authors have argued that automated model checking of PLC programs is feasible and beneficial in practice. In this paper we aim to explain why model checking is applicable to PLC programs even though its use for software in general is too difficult. We present an overview of the particularities of PLC programs which influence the feasibility and complexity of their model checking. Furthermore, we list the main challenges in this domain and the solutions proposed in previous works.

Poster THPHA159 [0.444 MB]

DOI •

reference for this paper ※ https://doi.org/10.18429/JACoW-ICALEPCS2017-THPHA159

Export •

reference for this paper using ※ BibTeX, ※ LaTeX, ※ Text/Word, ※ RIS, ※ EndNote (xml)

THPHA161

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

1792

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

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.

Poster THPHA161 [0.457 MB]

DOI •

reference for this paper ※ https://doi.org/10.18429/JACoW-ICALEPCS2017-THPHA161

Export •

reference for this paper using ※ BibTeX, ※ LaTeX, ※ Text/Word, ※ RIS, ※ EndNote (xml)