Transforming PLC Programs into Formal Models for Verification Purposes
Dániel Darvas, E Blanco, Borja Fernández Adiego · CERN Document Server (European Organization for Nuclear Research) · 2013
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.