Title :
Towards the automatic verification of PLC programs written in Instruction List
Author :
Canet, G. ; Couffin, S. ; Lesage, J.-J. ; Petit, A. ; Schnoebelen, Ph
Author_Institution :
Corp. Res. Center, Alcatel CIT, Marcoussis, France
Abstract :
We propose a framework for the automatic verification of PLC (programmable logic controller) programs written in Instruction List, one of the five languages defined in the IEC 61131-3 standard. We propose a formal semantics for a significant fragment of the IL language, and a direct coding of this semantics into a model checking tool. We then automatically verify rich behavioral properties written in linear temporal logic. Our approach is illustrated on the example of the tool-holder of a turning center
Keywords :
control engineering computing; formal verification; functional languages; functional programming; programmable controllers; programming language semantics; temporal logic; IEC 61131-3 standard; Instruction List; PLC programs; automatic verification; formal semantics; linear temporal logic; model checking tool; programmable logic controller programs; tool-holder; turning center; Automatic logic units; Ear; Formal verification; IEC standards; Input variables; Logic programming; Power system modeling; Programmable control; Safety; Turning;
Conference_Titel :
Systems, Man, and Cybernetics, 2000 IEEE International Conference on
Conference_Location :
Nashville, TN
Print_ISBN :
0-7803-6583-6
DOI :
10.1109/ICSMC.2000.884359
