JACoW logo

Journals of Accelerator Conferences Website (JACoW)

'Journal of Accelerator Conferences Website' (JACoW) is a publisher in Geneva, Switzerland that publishes the proceedings of accelerator conferences held around the world by an international collaboration of editors.

Title Applying Model Checking to Highly-Configurable Safety Critical Software: The SPS-PPS PLC Program
  • B. Fernández Adiego, E. Blanco Viñuela, F. Havart, T. Ladzinski, I.D. Lopez-Miguel, J-C. Tournier
    CERN, Geneva, Switzerland
Abstract 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.
Paper download WEPV042.PDF [0.178 MB / 5 pages]
Poster download WEPV042_POSTER.PDF [1.880 MB]
Cite download ※ BibTeX LaTeXText/WordRISEndNote
Conference ICALEPCS2021
Series International Conference on Accelerator and Large Experimental Physics Control Systems (18th)
Location Shanghai, China
Date 14-22 October 2021
Publisher JACoW Publishing, Geneva, Switzerland
Editorial Board Kazuro Furukawa (KEK, Tsukuba, Japan); Yingbing Yan (SARI,Shanghai, China); Yongbin Leng (SARI,Shanghai, China); Zhichu Chen (SARI,Shanghai, China); Volker RW Schaa (GSI, Darmstadt, Germany)
Online ISBN 978-3-95450-221-9
Online ISSN 2226-0358
Received 07 October 2021
Accepted 21 November 2021
Issue Date 08 March 2022
DOI doi:10.18429/JACoW-ICALEPCS2021-WEPV042
Pages 759-763
Creative Commons CC logoPublished by JACoW Publishing under the terms of the Creative Commons Attribution 3.0 International license. Any further distribution of this work must maintain attribution to the author(s), the published article's title, publisher, and DOI.