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

Paper	Title	Page
TU2BCO02	Protection Layers Design for the High Luminosity LHC Full Remote Alignment System	285
	B. Fernández Adiego, E. Blanco Viñuela, A. Germinario, H. Mainaud Durand, M. Sosin CERN, Meyrin, Switzerland
	The Full Remote Alignment System (FRAS) is a complex measurement, alignment and control system designed to remotely align components of the Large Hadron Collider (LHC) following its High Luminosity upgrade. The purpose of FRAS is to guarantee optimal alignment of the strong focusing magnets and associated components near the experimental interaction points, while at the same time limiting the radiation dose to which surveyors in the LHC tunnel are subjected. A failure in the FRAS control system, or an operator mistake, could provoke a non desired displacement of a component that could lead to damage of neighbouring equipment. Such an incident would incur a considerable repair cost both in terms of money and time. To mitigate this possibility, an exhaustive risk analysis of FRAS has been performed, with the design of protection layers according to the IEC 61511 standard proposed. This paper presents the different functional safety techniques applied to FRAS, reports on the current project status, and introduces the future activities to complete the safety life cycle.
	Slides TU2BCO02 [2.757 MB]
DOI •	reference for this paper ※ doi:10.18429/JACoW-ICALEPCS2023-TU2BCO02
About •	Received ※ 03 October 2023 — Accepted ※ 14 December 2023 — Issued ※ 19 December 2023
Cite •	reference for this paper using ※ BibTeX, ※ LaTeX, ※ Text/Word, ※ RIS, ※ EndNote (xml)

TUPDP001	Working Together for Safer Systems: A Collaboration Model for Verification of PLC Code	467
	I.D. Lopez-Miguel IAP TUW, Wien, Austria C. Betz, M. Salinas GSI, Darmstadt, Germany E. Blanco Viñuela, B. Fernández Adiego CERN, Meyrin, Switzerland
	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.
	Poster TUPDP001 [0.744 MB]
DOI •	reference for this paper ※ doi:10.18429/JACoW-ICALEPCS2023-TUPDP001
About •	Received ※ 03 October 2023 — Accepted ※ 20 November 2023 — Issued ※ 19 December 2023
Cite •	reference for this paper using ※ BibTeX, ※ LaTeX, ※ Text/Word, ※ RIS, ※ EndNote (xml)

THPDP059	Towards Automatic Generation of Fail-Safe PLC Code Compliant with Functional Safety Standards	1449
	A. Germinario, E. Blanco Viñuela, B. Fernández Adiego CERN, Meyrin, Switzerland
	In agreement with the IEC 61511 functional safety standard, fail-safe application programs should be written using a Limited Variability Language (LVL), that has a limited number of operations and data types, such as LD (Ladder Diagrams) or FBD (Function Block Diagrams) for safety PLC (Programmable Logic Controller) languages. The specification of safety instrumented systems, as part of the Safety Requirements Specification document, shall unambiguously define the logic of the program, creating a one-to-one relationship between code and specification. Hence, coding becomes a translation from a specification language to PLC code. This process is repetitive and error-prone when performed by a human. In this paper we describe the process of fully generating Siemens TIA portal LD programs for safety applications from a formal specification. The process starts by generating an intermediate model that represents a generic LD program based on a predefined meta-model. This intermediate model is then automatically translated into code. The idea can be expanded to other equivalent LVL languages from other PLC manufacturers. In addition, the intermediate model can be generated from different specification formalisms having the same level of expressiveness as the one presented in this paper: a Cause-Effect Matrix. Our medium-term vision is to automatically generate fail-safe programs from diverse formal specification methods and using different LVLs.
	Poster THPDP059 [1.935 MB]
