Cargando…

What is special about PLC software model checking?

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 a...

Descripción completa

Detalles Bibliográficos
Autores principales: Darvas, Daniel, Blanco Viñuela, Enrique, Majzik, Istvan
Lenguaje:eng
Publicado: 2018
Materias:
Acceso en línea:https://dx.doi.org/10.18429/JACoW-ICALEPCS2017-THPHA159
http://cds.cern.ch/record/2305317
_version_ 1780957564348923904
author Darvas, Daniel
Blanco Viñuela, Enrique
Majzik, Istvan
author_facet Darvas, Daniel
Blanco Viñuela, Enrique
Majzik, Istvan
author_sort Darvas, Daniel
collection CERN
description 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.
id oai-inspirehep.net-1656448
institution Organización Europea para la Investigación Nuclear
language eng
publishDate 2018
record_format invenio
spelling oai-inspirehep.net-16564482019-09-30T06:29:59Zdoi:10.18429/JACoW-ICALEPCS2017-THPHA159http://cds.cern.ch/record/2305317engDarvas, DanielBlanco Viñuela, EnriqueMajzik, IstvanWhat is special about PLC software model checking?Accelerators and Storage RingsModel 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.oai:inspirehep.net:16564482018
spellingShingle Accelerators and Storage Rings
Darvas, Daniel
Blanco Viñuela, Enrique
Majzik, Istvan
What is special about PLC software model checking?
title What is special about PLC software model checking?
title_full What is special about PLC software model checking?
title_fullStr What is special about PLC software model checking?
title_full_unstemmed What is special about PLC software model checking?
title_short What is special about PLC software model checking?
title_sort what is special about plc software model checking?
topic Accelerators and Storage Rings
url https://dx.doi.org/10.18429/JACoW-ICALEPCS2017-THPHA159
http://cds.cern.ch/record/2305317
work_keys_str_mv AT darvasdaniel whatisspecialaboutplcsoftwaremodelchecking
AT blancovinuelaenrique whatisspecialaboutplcsoftwaremodelchecking
AT majzikistvan whatisspecialaboutplcsoftwaremodelchecking