On the Expressiveness of the Approach to Constructing PLC-programs by LTL-Specification
https://doi.org/10.18255/1818-1015-2015-4-507-520
Abstract
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.
About the Authors
E. V. Kuzmin
P.G. Demidov Yaroslavl State University
Russian Federation
Russian Federation
doctor of science, associate professor
Sovetskaya str., 14, Yaroslavl, 150000, Russia
D. A. Ryabukhin
P.G. Demidov Yaroslavl State University
Russian Federation
Russian Federation
graduate student
Sovetskaya str., 14, Yaroslavl, 150000, Russia
V. A. Sokolov
P.G. Demidov Yaroslavl State University
Russian Federation
Russian Federation
doctor of science, professor
Sovetskaya str., 14, Yaroslavl, 150000, Russia
References
1. Кузьмин Е.В., Рябухин Д.А., Соколов В.А., “Моделирование согласованного поведения ПЛК-датчиков”, Моделирование и анализ информационных систем, 21:4 (2014), 75–90; [Kuzmin E. V., Ryabukhin D. A., Sokolov V. A., “Modeling a Consistent Behavior of PLC-Sensors”, Modeling and Analysis of Information Systems, 21:4 (2014), 75–90, (in Russian).]
2. Рябухин Д.А., Кузьмин Е.В., Соколов В.А., “Построение IL-программ ПЛК по LTL- спецификации”, Моделирование и анализ информационных систем, 21:2 (2014), 26– 38; [Ryabukhin D. A., Kuzmin E. V., Sokolov V. A., “Construction of PLC IL-programs by LTL-specification”, Modeling and Analysis of Information Systems, 21:2 (2014), 26–38, (in Russian).]
3. Кузьмин Е.В., Соколов В.А., Рябухин Д.А., “Построение и верификация LD- программ ПЛК по LTL-спецификации”, Моделирование и анализ информационных систем, 20:6 (2013), 78–94; [Kuzmin E. V., Sokolov V. A., Ryabukhin D. A., “Construction and Verification of PLC LD-programs by LTL-specification”, Modeling and Analysis of Information Systems, 20:6 (2013), 78–94, (in Russian).]
4. Кузьмин Е.В., Соколов В.А., Рябухин Д.А., “Построение и верификация ПЛК-программ по LTL-спецификации”, Моделирование и анализ информационных систем, 20:4 (2013), 5–22; [Kuzmin E. V., Sokolov V. A., Ryabukhin D. A., “Construction and Verification of PLC-programs by LTL-specification”, Modeling and Analysis of Information Systems, 20:4 (2013), 5–22, (in Russian).]
5. Кузьмин Е.В., Соколов В.А., “Моделирование, спецификация и построение программ логических контроллеров”, Моделирование и анализ информационных систем, 20:2 (2013), 104–120; [Kuzmin E. V., Sokolov V. A., “Modeling, Specification and Construction of PLC-programs”, Modeling and Analysis of Information Systems, 20:2 (2013), 104–120, (in Russian).]
6. Минский М., Вычисления и автоматы, М.: Мир, 1971; [Minsky M., Computation: Finite and Infinite Machines, Prentice-Hall, Inc., 1967.]
7. Петров И.В., Программируемые контроллеры. Стандартные языки и приемы прикладного проектирования, М.: СОЛОН-Пресс, 2004; [Petrov I.V., Programmiruemye kontrollery. Standartnye jazyki i priemy prikladnogo proektirovanija, M.: SOLON-Press, 2004, (in Russian).]
8. Baier C., Katoen J.-P., Principles of Model Checking, The MIT Press, 2008.
9. Clark E. M., Grumberg O., Peled D. A., Model Checking, The MIT Press, 2001.
10. CoDeSys, Controller Development System, http://www.3s-software.com/.
11. Kuzmin E. V., Sokolov V. A., Ryabukhin D. A., “Construction and Verification of PLC LD Programs by the LTL Specification”, Automatic Control and Computer Sciences, 48:7 (2014), 424–436.
12. Kuzmin E. V., Sokolov V. A., “Modeling, Specification and Construction of PLC-rograms”, Automatic Control and Computer Sciences, 48:7 (2014), 554–563.
13. Kuzmin E. V., Ryabukhin D. A., Sokolov V. A., “Modeling a Consistent Behavior of PLC-Sensors”, Automatic Control and Computer Sciences, 48:7 (2014), 602–614.
14. Parr E. A., Programmable Controllers. An engineer’s guide, Newnes, 2003.
15. Schroeppel R., A Two Counter Machine Cannot Calculate 2N, Memo 257. Massachusetts Institute of Technology, Artificial Intelligence Laboratory, 1972.
16. SMV, The Cadence SMV Model Checker, http://www.kenmcmil.com/smv.html.
Review
For citations:
Kuzmin E.V., Ryabukhin D.A., Sokolov V.A. On the Expressiveness of the Approach to Constructing PLC-programs by LTL-Specification. Modeling and Analysis of Information Systems. 2015;22(4):507-520. (In Russ.) https://doi.org/10.18255/1818-1015-2015-4-507-520
Views:
1166
Email this article 