DOI •	reference for this paper ※ doi:10.18429/JACoW-ICALEPCS2023-THPDP059
About •	Received ※ 03 October 2023 — Revised ※ 26 October 2023 — Accepted ※ 08 December 2023 — Issued ※ 09 December 2023
Cite •	reference for this paper using ※ BibTeX, ※ LaTeX, ※ Text/Word, ※ RIS, ※ EndNote (xml)

Paper

Title

Page

Protection Layers Design for the High Luminosity LHC Full Remote Alignment System

285

B. Fernández Adiego, E. Blanco Viñuela, A. Germinario, H. Mainaud Durand, M. Sosin
CERN, Meyrin, Switzerland

The Full Remote Alignment System (FRAS) is a complex measurement, alignment and control system designed to remotely align components of the Large Hadron Collider (LHC) following its High Luminosity upgrade. The purpose of FRAS is to guarantee optimal alignment of the strong focusing magnets and associated components near the experimental interaction points, while at the same time limiting the radiation dose to which surveyors in the LHC tunnel are subjected. A failure in the FRAS control system, or an operator mistake, could provoke a non desired displacement of a component that could lead to damage of neighbouring equipment. Such an incident would incur a considerable repair cost both in terms of money and time. To mitigate this possibility, an exhaustive risk analysis of FRAS has been performed, with the design of protection layers according to the IEC 61511 standard proposed. This paper presents the different functional safety techniques applied to FRAS, reports on the current project status, and introduces the future activities to complete the safety life cycle.

Slides TU2BCO02 [2.757 MB]

DOI •

reference for this paper ※ doi:10.18429/JACoW-ICALEPCS2023-TU2BCO02

About •

Received ※ 03 October 2023 — Accepted ※ 14 December 2023 — Issued ※ 19 December 2023

Cite •

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

TUPDP001

Working Together for Safer Systems: A Collaboration Model for Verification of PLC Code

467

I.D. Lopez-Miguel
IAP TUW, Wien, Austria
C. Betz, M. Salinas
GSI, Darmstadt, Germany
E. Blanco Viñuela, B. Fernández Adiego
CERN, Meyrin, Switzerland

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.

Poster TUPDP001 [0.744 MB]

DOI •

reference for this paper ※ doi:10.18429/JACoW-ICALEPCS2023-TUPDP001

About •

Received ※ 03 October 2023 — Accepted ※ 20 November 2023 — Issued ※ 19 December 2023

Cite •

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

THPDP059

Towards Automatic Generation of Fail-Safe PLC Code Compliant with Functional Safety Standards

1449

A. Germinario, E. Blanco Viñuela, B. Fernández Adiego
CERN, Meyrin, Switzerland

In agreement with the IEC 61511 functional safety standard, fail-safe application programs should be written using a Limited Variability Language (LVL), that has a limited number of operations and data types, such as LD (Ladder Diagrams) or FBD (Function Block Diagrams) for safety PLC (Programmable Logic Controller) languages. The specification of safety instrumented systems, as part of the Safety Requirements Specification document, shall unambiguously define the logic of the program, creating a one-to-one relationship between code and specification. Hence, coding becomes a translation from a specification language to PLC code. This process is repetitive and error-prone when performed by a human. In this paper we describe the process of fully generating Siemens TIA portal LD programs for safety applications from a formal specification. The process starts by generating an intermediate model that represents a generic LD program based on a predefined meta-model. This intermediate model is then automatically translated into code. The idea can be expanded to other equivalent LVL languages from other PLC manufacturers. In addition, the intermediate model can be generated from different specification formalisms having the same level of expressiveness as the one presented in this paper: a Cause-Effect Matrix. Our medium-term vision is to automatically generate fail-safe programs from diverse formal specification methods and using different LVLs.

Poster THPDP059 [1.935 MB]

DOI •

reference for this paper ※ doi:10.18429/JACoW-ICALEPCS2023-THPDP059

About •

Received ※ 03 October 2023 — Revised ※ 26 October 2023 — Accepted ※ 08 December 2023 — Issued ※ 09 December 2023

Cite •

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