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 What is Special About PLC Software Model Checking?
  • D. Darvas, I. Majzik
    BUTE, Budapest, Hungary
  • E. Blanco Vinuelapresenter
    CERN, Geneva, Switzerland
Abstract Model checking is a formal verification technique to check given properties of models, designs or programs with mathematical precision. Due to its high knowledge and resource demand, the use of model checking is restricted mainly to core parts of highly critical systems. However, we and many other authors have argued that automated model checking of PLC programs is feasible and beneficial in practice. In this paper we aim to explain why model checking is applicable to PLC programs even though its use for software in general is too difficult. We present an overview of the particularities of PLC programs which influence the feasibility and complexity of their model checking. Furthermore, we list the main challenges in this domain and the solutions proposed in previous works.
Paper download THPHA159.PDF [0.269 MB / 6 pages]
Poster download THPHA159_POSTER.PDF [0.444 MB]
Export download ※ BibTeX LaTeXText/WordRISEndNote
Conference ICALEPCS2017, Barcelona, Spain
Series International Conference on Accelerator and Large Experimental Control Systems (16th)
Proceedings Link to full ICALEPCS2017 Proccedings
Session Poster Session
Date 12-Oct-17   16:45–19:00
Main Classification Software Technology Evolution
Keywords ion, PLC, MMI, software, controls
Publisher JACoW, Geneva, Switzerland
Editors Volker RW Schaa (GSI, Darmstadt, Germany); Isidre Costa (ALBA-CELLS, Cerdanyola del Vallès, Spain); David Fernández (ALBA-CELLS, Cerdanyola del Vallès, Spain); Óscar Matilla (ALBA-CELLS, Cerdanyola del Vallès, Spain)
ISBN 978-3-95450-193-9
Published January 2018
Copyright © 2018 by JACoW, Geneva, Switzerland     CC-BY Creative Commons License
cc Creative Commons Attribution 3.0