Title :
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
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;
Conference_Titel :
Tools & Methods of Program Analysis (TMPA), 2013
Conference_Location :
Kostroma
Print_ISBN :
978-0-9860773-1-9
DOI :
10.1109/TMPA.2013.7163716
