maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State University10.18255/1818-1015-2012-4-25-36mais-38Research ArticleОригинальные статьиArticlesО построении и верификации программ логических контроллеровOn Construction and Verification of PLC-ProgramsКузьминЕгор ВладимировичKuzminE. V.

д-р физ.-мат. наук, профессор

д-р физ.-мат. наук, профессор

kuzmin@uniyar.ac.ruСоколовВалерий АнатольевичSokolovV. A.

д-р физ.-мат. наук, профессор

д-р физ.-мат. наук, профессор

sokolov@uniyar.ac.ruЯрославский государственный университет им. П.Г. ДемидоваРоссияЯрославский государственный университет им. П.Г. ДемидоваRussian Federation2012280220151942536Copyright © Кузьмин Е.В., Соколов В.А., 20152015Кузьмин Е.В., Соколов В.А.Kuzmin E.V., Sokolov V.A.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://www.mais-journal.ru/jour/article/view/38

Проводится обзор методов и подходов к программированию «дискретных» задач ПЛК на примере задачи построения программы управления кодовым замком. Для этих подходов оценивается удобство анализа программной корректности методом проверки модели относительно средства автоматической верификации Cadence SMV. Выявляются возможные уязвимости ПЛК-программ, возникающие при некоторых подходах к программированию ПЛК.

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.

программирование логических контроллеровверификация программметод проверки моделиPLC-programsverificationmodel checkingРФФИ, Минобрнауки РФReferencesГрис Д. Наука программирования: Пер. с англ. М.: Мир, 1984. 416 с.Грис Д. Наука программирования: Пер. с англ. М.: Мир, 1984. 416 с.Кларк Э. М., Грамберг О., Пелед Д. Верификация моделей программ: Model Checking: Пер. с англ. М.: МЦНМО, 2002. 416 с.Кларк Э. М., Грамберг О., Пелед Д. Верификация моделей программ: Model Checking: Пер. с англ. М.: МЦНМО, 2002. 416 с.Парр Э. Программируемые контроллеры: руководство для инженера. М.: БИНОМ. Лаборатория знаний, 2007. 516 с.Парр Э. Программируемые контроллеры: руководство для инженера. М.: БИНОМ. Лаборатория знаний, 2007. 516 с.Кузьмин Е. В., Соколов В. А. О верификации LD-программ логических контроллеров // Моделирование и анализ информационных систем. 2012. Т. 19, №2. С. 138–144.Кузьмин Е. В., Соколов В. А. О верификации LD-программ логических контроллеров // Моделирование и анализ информационных систем. 2012. Т. 19, №2. С. 138–144.Петров И. В. Программируемые контроллеры. Стандартные языки и приемы прикладного проектирования. М.: СОЛОН-Пресс, 2004. 256 с.Петров И. В. Программируемые контроллеры. Стандартные языки и приемы прикладного проектирования. М.: СОЛОН-Пресс, 2004. 256 с.CoDeSys. Controller Development System. http://www.3s-software.com/CoDeSys. Controller Development System. http://www.3s-software.com/SMV. The Cadence SMV Model Checker. http://www.kenmcmil.com/smv.htmlSMV. The Cadence SMV Model Checker. http://www.kenmcmil.com/smv.html

The authors declare that there are no conflicts of interest present.