|
Modelirovanie i Analiz Informatsionnykh Sistem, 2012, Volume 19, Number 2, Pages 138–144
(Mi mais225)
|
|
|
|
This article is cited in 5 scientific papers (total in 5 papers)
On verification of PLC-programs written in the LD-language
E. V. Kuz'min, V. A. Sokolov P. G. Demidov Yaroslavl State University
Abstract:
We discuss some questions connected with the construction of a technology of analysing correctness of Programmable Logic Controller programs. We consider an example of modeling and automated verification of PLC-programs written in the Ladder Diagram language (including timed function blocks) of the IEC 61131-3 standard. We use the Cadence SMV for symbolic model checking. Program properties are written in the linear-time temporal logic LTL.
Keywords:
verification, model checking, PLC-programs, Ladder Diagrams.
Received: 05.04.2012
Citation:
E. V. Kuz'min, V. A. Sokolov, “On verification of PLC-programs written in the LD-language”, Model. Anal. Inform. Sist., 19:2 (2012), 138–144
Linking options:
https://www.mathnet.ru/eng/mais225 https://www.mathnet.ru/eng/mais/v19/i2/p138
|
Statistics & downloads: |
Abstract page: | 371 | Full-text PDF : | 132 | References: | 40 |
|