Title :
A model-driven engineering approach to formal verification of PLC programs
Author :
Farines, Jean-Marie ; De Queiroz, Max H. ; Rocha, Vinicius G da ; Carpes, Ana Maria M ; Vernadat, François ; Crégut, Xavier
Author_Institution :
Dept. de Automacao e Sist., Univ. Fed. de Santa Catarina, Florianopolis, Brazil
Abstract :
This paper presents a model-driven engineering approach to model and verify PLC programs written in Ladder Diagram. PLC and plant are modeled in FIACRE language according to transformation models. A verification toolchain is built around FIACRE, in order to guarantee the satisfaction of generic and application-oriented properties. The potential of this approach and associated toolchain is tested on a PLC controlled pneumatic system. Transformation from Ladder Diagram to FIACRE models is described in details and verification of PLC alone or linked with a plant is discussed in the application context.
Keywords :
control engineering computing; industrial plants; pneumatic systems; program verification; programmable controllers; FIACRE language; Ladder Diagram; PLC controlled pneumatic system; PLC programs; application-oriented properties; formal verification; model-driven engineering approach; plant; transformation models; Arrays; Context modeling; Manuals; Process control; Safety; Semantics; Unified modeling language;
Conference_Titel :
Emerging Technologies & Factory Automation (ETFA), 2011 IEEE 16th Conference on
Conference_Location :
Toulouse
Print_ISBN :
978-1-4577-0017-0
Electronic_ISBN :
1946-0740
DOI :
10.1109/ETFA.2011.6058983
