ICALEPCS2021 - List of Authors (Tournier, J-C.)

Paper	Title	Page
MOPV017	CERN SCADA Systems 2020 Large Upgrade Campaign Retrospective	156
	L.G. Goralczyk, A.F. Kostopoulos, B. Schofield, J-C. Tournier CERN, Geneva, Switzerland
	In this paper we report the experience from a large-scale upgrade campaign of SCADA control systems performed during the second LHC Long Shutdown at CERN. Such periodical upgrades are dictated by the ever evolving SCADA WinCC OA system and the CERN frameworks evolution used in those control systems. These upgrades concern: accelerator control systems, e.g. quench protection system, powering interlocks, magnet alignment; control systems devoted to accelerator facilities such as cryogenics, vacuum, gas… and other global technical infrastructure systems as well as the CERN electrical distribution system. Since there are more than 200 SCADA projects covering the CERN accelerator complex and technical infrastructure, any disruption requires careful coordination, planning and execution with process owners. Having gained experience from previous campaigns and reaching a new level of automation we were able to make visible improvements by shortening the required time and reducing the personnel required. Activities, lessons learned and further improvements are presented as well as a comprehensive statistical insight of the whole campaign.
	Poster MOPV017 [4.222 MB]
DOI •	reference for this paper ※ https://doi.org/10.18429/JACoW-ICALEPCS2021-MOPV017
About •	Received ※ 09 October 2021 Revised ※ 14 October 2021 Accepted ※ 04 November 2021 Issue date ※ 18 November 2021
Cite •	reference for this paper using ※ BibTeX, ※ LaTeX, ※ Text/Word, ※ RIS, ※ EndNote (xml)

MOPV042	PLCverif: Status of a Formal Verification Tool for Programmable Logic Controller	248
	J-C. Tournier, B. Fernández Adiego, I.D. Lopez-Miguel CERN, Geneva, Switzerland
	Programmable Logic Controllers (PLC) are widely used for industrial automation including safety systems at CERN. The incorrect behaviour of the PLC control system logic can cause significant financial losses by damage of property or the environment or even injuries in some cases, therefore ensuring their correct behaviour is essential. While testing has been for many years the traditional way of validating the PLC control system logic, CERN developed a model checking platform to go one step further and formally verify PLC logic. This platform, called PLCverif, first released internally for CERN usage in 2019, is now available to anyone since September 2020 via an open source licence. In this paper, we will first give an overview of the PLCverif platform capabilities before focusing on the improvements done since 2019 such as the larger support coverage of the Siemens PLC programming languages, the better support of the C Bounded Model Checker backend (CBMC) and the process of releasing PLCverif as an open-source software.
DOI •	reference for this paper ※ https://doi.org/10.18429/JACoW-ICALEPCS2021-MOPV042
About •	Received ※ 07 October 2021 Revised ※ 20 October 2021 Accepted ※ 21 December 2021 Issue date ※ 23 February 2022
Cite •	reference for this paper using ※ BibTeX, ※ LaTeX, ※ Text/Word, ※ RIS, ※ EndNote (xml)

WEPV042	Applying Model Checking to Highly-Configurable Safety Critical Software: The SPS-PPS PLC Program	759
	B. Fernández Adiego, E. Blanco Viñuela, F. Havart, T. Ladzinski, I.D. Lopez-Miguel, J-C. Tournier CERN, Geneva, Switzerland
	An important aspect of many particle accelerators is the constant evolution and frequent configuration changes that are needed to perform the experiments they are designed for. This often leads to the design of configurable software that can absorb these changes and perform the required control and protection actions. This design strategy minimizes the engineering and maintenance costs, but it makes the software verification activities more challenging since safety properties must be guaranteed for any of the possible configurations. Software model checking is a popular automated verification technique in many industries. This verification method explores all possible combinations of the system model to guarantee its compliance with certain properties or specification. This is a very appropriate technique for highly configurable software, since there is usually an enormous amount of combinations to be checked. This paper presents how PLCverif, a CERN model checking platform, has been applied to a highly configurable Programmable Logic Controller (PLC) program, the SPS Personnel Protection System (PPS). The benefits and challenges of this verification approach are also discussed.
	Poster WEPV042 [1.880 MB]
