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

Volume

4

fYear

2000

fDate

2000

Firstpage

2449

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;

fLanguage

English

Publisher

ieee

Conference_Titel

Systems, Man, and Cybernetics, 2000 IEEE International Conference on

Conference_Location

Nashville, TN

ISSN

1062-922X

Print_ISBN

0-7803-6583-6

Type

conf

DOI

10.1109/ICSMC.2000.884359

Filename

884359