|
Рис. 1. Общая схема автоматической верификации управляющего алгоритма методом Model Checking
|
Предложен способ верификации алгоритмов управления сложными техническими системами на базе подхода Model checking (рис. 1). На основании технического задания на разработку (неформальная спецификация алгоритма и требований к нему) специфицируются алгоритм (на языке Рефлекс) и список формальных требований (язык темпоральной логики).
В цикле, на основании текущего требования формальная спецификация алгоритма редуцируется до модуля М в формате, пригодному для автоматической верификации (модель Крипке). Затем проводится автоматическая верификация модуля (проверяется, что на М выполняется свойство φ). В случае отсутствия ошибок запускается новый цикл для проверки следующего требования из списка. В случае ошибки процесс останавливается для анализа и исправления обнаруженной ошибки.
В качестве понятийного аппарата для спецификации тестов используется понятийный аппарат процесс-ориентированного программирования (модель гиперпроцесса), поддержанный как лингвистическими средствами (язык процесс-ориентированного программирования Рефлекс), так и инструментальными средствами (транслятор языка Рефлекс и IDE на основе редактора Notepad++). На тестовых задачах показано, что с помощью языка Reflex возможны кроме, собственно, спецификации алгоритмов управления, также и спецификации тестовых моделей. Штатные инструментальные средства обеспечивают автоматическое преобразование создаваемых спецификаций в исполняемый код, который в отличие от существующих методик, используемых в подходе Model checking, не требует дополнительных затрат на реализацию и отладку.
Публикации
1. Лях Т. В., Зюбин В. Е. Применение концепции виртуальных объектов управления для решения задач промышленной автоматизации // Ershov Informatics Conference: Workshop On Science Intensive Applied Software. June 24–27, 2014, St. Petersburg, Russia. Proceedings. P. 57–64.
2. Лях Т. В. Тестирование алгоритмов управления с помощью концепции ВОУ и формальных методов // Материалы 53-ой Международной научной студенческой конференции "Студент и научно-технический прогресс": Информационные технологии, Новосибирск, 11-17 апреля 2015. С. 114.
|
