On Construction and Verification of PLC-Programs
https://doi.org/10.18255/1818-1015-2012-4-25-36
Abstract
We review some methods and approaches to programming discrete problems for Programmable Logic Controllers on the example of constructing PLC-programs for controling a code lock. For these approaches we evaluate the usability of the model checking method for the analysis of program correctness with respect to the automatic verification tool Cadence SMV. Some possible PLC-program vulnerabilities arising at a number approaches to programming of PLC are revealed.
About the Authors
E. V. Kuzmin
Ярославский государственный университет им. П.Г. Демидова
Russian Federation
д-р физ.-мат. наук, профессор
Russian Federation
д-р физ.-мат. наук, профессор
V. A. Sokolov
Ярославский государственный университет им. П.Г. Демидова
Russian Federation
д-р физ.-мат. наук, профессор
Russian Federation
д-р физ.-мат. наук, профессор
References
1. Грис Д. Наука программирования: Пер. с англ. М.: Мир, 1984. 416 с.
2. Кларк Э. М., Грамберг О., Пелед Д. Верификация моделей программ: Model Checking: Пер. с англ. М.: МЦНМО, 2002. 416 с.
3. Парр Э. Программируемые контроллеры: руководство для инженера. М.: БИНОМ. Лаборатория знаний, 2007. 516 с.
4. Кузьмин Е. В., Соколов В. А. О верификации LD-программ логических контроллеров // Моделирование и анализ информационных систем. 2012. Т. 19, №2. С. 138–144.
5. Петров И. В. Программируемые контроллеры. Стандартные языки и приемы прикладного проектирования. М.: СОЛОН-Пресс, 2004. 256 с.
6. CoDeSys. Controller Development System. http://www.3s-software.com/
7. SMV. The Cadence SMV Model Checker. http://www.kenmcmil.com/smv.html
Review
For citations:
Kuzmin E.V., Sokolov V.A. On Construction and Verification of PLC-Programs. Modeling and Analysis of Information Systems. 2012;19(4):25-36. (In Russ.) https://doi.org/10.18255/1818-1015-2012-4-25-36
Views:
1071
Email this article 