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


https://doi.org/10.18255/1818-1015-2012-2-138-144

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


Аннотация

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

Об авторах

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


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


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

1. Грис Д. Наука программирования. Пер. с англ. М.: Мир, 1984. 416 с.

2. Кларк Э. М., Грамберг О., Пелед Д. Верификация моделей программ: Model Checking. Пер. с англ. М.: МЦНМО, 2002. 416 с.

3. Парр Э. Программируемые контроллеры: руководство для инженера. М.: БИНОМ. Лаборатория знаний, 2007. 516 с.

4. Петров И. В. Программируемые контроллеры. Стандартные языки и приемы прикладного проектирования. М.: СОЛОН-Пресс, 2004. 256 с.

5. 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.

6. CoDeSys. Controller Development System. http://www.3s-software.com/

7. 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.

8. 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.

9. SMV. The Cadence SMV Model Checker. http://www.kenmcmil.com/smv.html


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

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

For citation: Kuzmin E.V., Sokolov V.A. On Verification of PLC-Programs Written in the LD-Language. Modeling and Analysis of Information Systems. 2012;19(2):138-144. (In Russ.) https://doi.org/10.18255/1818-1015-2012-2-138-144

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

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

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


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


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