Construction and Verification of PLC-programs by LTL-specification
https://doi.org/10.18255/1818-1015-2013-4-5-22
Abstract
An approach to construction and verification of PLC-programs for discrete tasks is proposed. For the specification of a program behavior we use the linear-time temporal logic LTL. Programming is carried out in the ST-language 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 PLCprograms is shown by an example. For a discrete problem we give a ST-program, its LTL-specification and an SMV-model.
A purpose of the article is to describe an approach to programming PLC, which would provide a possibility of PLC-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 that 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, 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-program is constructed according to LTL-specification. Then, the SMV-model is analysed by the symbolic model checking tool Cadence SMV.
About the Authors
E. V. Kuzmin
P.G. Demidov Yaroslavl State University
Russian Federation
Russian Federation
д-р физ.-мат. наук, профессор,
Sovetskaya str., 14, Yaroslavl, 150000, Russia
V. A. Sokolov
P.G. Demidov Yaroslavl State University
Russian Federation
Russian Federation
д-р физ.-мат. наук, профессор,
Sovetskaya str., 14, Yaroslavl, 150000, Russia
D. A. Ryabukhin
P.G. Demidov Yaroslavl State University
Russian Federation
Russian Federation
аспирант,
Sovetskaya str., 14, Yaroslavl, 150000, Russia
References
1. Кузьмин Е. В., Соколов В. А. Моделирование, спецификация и построение программ логических контроллеров // Моделирование и анализ информационных систем. 2013. Т. 20, №2. С. 104–120. (Kuzmin E. V., Sokolov V. A. Modeling, Specification and Construction of PLC-programs // Modeling and analysis of information systems. 2013. V. 20, №2. P. 104–120 [in Russian]).
2. Кузьмин Е. В., Соколов В. А. О построении и верификации программ логических контроллеров // Моделирование и анализ информационных систем. 2012. Т. 19, №4. С. 25–36. (Kuzmin E. V., Sokolov V. A. On Construction and Verification of PLC-Programs // Modeling and analysis of information systems. 2012. V. 19, №4. P. 25–36 [in Russian]).
3. Кузьмин Е. В., Соколов В. А. О верификации LD-программ логических контроллеров // Моделирование и анализ информационных систем. 2012. Т. 19, №2. С. 138–144. (Kuzmin E. V., Sokolov V. A. On Verification of PLC-Programs Written in the LDLanguage // Modeling and analysis of information systems. 2012. V. 19, №2. P. 138–144 [in Russian]).
4. Петров И. В. Программируемые контроллеры. Стандартные языки и приемы прикладного проектирования. М.: СОЛОН-Пресс, 2004. 256 с. (Petrov I. V. Programmiruemye kontrollery. Standartnye jazyki i priemy prikladnogo proektirovanija. M.: SOLONPress, 2004. 256 p. [in Russian]).
5. Canet G., Couffin S., Lesage J.-J., Petit A., Schnoebelen Ph. Towards the Automatic Verification of PLC Programs Written in Instruction List // Proc. of the IEEE International Conference on Systems, Man and Cybernetics. Argos Press, 2000. P. 2449–2454.
6. Clark E. M., Grumberg O., Peled D. A. Model Checking. The MIT Press, 2001.
7. CoDeSys. Controller Development System. http://www.3s-software.com/
8. Gries D. The Science of Programming. Springer-Verlag, 1981.
9. Parr E. A. Programmable Controllers. An engineer’s guide. Newnes, 2003. 442 p.
10. Pavlovic O., Pinger R., Kollmann M. Automation of Formal Verification of PLC Programs Written in IL // Proceedings of 4th International Verification Workshop (VERIFY’07). Bremen, Germany, 2007. P. 152–163.
11. Rossi O., Schnoebelen Ph. Formal Modeling of Timed Function Blocks for the Automatic Verification of Ladder Diagram Programs // Proc. of the 4th International Conference on Automation of Mixed Processes: Hybrid Dynamic Systems, Shaker Verlag, 2000. P. 177-182.
12. SMV. The Cadence SMV Model Checker. http://www.kenmcmil.com/smv.html
Review
For citations:
Kuzmin E.V., Sokolov V.A., Ryabukhin D.A. Construction and Verification of PLC-programs by LTL-specification. Modeling and Analysis of Information Systems. 2013;20(4):5-22. (In Russ.) https://doi.org/10.18255/1818-1015-2013-4-5-22
Views:
1155
Email this article 