On the expressiveness of the approach to constructing PLC-programs by LTL-specification
- Authors: Kuzmin E.V.1, Ryabukhin D.A.1, Sokolov V.A.1
-
Affiliations:
- Demidov Yaroslavl State University
- Issue: Vol 50, No 7 (2016)
- Pages: 510-519
- Section: Article
- URL: https://journals.rcsi.science/0146-4116/article/view/174524
- DOI: https://doi.org/10.3103/S0146411616070130
- ID: 174524
Cite item
Abstract
The article is devoted to an approach to constructing and verification of discrete PLC-programs by LTL-specification. This approach provides a possibility of analysing the correctness of PLCprograms by using 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 an LTL-specification can be built, which is used for machine implementation in any PLC programming language of standard IEC 61131-3. Minsky machines are equipollent to Turing machines, and the considered approach also has the 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 the implementation of a counter machine on IL, FBD/CFC and LD languages is reduced to rewriting blocks of an ST-program. The idea of the proof is demonstrated by an example of a Minsky 3-counter machine, which implements a function of squaring.
About the authors
E. V. Kuzmin
Demidov Yaroslavl State University
Author for correspondence.
Email: kuzmin@uniyar.ac.ru
Russian Federation, ul. Sovetskaya 14, Yaroslavl, 150000
D. A. Ryabukhin
Demidov Yaroslavl State University
Email: kuzmin@uniyar.ac.ru
Russian Federation, ul. Sovetskaya 14, Yaroslavl, 150000
V. A. Sokolov
Demidov Yaroslavl State University
Email: kuzmin@uniyar.ac.ru
Russian Federation, ul. Sovetskaya 14, Yaroslavl, 150000