DOI •	reference for this paper ※ https://doi.org/10.18429/JACoW-ICALEPCS2021-WEPV042
About •	Received ※ 07 October 2021 Accepted ※ 21 November 2021 Issue date ※ 25 December 2021
Cite •	reference for this paper using ※ BibTeX, ※ LaTeX, ※ Text/Word, ※ RIS, ※ EndNote (xml)

Paper

Title

Page

CERN SCADA Systems 2020 Large Upgrade Campaign Retrospective

156

L.G. Goralczyk, A.F. Kostopoulos, B. Schofield, J-C. Tournier
CERN, Geneva, Switzerland

In this paper we report the experience from a large-scale upgrade campaign of SCADA control systems performed during the second LHC Long Shutdown at CERN. Such periodical upgrades are dictated by the ever evolving SCADA WinCC OA system and the CERN frameworks evolution used in those control systems. These upgrades concern: accelerator control systems, e.g. quench protection system, powering interlocks, magnet alignment; control systems devoted to accelerator facilities such as cryogenics, vacuum, gas… and other global technical infrastructure systems as well as the CERN electrical distribution system. Since there are more than 200 SCADA projects covering the CERN accelerator complex and technical infrastructure, any disruption requires careful coordination, planning and execution with process owners. Having gained experience from previous campaigns and reaching a new level of automation we were able to make visible improvements by shortening the required time and reducing the personnel required. Activities, lessons learned and further improvements are presented as well as a comprehensive statistical insight of the whole campaign.

Poster MOPV017 [4.222 MB]

DOI •

reference for this paper ※ https://doi.org/10.18429/JACoW-ICALEPCS2021-MOPV017

About •

Received ※ 09 October 2021 Revised ※ 14 October 2021 Accepted ※ 04 November 2021 Issue date ※ 18 November 2021

Cite •

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

MOPV042

PLCverif: Status of a Formal Verification Tool for Programmable Logic Controller

248

J-C. Tournier, B. Fernández Adiego, I.D. Lopez-Miguel
CERN, Geneva, Switzerland

Programmable Logic Controllers (PLC) are widely used for industrial automation including safety systems at CERN. The incorrect behaviour of the PLC control system logic can cause significant financial losses by damage of property or the environment or even injuries in some cases, therefore ensuring their correct behaviour is essential. While testing has been for many years the traditional way of validating the PLC control system logic, CERN developed a model checking platform to go one step further and formally verify PLC logic. This platform, called PLCverif, first released internally for CERN usage in 2019, is now available to anyone since September 2020 via an open source licence. In this paper, we will first give an overview of the PLCverif platform capabilities before focusing on the improvements done since 2019 such as the larger support coverage of the Siemens PLC programming languages, the better support of the C Bounded Model Checker backend (CBMC) and the process of releasing PLCverif as an open-source software.

DOI •

reference for this paper ※ https://doi.org/10.18429/JACoW-ICALEPCS2021-MOPV042

About •

Received ※ 07 October 2021 Revised ※ 20 October 2021 Accepted ※ 21 December 2021 Issue date ※ 23 February 2022

Cite •

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

WEPV042

Applying Model Checking to Highly-Configurable Safety Critical Software: The SPS-PPS PLC Program

759

B. Fernández Adiego, E. Blanco Viñuela, F. Havart, T. Ladzinski, I.D. Lopez-Miguel, J-C. Tournier
CERN, Geneva, Switzerland

An important aspect of many particle accelerators is the constant evolution and frequent configuration changes that are needed to perform the experiments they are designed for. This often leads to the design of configurable software that can absorb these changes and perform the required control and protection actions. This design strategy minimizes the engineering and maintenance costs, but it makes the software verification activities more challenging since safety properties must be guaranteed for any of the possible configurations. Software model checking is a popular automated verification technique in many industries. This verification method explores all possible combinations of the system model to guarantee its compliance with certain properties or specification. This is a very appropriate technique for highly configurable software, since there is usually an enormous amount of combinations to be checked. This paper presents how PLCverif, a CERN model checking platform, has been applied to a highly configurable Programmable Logic Controller (PLC) program, the SPS Personnel Protection System (PPS). The benefits and challenges of this verification approach are also discussed.

Poster WEPV042 [1.880 MB]

DOI •

reference for this paper ※ https://doi.org/10.18429/JACoW-ICALEPCS2021-WEPV042

About •

Received ※ 07 October 2021 Accepted ※ 21 November 2021 Issue date ※ 25 December 2021

Cite •

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