PLCverif: A Tool to Verify PLC Programs Based on Model Checking Techniques

Model checking is a promising formal verification method to complement testing in order to improve the quality of PLC programs. However, its application typically needs deep expertise in formal methods. To overcome this problem, we introduce PLCverif, a tool that builds on our verification methodolo...

Descripción completa

Detalles Bibliográficos
Autores principales: Darvas, Dániel, Blanco Vinuela, Enrique, Fernández Adiego, Borja
Lenguaje:eng
Publicado: 2015
Materias:
Accelerators and Storage Rings
Acceso en línea:https://dx.doi.org/10.18429/JACoW-ICALEPCS2015-WEPGF092
http://cds.cern.ch/record/2213507
_version_ 1780952000423264256
author Darvas, Dániel
Blanco Vinuela, Enrique
Fernández Adiego, Borja
author_facet Darvas, Dániel
Blanco Vinuela, Enrique
Fernández Adiego, Borja
author_sort Darvas, Dániel
collection CERN
description Model checking is a promising formal verification method to complement testing in order to improve the quality of PLC programs. However, its application typically needs deep expertise in formal methods. To overcome this problem, we introduce PLCverif, a tool that builds on our verification methodology and hides all the formal verification-related difficulties from the user, including model construction, model reduction and requirement formalisation. The goal of this tool is to make model checking accessible to the developers of the PLC programs. Currently, PLCverif supports the verification of PLC code written in ST (Structured Text), but it is open to other languages defined in IEC 61131-3. The tool can be easily extended by adding new model checkers.
id oai-inspirehep.net-1481692
institution Organización Europea para la Investigación Nuclear
language eng
publishDate 2015
record_format invenio
spelling oai-inspirehep.net-14816922019-09-30T06:29:59Zdoi:10.18429/JACoW-ICALEPCS2015-WEPGF092http://cds.cern.ch/record/2213507engDarvas, DánielBlanco Vinuela, EnriqueFernández Adiego, BorjaPLCverif: A Tool to Verify PLC Programs Based on Model Checking TechniquesAccelerators and Storage RingsModel checking is a promising formal verification method to complement testing in order to improve the quality of PLC programs. However, its application typically needs deep expertise in formal methods. To overcome this problem, we introduce PLCverif, a tool that builds on our verification methodology and hides all the formal verification-related difficulties from the user, including model construction, model reduction and requirement formalisation. The goal of this tool is to make model checking accessible to the developers of the PLC programs. Currently, PLCverif supports the verification of PLC code written in ST (Structured Text), but it is open to other languages defined in IEC 61131-3. The tool can be easily extended by adding new model checkers.oai:inspirehep.net:14816922015
spellingShingle Accelerators and Storage Rings
Darvas, Dániel
Blanco Vinuela, Enrique
Fernández Adiego, Borja
PLCverif: A Tool to Verify PLC Programs Based on Model Checking Techniques
title PLCverif: A Tool to Verify PLC Programs Based on Model Checking Techniques
title_full PLCverif: A Tool to Verify PLC Programs Based on Model Checking Techniques
title_fullStr PLCverif: A Tool to Verify PLC Programs Based on Model Checking Techniques
title_full_unstemmed PLCverif: A Tool to Verify PLC Programs Based on Model Checking Techniques
title_short PLCverif: A Tool to Verify PLC Programs Based on Model Checking Techniques
title_sort plcverif: a tool to verify plc programs based on model checking techniques
topic Accelerators and Storage Rings
url https://dx.doi.org/10.18429/JACoW-ICALEPCS2015-WEPGF092
http://cds.cern.ch/record/2213507
work_keys_str_mv AT darvasdaniel plcverifatooltoverifyplcprogramsbasedonmodelcheckingtechniques
AT blancovinuelaenrique plcverifatooltoverifyplcprogramsbasedonmodelcheckingtechniques
AT fernandezadiegoborja plcverifatooltoverifyplcprogramsbasedonmodelcheckingtechniques

Ejemplares similares