О построении и верификации программ логических контроллеров


https://doi.org/10.18255/1818-1015-2012-4-25-36

Полный текст:


Аннотация

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


Об авторах

Егор Владимирович Кузьмин
Ярославский государственный университет им. П.Г. Демидова
Россия
д-р физ.-мат. наук, профессор


Валерий Анатольевич Соколов
Ярославский государственный университет им. П.Г. Демидова
Россия
д-р физ.-мат. наук, профессор


Список литературы

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


Дополнительные файлы

Для цитирования: Кузьмин Е.В., Соколов В.А. О построении и верификации программ логических контроллеров. Моделирование и анализ информационных систем. 2012;19(4):25-36. https://doi.org/10.18255/1818-1015-2012-4-25-36

For citation: 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

Просмотров: 331

Обратные ссылки

  • Обратные ссылки не определены.


Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 1818-1015 (Print)
ISSN 2313-5417 (Online)