Поволжский регион УДК 681.5 : 004.415.28 В. Н. Дубинин, В. В. Вяткин ВЕРИФИКАЦИЯ ПРИЛОЖЕНИЙ IEC 61499 НА ОСНОВЕ МЕТОДА Model Checking1 Аннотация. <...> Предлагается подход к верификации управляющих приложений международного стандарта IEC 61499 на основе метода Model Checking. <...> В рамках данного подхода предлагается формальная модель переходов состояний системы в виде правил изменения функций. <...> Для проектирования промышленных систем управления нового поколения, характеризующихся распределенностью, интеллектуальностью и способностью к реконфигурации, был разработан международный стандарт IEC 61499 [2], являющийся преемником стандарта IEC 61131-3 и ориентированный на проектирование систем управления на основе программируемых логических контроллеров (ПЛК). <...> Основным артефактом проектирования в IEC 61499 являются функциональные блоки (ФБ), что во многом определяет особенности моделирования и верификации управляющего ПО на основе IEC 61499. <...> Большое признание в настоящее время получила верификация на основе метода Model Checking [1], а среди инструментальных средств поддержки – система SMV [3, 4]. <...> Одна из реализаций SMV (NuSMV [4]), кроме верификации, позволяет проводить также и имитационное моделирование. <...> Следует отметить, что система SMV успешно использовалась для верификации во многих областях разработки аппаратуры и ПО, в частности, в промышленности при верификации ФБ стандарта IEC 61131-3 [5]. <...> Существует два основных подхода к моделированию систем ФБ на SMV: 1) моделирование ФБ с использованием промежуточной модели и ее последующее представление на SMV; 2) прямое представление ФБ на SMV. <...> Например, в [6] представлен метод моделирования ФБ IEC 61499 с использо1 Работа выполнена в рамках аналитической ведомственной целевой программы «Развитие научного потенциала высшей школы (2009–2011 годы)», № гос. регистрации НИР 01200952061. <...> В данной работе предлагается формальная модель переходов состояний приложений IEC 61499 в виде правил изменения функций. <...> В этом смысле формальную модель системы <...>