This article is cited in 3 scientific papers (total in 3 papers)
Construction of PLC IL-Programs by LTL-Specification
D. A. Ryabukhin, E. V. Kuzmin, V. A. Sokolov
P. G. Demidov Yaroslavl State University, Sovetskaya str., 14, Yaroslavl, 150000, Russia
An approach to the construction and verification of PLC IL-programs for discrete problems is proposed.
For the specification of the program behavior, we use the linear-time temporal logic LTL.
Programming is carried out in the IL-language (Instruction List) according to an LTL-specification. The correctness analysis of an LTL-specification is carried out by the symbolic model checking tool Cadence SMV.
A new approach to programming and verification of PLC IL-programs is shown by an example. For a discrete problem, we give an IL-program and its LTL-specification.
The purpose of the article is to describe an approach to programming PLC, which would provide a possibility
of IL-program correctness analysis by the model checking method.
Under the proposed approach, the change of the value of each program variable is described by a pair of LTL-formulas. The first LTL-formula describes situations which increase the value of the corresponding variable, the second LTL-formula specifies conditions leading to a decrease of the variable value.
The LTL-formulas (used for specification of the corresponding variable behavior) are constructive in the sense that they construct the PLC-program (IL-program), which satisfies temporal properties expressed by these formulas.
Thus, the programming of PLC is reduced to the construction of LTL-specification of the behavior of each program variable.
In addition, an SMV-model of a PLC IL-program is constructed according to LTL-specification.
Then, the SMV-model is analysed by the symbolic model checking tool Cadence SMV.
programmable logic controllers, software engineering, specification and verification of PLC-programs, Instruction List.
PDF file (181 kB)
D. A. Ryabukhin, E. V. Kuzmin, V. A. Sokolov, “Construction of PLC IL-Programs by LTL-Specification”, Model. Anal. Inform. Sist., 21:2 (2014), 26–38
Citation in format AMSBIB
\by D.~A.~Ryabukhin, E.~V.~Kuzmin, V.~A.~Sokolov
\paper Construction of PLC IL-Programs by LTL-Specification
\jour Model. Anal. Inform. Sist.
Citing articles on Google Scholar:
Related articles on Google Scholar:
This publication is cited in the following articles:
E. V. Kuzmin, D. A. Ryabukhin, V. A. Sokolov, “Modelirovanie soglasovannogo povedeniya PLK-datchikov”, Model. i analiz inform. sistem, 21:4 (2014), 75–90
E. V. Kuzmin, D. A. Ryabukhin, V. A. Sokolov, “O vyrazitelnosti podkhoda k postroeniyu PLK-programm po LTL-spetsifikatsii”, Model. i analiz inform. sistem, 22:4 (2015), 507–520
D. A. Ryabukhin, E. V. Kuzmin, V. A. Sokolov, “Postroenie CFC-programm PLK po LTL-spetsifikatsii”, Model. i analiz inform. sistem, 23:2 (2016), 173–184
|Number of views:|