Cargando…

Applying Model Checking to Industrial-Sized PLC Programs

Programmable logic controllers (PLCs) are embedded computers widely used in industrial control systems. Ensuring that a PLC software complies with its specification is a challenging task. Formal verification has become a recommended practice to ensure the correctness of safety-critical software but...

Descripción completa

Detalles Bibliográficos
Autores principales: Fernandez Adiego, Borja, Darvas, Daniel, Blanco Vinuela, Enrique, Tournier, Jean-Charles, Bliudze, Simon, Blech, Jan Olaf, Gonzalez Suarez, Victor M
Lenguaje:eng
Publicado: 2015
Materias:
Acceso en línea:https://dx.doi.org/10.1109/TII.2015.2489184
http://cds.cern.ch/record/2110234
_version_ 1780948870150225920
author Fernandez Adiego, Borja
Darvas, Daniel
Blanco Vinuela, Enrique
Tournier, Jean-Charles
Bliudze, Simon
Blech, Jan Olaf
Gonzalez Suarez, Victor M
author_facet Fernandez Adiego, Borja
Darvas, Daniel
Blanco Vinuela, Enrique
Tournier, Jean-Charles
Bliudze, Simon
Blech, Jan Olaf
Gonzalez Suarez, Victor M
author_sort Fernandez Adiego, Borja
collection CERN
description Programmable logic controllers (PLCs) are embedded computers widely used in industrial control systems. Ensuring that a PLC software complies with its specification is a challenging task. Formal verification has become a recommended practice to ensure the correctness of safety-critical software but is still underused in industry due to the complexity of building and managing formal models of real applications. In this paper, we propose a general methodology to perform automated model checking of complex properties expressed in temporal logics (\eg CTL, LTL) on PLC programs. This methodology is based on an intermediate model (IM), meant to transform PLC programs written in various standard languages (ST, SFC, etc.) to different modeling languages of verification tools. We present the syntax and semantics of the IM and the transformation rules of the ST and SFC languages to the nuXmv model checker passing through the intermediate model. Finally, two real cases studies of \CERN PLC programs, written mainly in the ST language, are presented to illustrate and validate the proposed approach.
id cern-2110234
institution Organización Europea para la Investigación Nuclear
language eng
publishDate 2015
record_format invenio
spelling cern-21102342019-09-30T06:29:59Zdoi:10.1109/TII.2015.2489184http://cds.cern.ch/record/2110234engFernandez Adiego, BorjaDarvas, DanielBlanco Vinuela, EnriqueTournier, Jean-CharlesBliudze, SimonBlech, Jan OlafGonzalez Suarez, Victor MApplying Model Checking to Industrial-Sized PLC ProgramsComputing and ComputersProgrammable logic controllers (PLCs) are embedded computers widely used in industrial control systems. Ensuring that a PLC software complies with its specification is a challenging task. Formal verification has become a recommended practice to ensure the correctness of safety-critical software but is still underused in industry due to the complexity of building and managing formal models of real applications. In this paper, we propose a general methodology to perform automated model checking of complex properties expressed in temporal logics (\eg CTL, LTL) on PLC programs. This methodology is based on an intermediate model (IM), meant to transform PLC programs written in various standard languages (ST, SFC, etc.) to different modeling languages of verification tools. We present the syntax and semantics of the IM and the transformation rules of the ST and SFC languages to the nuXmv model checker passing through the intermediate model. Finally, two real cases studies of \CERN PLC programs, written mainly in the ST language, are presented to illustrate and validate the proposed approach.CERN-OPEN-2015-009oai:cds.cern.ch:21102342015-12-02
spellingShingle Computing and Computers
Fernandez Adiego, Borja
Darvas, Daniel
Blanco Vinuela, Enrique
Tournier, Jean-Charles
Bliudze, Simon
Blech, Jan Olaf
Gonzalez Suarez, Victor M
Applying Model Checking to Industrial-Sized PLC Programs
title Applying Model Checking to Industrial-Sized PLC Programs
title_full Applying Model Checking to Industrial-Sized PLC Programs
title_fullStr Applying Model Checking to Industrial-Sized PLC Programs
title_full_unstemmed Applying Model Checking to Industrial-Sized PLC Programs
title_short Applying Model Checking to Industrial-Sized PLC Programs
title_sort applying model checking to industrial-sized plc programs
topic Computing and Computers
url https://dx.doi.org/10.1109/TII.2015.2489184
http://cds.cern.ch/record/2110234
work_keys_str_mv AT fernandezadiegoborja applyingmodelcheckingtoindustrialsizedplcprograms
AT darvasdaniel applyingmodelcheckingtoindustrialsizedplcprograms
AT blancovinuelaenrique applyingmodelcheckingtoindustrialsizedplcprograms
AT tournierjeancharles applyingmodelcheckingtoindustrialsizedplcprograms
AT bliudzesimon applyingmodelcheckingtoindustrialsizedplcprograms
AT blechjanolaf applyingmodelcheckingtoindustrialsizedplcprograms
AT gonzalezsuarezvictorm applyingmodelcheckingtoindustrialsizedplcprograms