On the Expressiveness of the Approach to Constructing PLC-programs by LTL-Specification

• Main Authors: E. V. Kuzmin, D. A. Ryabukhin, V. A. Sokolov
• Format: Article
• Language: English
• Published: Yaroslavl State University 2015-08-01
• Series: Modelirovanie i Analiz Informacionnyh Sistem
• Subjects: programmable logic controllers (plc); construction and verification of plc-programs; ltl-specification; minsky counter machines
• Online Access: https://www.mais-journal.ru/jour/article/view/269
• ISSN: 1818-1015; 2313-5417

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.