This article is cited in 1 scientific paper (total in 1 paper)
On the expressiveness of the approach to constructing PLC-programs by LTL-specification
E. V. Kuzmin, D. A. Ryabukhin, V. A. Sokolov
P.G. Demidov Yaroslavl State University, Sovetskaya str., 14, Yaroslavl, 150000, Russia
The article is devoted to the approach to constructing and verification of discrete PLC-programs
by LTL-specification. This approach provides an ability of correctness analysis of PLC-programs by
the model checking method. The linear temporal logic LTL is used as a language of specification of
the program behavior. The correctness analysis of LTL-specification is automatically performed by the
symbolic model checking tool Cadence SMV.
The article demonstrates the consistency of the approach to constructing and verification of PLC
programs by LTL-specification from the point of view of Turing power. It is proved, that in accordance
with this approach for any Minsky counter machine can be built an LTL-specification, which is used for
machine implementation in any PLC programming language of standard IEC 61131-3. Minsky machines
equipollent Turing machines, and the considered approach also has Turing power.
The proof focuses on representation of a counter machine behavior in the form of a set of LTL-formulas and matching these formulas to constructions of ST and SFC languages. SFC is interesting
as a specific graphical language. ST is considered as a basic language because an implementation of a
counter machine in IL, FBD/CFC and LD languages is reduced to rewriting blocks of ST-program.
The idea of the proof is demonstrated by an example of a Minsky 3-counter machine, which implements a function of squaring.
programmable logic controllers (PLC), construction and verification of PLC-programs, LTL-specification, Minsky counter machines.
PDF file (250 kB)
E. V. Kuzmin, D. A. Ryabukhin, V. A. Sokolov, “On the expressiveness of the approach to constructing PLC-programs by LTL-specification”, Model. Anal. Inform. Sist., 22:4 (2015), 507–520
Citation in format AMSBIB
\by E.~V.~Kuzmin, D.~A.~Ryabukhin, V.~A.~Sokolov
\paper On the expressiveness of the approach to constructing PLC-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:
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:|