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

fYear

2011

fDate

5-9 Sept. 2011

Firstpage

1

Lastpage

8

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Emerging Technologies & Factory Automation (ETFA), 2011 IEEE 16th Conference on

Conference_Location

Toulouse

ISSN

1946-0740

Print_ISBN

978-1-4577-0017-0

Electronic_ISBN

1946-0740

Type

conf

DOI

10.1109/ETFA.2011.6058983

Filename

6058983