Construction and verification of PLC programs by LTL specification

Author

Kuzmin, E.V. ; Ryabukhin, D.A. ; Shipov, A.A.

Author_Institution

Yaroslavl State Univ., Yaroslavl, Russia

fYear

2013

fDate

10-12 Oct. 2013

Firstpage

15

Lastpage

22

Abstract

The article proposes an approach to construction and verification of PLC ST-programs for discrete problems. The linear-time temporal logic LTL is used for the specification of the program behavior. Programming is carried out in the ST (Structured Text) language, according to the LTL-specification. The correctness analysis of the LTL-specification is performed by Cadence SMV, a symbolic model checking tool. A new approach to programming and verification of PLC ST-programs is illustrated. For each discrete problem, we propose creating an ST-program, its LTL-specification, and an SMV-model.

Keywords

program verification; programmable controllers; programming languages; temporal logic; Cadence SMV model; LTL specification; PLC ST-program construction; PLC ST-program verification; linear-time temporal logic LTL; program behavior; structured text language; symbolic model checking tool; Analytical models; Buildings; Control systems; Games; Model checking; Programming; Turning;

fLanguage

English

Publisher

ieee

Conference_Titel

Tools & Methods of Program Analysis (TMPA), 2013

Conference_Location

Kostroma

Print_ISBN

978-0-9860773-1-9

Type

conf

DOI

10.1109/TMPA.2013.7163716

Filename

7163716