ICALEPCS2017 - List of Authors (Fernandez Adiego, B.)

Paper	Title	Page
THCPA01	Safety Instrumented Systems and the AWAKE Plasma Control as a Use Case	1206
	E. Blanco Viñuela, H.F. Braunmuller, B. Fernández Adiego, R. Speroni CERN, Geneva, Switzerland
	Safety is likely the most critical concern in many process industries, yet there is a general uncertainty on the proper engineering to reduce the risks and ensure the safety of persons or material at the same time of providing the process control system. Some of the reasons for this misperception are unclear requirements, lack of functional safety engineering knowledge or incorrect protection functionalities attributed to the BPCS (Basic Process Control System). Occasionally the control engineers are not aware of the hazards inherent to an industrial process and this causes the lack of the right design of the overall controls. This paper illustrates the engineering of the SIS (Safety Instrumented System) and the BPCS of the plasma vapour controls of the AWAKE R&D project, the first proton-driven plasma wakefield acceleration experiment in the world. The controls design and implementation refers to the IEC61511/ISA84 standard, including technological choices, design, operation and maintenance. Finally, the publication reveals usual difficulties appearing in such kind of industrial installations and the actions to be done to ensure the proper functional safety system design.
	Slides THCPA01 [6.199 MB]
DOI •	reference for this paper ※ https://doi.org/10.18429/JACoW-ICALEPCS2017-THCPA01
Export •	reference for this paper using ※ BibTeX, ※ LaTeX, ※ Text/Word, ※ RIS, ※ EndNote (xml)

THPHA160	Experience With Static PLC Code Analysis at CERN	1787
	C. Tsiplaki Spiliopoulou, E. Blanco Viñuela, B. Fernández Adiego CERN, Geneva, Switzerland
	The large number of industrial control systems based on PLCs (Programmable Logic Controllers) available at CERN implies a huge number of programs and lines of code. The software quality assurance becomes a key point to ensure the reliability of the control systems. Static code analysis is a relatively easy-to-use, simple way to find potential faults or error-prone parts in the source code. While static code analysis is widely used for general purpose programming languages (e.g. Java, C), this is not the case for PLC programs. We have analyzed the possibilities and the gains to be expected from applying static analysis to the PLC code used at CERN, based on the UNICOS framework. This paper reports on our experience with the method and the available tools and sketches an outline for future work to make this analysis method practically applicable.
	Poster THPHA160 [0.555 MB]
DOI •	reference for this paper ※ https://doi.org/10.18429/JACoW-ICALEPCS2017-THPHA160
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

Safety Instrumented Systems and the AWAKE Plasma Control as a Use Case

1206

E. Blanco Viñuela, H.F. Braunmuller, B. Fernández Adiego, R. Speroni
CERN, Geneva, Switzerland

Safety is likely the most critical concern in many process industries, yet there is a general uncertainty on the proper engineering to reduce the risks and ensure the safety of persons or material at the same time of providing the process control system. Some of the reasons for this misperception are unclear requirements, lack of functional safety engineering knowledge or incorrect protection functionalities attributed to the BPCS (Basic Process Control System). Occasionally the control engineers are not aware of the hazards inherent to an industrial process and this causes the lack of the right design of the overall controls. This paper illustrates the engineering of the SIS (Safety Instrumented System) and the BPCS of the plasma vapour controls of the AWAKE R&D project, the first proton-driven plasma wakefield acceleration experiment in the world. The controls design and implementation refers to the IEC61511/ISA84 standard, including technological choices, design, operation and maintenance. Finally, the publication reveals usual difficulties appearing in such kind of industrial installations and the actions to be done to ensure the proper functional safety system design.

Slides THCPA01 [6.199 MB]

DOI •

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

Export •

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

THPHA160

Experience With Static PLC Code Analysis at CERN

1787

C. Tsiplaki Spiliopoulou, E. Blanco Viñuela, B. Fernández Adiego
CERN, Geneva, Switzerland

The large number of industrial control systems based on PLCs (Programmable Logic Controllers) available at CERN implies a huge number of programs and lines of code. The software quality assurance becomes a key point to ensure the reliability of the control systems. Static code analysis is a relatively easy-to-use, simple way to find potential faults or error-prone parts in the source code. While static code analysis is widely used for general purpose programming languages (e.g. Java, C), this is not the case for PLC programs. We have analyzed the possibilities and the gains to be expected from applying static analysis to the PLC code used at CERN, based on the UNICOS framework. This paper reports on our experience with the method and the available tools and sketches an outline for future work to make this analysis method practically applicable.

Poster THPHA160 [0.555 MB]

DOI •

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

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)