Transforming PLC Programs into Formal Models for Verification Purposes

Most of CERN’s industrial installations rely on PLC-based (Programmable Logic Controller) control systems developed using the UNICOS framework. This framework contains common, reusable program modules and their correctness is a high priority. Testing is already applied to find errors, but this metho...

Descripción completa

Detalles Bibliográficos
Autores principales: Darvas, D, Fernandez Adiego, B, Blanco, E
Lenguaje:eng
Publicado: 2013
Materias:
Accelerators and Storage Rings
Acceso en línea:http://cds.cern.ch/record/1629275
_version_ 1780934128282107904
author Darvas, D
Fernandez Adiego, B
Blanco, E
author_facet Darvas, D
Fernandez Adiego, B
Blanco, E
author_sort Darvas, D
collection CERN
description Most of CERN’s industrial installations rely on PLC-based (Programmable Logic Controller) control systems developed using the UNICOS framework. This framework contains common, reusable program modules and their correctness is a high priority. Testing is already applied to find errors, but this method has limitations. In this work an approach is proposed to transform automatically PLC programs into formal models, with the goal of applying formal verification to ensure their correctness. We target model checking which is a precise, mathematical-based method to check formalized requirements automatically against the system.
id cern-1629275
institution Organización Europea para la Investigación Nuclear
language eng
publishDate 2013
record_format invenio
spelling cern-16292752019-09-30T06:29:59Zhttp://cds.cern.ch/record/1629275engDarvas, DFernandez Adiego, BBlanco, ETransforming PLC Programs into Formal Models for Verification PurposesAccelerators and Storage RingsMost of CERN’s industrial installations rely on PLC-based (Programmable Logic Controller) control systems developed using the UNICOS framework. This framework contains common, reusable program modules and their correctness is a high priority. Testing is already applied to find errors, but this method has limitations. In this work an approach is proposed to transform automatically PLC programs into formal models, with the goal of applying formal verification to ensure their correctness. We target model checking which is a precise, mathematical-based method to check formalized requirements automatically against the system.CERN-ACC-NOTE-2013-0040oai:cds.cern.ch:16292752013-11-14
spellingShingle Accelerators and Storage Rings
Darvas, D
Fernandez Adiego, B
Blanco, E
Transforming PLC Programs into Formal Models for Verification Purposes
title Transforming PLC Programs into Formal Models for Verification Purposes
title_full Transforming PLC Programs into Formal Models for Verification Purposes
title_fullStr Transforming PLC Programs into Formal Models for Verification Purposes
title_full_unstemmed Transforming PLC Programs into Formal Models for Verification Purposes
title_short Transforming PLC Programs into Formal Models for Verification Purposes
title_sort transforming plc programs into formal models for verification purposes
topic Accelerators and Storage Rings
url http://cds.cern.ch/record/1629275
work_keys_str_mv AT darvasd transformingplcprogramsintoformalmodelsforverificationpurposes
AT fernandezadiegob transformingplcprogramsintoformalmodelsforverificationpurposes
AT blancoe transformingplcprogramsintoformalmodelsforverificationpurposes

Ejemplares similares