JACoW logo

Joint Accelerator Conferences Website

The Joint Accelerator Conferences Website (JACoW) is an international collaboration that publishes the proceedings of accelerator conferences held around the world.

Title PLCverif Re-engineered: An Open Platform for the Formal Analysis of PLC Programs
  • E. Blanco Viñuela, D. Darvas
    CERN, Geneva, Switzerland
  • V. Molnár
    BUTE, Budapest, Hungary
Abstract Programmable Logic Controllers (PLC) are widely used for industrial automation in industry and at CERN. The reliability of PLC software is crucial, but typically only testing is used to validate it. Our work targets the use of formal verification in practical ways for many years, which showed that it can be beneficial and practically applicable to various PLC programs. In this paper, we present PLCverif, our platform for formal analysis of PLC programs which has largely enhanced the quality of the deployed PLC software. By re-engineering the previous internal prototype tool, we built PLCverif to be an open, extensible platform that can be used not only for CERN’s specific PLC programs. PLCverif is licensed under an open source license, allowing the interested parties to use and extend it.
Paper download MOBPP01.PDF [0.430 MB / 7 pages]
Slides download MOBPP01_TALK.PDF [5.586 MB]
Export download ※ BibTeX LaTeXText/WordRISEndNote
Conference ICALEPCS2019
Series International Conference on Accelerator and Large Experimental Physics Control Systems (17th)
Location New York, NY, USA
Date 05-11 October 2019
Publisher JACoW Publishing, Geneva, Switzerland
Editorial Board Karen S. White (ORNL, Oak Ridge, TN, USA); Kevin A. Brown (BNL, Upton, NY, USA); Philip S. Dyer (BNL, Upton, NY, USA); Volker RW Schaa (GSI, Darmstadt, Germany)
Online ISBN 978-3-95450-209-7
Online ISSN 2226-0358
Received 27 September 2019
Accepted 09 October 2019
Issue Date 30 August 2020
DOI doi:10.18429/JACoW-ICALEPCS2019-MOBPP01
Pages 21-27
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.