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

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

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

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

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

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

sokolov@uniyar.ac.ruЯрославский государственный университет им. П.Г. ДемидоваРоссияЯрославский государственный университет им. П.Г. ДемидоваRussian Federation201225022015192138144Copyright © Кузьмин Е.В., Соколов В.А., 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/24

Обсуждаются вопросы построения технологии анализа корректности программ логических контроллеров. Рассматривается пример моделирования и верификации ѕдискретныхї LD-программ с таймером с помощью программного средства символьной проверки модели SMV при спецификации свойств на языке темпоральной логики линейного времени LTL.

We discuss some questions connected with the construction of a technology of analysing correctness of Programmable Logic Controller programs. We consider an example of modeling and automated verification of PLC-programs written in the Ladder Diagram language (including timed function blocks) of the IEC 61131-3 standard. We use the Cadence SMV for symbolic model checking. Program properties are written in the linear-time temporal logic LTL.

верификацияпроверка моделипрограммы логических контроллеровLD-диаграммыverificationmodel checkingPLC-programsLadder DiagramsРФФИReferencesГрис Д. Наука программирования. Пер. с англ. М.: Мир, 1984. 416 с.Грис Д. Наука программирования. Пер. с англ. М.: Мир, 1984. 416 с.Кларк Э. М., Грамберг О., Пелед Д. Верификация моделей программ: Model Checking. Пер. с англ. М.: МЦНМО, 2002. 416 с.Кларк Э. М., Грамберг О., Пелед Д. Верификация моделей программ: Model Checking. Пер. с англ. М.: МЦНМО, 2002. 416 с.Парр Э. Программируемые контроллеры: руководство для инженера. М.: БИНОМ. Лаборатория знаний, 2007. 516 с.Парр Э. Программируемые контроллеры: руководство для инженера. М.: БИНОМ. Лаборатория знаний, 2007. 516 с.Петров И. В. Программируемые контроллеры. Стандартные языки и приемы прикладного проектирования. М.: СОЛОН-Пресс, 2004. 256 с.Петров И. В. Программируемые контроллеры. Стандартные языки и приемы прикладного проектирования. М.: СОЛОН-Пресс, 2004. 256 с.Canet G., Couffin S., Lesage J.-J., Petit A., Schnoebelen Ph. Towards the Automatic Verification of PLC Programs Written in Instruction List // Proceedings of the IEEE International Conference on Systems, Man and Cybernetics (SMC-2000), Argos Press, 2000. P. 2449-2454.Canet G., Couffin S., Lesage J.-J., Petit A., Schnoebelen Ph. Towards the Automatic Verification of PLC Programs Written in Instruction List // Proceedings of the IEEE International Conference on Systems, Man and Cybernetics (SMC-2000), Argos Press, 2000. P. 2449-2454.CoDeSys. Controller Development System. http://www.3s-software.com/CoDeSys. Controller Development System. http://www.3s-software.com/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.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.Rossi O., Schnoebelen Ph. Formal Modeling of Timed Function Blocks for the Automatic Verification of Ladder Diagram Programs // Proceedings of the 4th International Conference on Automation of Mixed Processes: Hybrid Dynamic Systems (ADPM-2000), Shaker Verlag, 2000. P. 177-182.Rossi O., Schnoebelen Ph. Formal Modeling of Timed Function Blocks for the Automatic Verification of Ladder Diagram Programs // Proceedings of the 4th International Conference on Automation of Mixed Processes: Hybrid Dynamic Systems (ADPM-2000), Shaker Verlag, 2000. P. 177-182.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.