Графотрансформационный подход к синтезу формальных

on

Введение Основными этапами разработки управляющих систем на основе функциональных блоков (ФБ) нового международного стандарта IEC 61499 являются формулировка требований (предъявляемых к системе), формализованное описание управления и объекта управления (моделирование), верификация, валидация и реализация . Одним из слабо формализованных этапов является разработка формальных моделей контроллеров и объектов управления. Это приводит к ошибкам проектирования, усложняет автоматизацию данного этапа и замедляет процессы разработки и повторного проектирования системы в целом. Наибольшей популярностью при моделировании систем ФБ IEC 61499 пользуются модульные NCES-сети , берущие свое начало от сетей Петри. Одной из первых в этой области была работа освещаются вопросы моделирования алгоритмов ФБ с помощью NCES на уровне целочисленной арифметики. В последнее время были предприняты новые попытки автоматизации моделирования систем ФБ на основе NCES-сетей. В работе были предложены неформальные правила для создания моделей некоторых элементов ФБ, а также моделей их выполнения. Данные правила были реализованы в системе FBSD, разработанной в среде Eclipse. В работе правила преобразования реализуются в виде XSLT-скриптов и правил языка Пролог. Следует отметить, что работы ограничены в плане моделирования, например, в них не учитывается диаграмма состояний операций ЕСС (см. Figure 12 в ). Несмотря на значительный прогресс в области моделирования и автоматизации построения формальных моделей ФБ на основе NCES-сетей, можно выделить следующие основные нерешенные проблемы: 1) сложность моделирования потоков данных и алгоритмов; 2) отсутствие формальных правил преобразования систем ФБ в NCES-сети; 3) сложность перепрограммирования систем синтеза при изменении правил. И главное — отсутствует целостная методология синтеза формальных моделей для систем ФБ. В данной работе для синтеза формальных моделей систем ФБ IEC 61499 предлагается подход на основе управления моделями. Отправным пунктом проектирования является начальное описание системы ФБ, а конечным результатом — формальная модель системы. Для уменьшения сложности моделирования алгоритмов и передач данных в системах ФБ в качестве модельной формы предлагаются арифметические NCES-сети. Технология, основанная на управлении моделями (Model Driven Engineering — MDE), является в настоящее время передовой технологией разработки программного обеспечения. Трансформация моделей является «душой и сердцем» этой технологии . Важным направлением в области трансформации моделей является синтез моделей. Он относится к классу экзогенных вертикальных трансформаций. Для того чтобы трансформировать модели, они должны быть выражены на некотором языке моделирования, синтаксис которого определяется некоторой метамоделью. Метамодели выражают как исходную, так и целевую модели трансформации. Существует несколько нотаций (метаметамоделей) для построения метамоделей, среди которых, например, язык UML. Перспективным подходом к трансформации моделей является подход, основанный на трансформации графов . Он развивается и уже нашел применение в MDE. Например, был успешно применен для рефакторинга диаграмм ЕСС в базисных ФБ . Преимуществом подхода является его формальность, что позволяет избежать многих ошибок проектирования и проверить правила на корректность. Этот подход был принят в данной работе за основу. В качестве метамоделей используются типизированные атрибутные графы (ТАГ) , и трансформация на их основе поддерживается системой AGG, которая является одним из наиболее популярных средств для трансформаций графов . 1 Поток моделей в процессе синтеза Представим процесс синтеза aNCES-сетей для систем ФБ как поток графовых моделей (рис. 1). В приведенной на рис. 1 диаграмме состояний модели представлены как состояния, а макропреобразования — как переходы. Отправным пунктом преобразований является графовая модель исходной системы ФБ (состояние s0). Как правило, эта модель является многоуровневой. Конечным пунктом преобразования является графовая модель одноуровневой («плоской») aNCES-сети (состояние s4). Эта модель является наиболее приемлемой для дальнейшего анализа. Промежуточное (опциональное) состояние s1 представляет исходную систему ФБ, в базовых ФБ которой проведен рефакторинг диаграмм управления выполнением (диаграмм ЕСС) . Состояние s2 определяет одноуровневую («плоскую») систему ФБ, которую можно принять за некоторую нормализованную форму для дальнейшего использования, например, для реализации, имитационного моделирования или анализа. Состояние s3 представляет многоуровневую aNCES-модель, состоящую из множества взаимосвязанных aNCES-модулей. Это наиболее компактное и понятное для пользователя представление aNCES-моделей. Переход из одного состояния в другое производится в результате применения наборов трансформационных правил R0, R1, R2 и R3. Рис. 1 Поток моделей в задаче синтеза NCES-сетей для систем ФБ 2 Арифметические NCES-сети В зависимости от типа маркировки и весов дуг будем различать арифметические NCES-сети целочисленного и вещественного типов, причем второй тип сети включает первый. Арифметические NCES-сети вещественного типа определяются как N = (P, T, H, A, B, I, W, S, M, F, Q, C, m0), где P — конечное непустое множество позиций; T — конечное непустое множество переходов; H ? P?T ? T?P — множество обычных дуг; A?P?T?T?P — множество арифметических дуг; H?A=?; B?P?T — множество условных дуг; I?P?T — множество ингибиторных дуг; W:Н?B>R — функция весов обычных и условных дуг, где R — множество действительных чисел; S?T?T — множество событийных дуг; M:T>{, ?} — режим срабатывания перехода; F=F(0)?F(1)?F(2)?… — бесконечное множество функций различных арностей. Функция f?F(n) определяется как f:Rn>R; Q:T>F?{none} — функция, назначающая переходам функции из F; C:A?P?T>{1, 2, …} — функция нумерации входных арифметических дуг переходов; m0:P>R — начальная маркировка сети. Как можно заметить, основное отличие арифметических NCES-сетей вещественного типа от обычных NCES-сетей заключается в том, что расширен домен маркировок и весов дуг до вещественных чисел и переходам могут назначаться функции обработки данных. Введем следующие множества: apret= {p | (p, t)?A} — множество входных арифметических позиций перехода t?T; apostt= {p | (t, p)?A} — множество выходных арифметических позиций перехода t?T. Должны выполняться следующие ограничения: 1) ?t?T; 2) |apret| должно быть равно арности функции Q(t) (если таковая имеется). Функция нумерации входных арифметических дуг перехода t определяется как Ct:apret>{1, 2, …, |apret|}. Общая функция нумерации С вычисляется как . Порядок нумерации входных арифметических дуг должен соответствовать порядку аргументов функции, поставленной в соответствие переходу. Семантика вещественных NCES (без функций) сходна с семантикой обычных NCES, несмотря на то, что используется вещественный домен чисел. Семантика арифметических вещественных NCES (с функциями) отличается от семантики обычных NCES в следующем: 1) маркировка позиций из множеств apret и apostt не влияет на разрешенность перехода t?T; 2) при срабатывании перехода t?T, для которого Q(t) ? none, маркировка позиций apret не изменяется, а маркировка позиции из apostt устанавливается равной значению функции Q(t). При вызове функции Q(t) позиции из apret упорядочиваются в соответствии с функцией нумерации Ct. На рис. 2 приведен пример перехода сетевой модели, имеющего обычные (pt и tp), условные (c), событийные (ev), ингибиторные (i) и арифметические (pa и ap) дуги, а также функцию обработки данных (f). Следует отметить, что в рамках aNCES-сетей могут быть разработаны доменно-ориентированные переходы для определенной предметной области. Для моделирования алгоритмов полезны переходы-обработчики, выполняющие элементарные арифметические, логические операции и операции сравнения. Из них могут быть составлены любые алгоритмы обработки данных. Рис. 2 Переход aNCES-сети Другое важное расширение aNCES-сетей находится в области структуризации сетевых моделей. Известно, что в обычных модульных NCES-сетях не разрешены потоки меток между модулями. Это затрудняет моделирование потоков данных между ФБ. Используемый в aNCES-сетях модуль представляет собой макроопределение (рис. 3). В отличие от NCES-модулей, между модулями этого типа возможна передача меток. Тип входа-выхода модуля определяется типом проходящей через границу модуля дуги. Рис. 3 Схема модуля aNCES 3 Метамодели систем функциональных блоков Ниже определяется графический язык функциональных блоков, основанный на их представлении в виде ТАГ. Мотивом разработки языка является создание языковой базы для трансформации описаний систем ФБ в другие модельные формы, в частности в сетевые модели для проведения верификации системы. Синтаксис языка ФБ определяется с помощью метамоделей. Подход на основе метамоделирования широко распространен для определения синтаксиса визуальных языков моделирования. Разработаны метамодели начального языка ФБ, включая метамодели базисного и составного ФБ, а также метамодели одноуровневых систем, используемые в процессе синтеза формальных моделей. В качестве примера рассмотрим лишь метамодель одноуровневой системы ФБ (соответствующей состоянию s2 на рис. 1). В одноуровневой системе ФБ раскрыты все блоки, включая базисные. Эти системы состоят только из «начинок» базисных ФБ, связанных сетью клапанов данных (КД). При этом интерфейсные элементы базисных ФБ сохраняются. Эту форму представления систем ФБ можно считать нормализованной, поскольку ее дальнейшее раскрытие невозможно. Идея КД и переход к одноуровневой структуре систем ФБ были впервые предложены в работе . КД представляет программную единицу, осуществляющую при приходе управляющего сигнала копирование данных с информационных входов на выходы. В простейшем случае КД представляет копировщик, управляемый от разветвителя сигнала (рис. 4). Каждый КД имеет один событийный вход-выход и несколько информационных входов-выхо ов. Для представления КД могут использоваться различные нотации (рис. 5). На рис. 6 представлена метамодель замкнутой одноуровневой системы ФБ. Рис. 4 Простой клапан данных Рис. 5 Представления клапана данных Рис. 6 Метамодель одноуровневой системы ФБ В приведенной метамодели (рис. 6) используются следующие типы вершин: CEI и CEO — событийные вход и выход оболочки ФБ соответственно; CDI и CDO — информационные вход и выход оболочки ФБ соответственно; S — ЕС-состояние; Cond — условие ЕС-перехода; Act — ЕС-акция; Var — внутренняя переменная; DV_E — разветвитель КД; DV_D — копировщик КД. В метамодели на рис. 6 используются следующие типы дуг: w — WITH-связь; eic — дуга, связывающая событийный вход оболочки с условием ЕС-перехода; aeo — дуга, связывающая ЕС-акцию с событийным выходом оболочки; t — дуга, связывающая EC-состояния и условия; a — дуга, связывающая ЕС-состояние с первой EC-акцией или ЕС-акции между собой согласно порядку их выполнения; so — дуга, определяющая порядок оценки ЕС-переходов, выходящих из одного ЕС-состояния; par — дуга для представления потоков данных через алгоритмы. Данная дуга служит также для определения параметров условия ЕС-перехода. Для представления потока событий между ФБ используются дуги типа ec, а для представления потока данных — дуги типа dc. Из всех используемых атрибутов вершин требует пояснения только атрибут path. Данный атрибут представляет путь до родительского ссылочного экземпляра в дереве иерархии. Путь представляет собой конкатенацию имен экземпляров ФБ, лежащих на этом пути. В предложенной метамодели алгоритмы, связанные с ЕС-акцией, специфицируются только на уровне интерфейсов (входов-выходов). Кардинальности связей определяют допустимую структуру взаимосвязей экземпляров вершин. 4 Метамодели арифметических NCES-сетей В данном разделе представлен графический язык модульных aNCES-сетей, основанный на их представлении в виде ТАГ. На рис. 7 приведена метамодель (без атрибутов) используемой в работе доменно-ориентированной aNCES-сети с учетом следующих упрощений: 1) используется один доменно-ориентированный арифметический переход Copy для моделирования КД; 2) используется ограниченный набор типов входов-выходов aNCES-модулей. Вершины типов CTI, CCI, CPI, CTO, CCO и CPO определяют интерфейс модуля, причем вершина типа CTI (CTO) представляет событийный вход (выход), CCI (CCO) — условный вход (выход), CPI (CPO) — вход (выход) по данным. Вершины типов TI, CI, PI, TO, CO и PO аналогичны перечисленным вершинам, но они определяют интерфейс ссылочного экземпляра модуля. Вершина типа Т представляет переход сетевой модели, вершина типа P — позицию сетевой модели, а вершина типа Module — ссылочный экземпляр модуля. Дуги типа b определяют принадлежность интерфейсных вершин определенному ссылочному экземпляру модуля. Дуги типа pt и tp представляют связи между позициями и переходами и переходами и позициями соответственно. Связь типа ev служит для определения событийных дуг, а типа c — условных дуг. Дуги типа pa и ap являются арифметическими. Следует заметить, что метамодели конкретных типов и систем NCES могут быть получены из приведенной метамодели путем удаления определенных структурных элементов или в результате манипулирования с кратностью вершин. Например, чтобы из приведенной метамодели получить метамодель базисного модуля NCES-сети, достаточно положить кратность всех вершин, кроме вершин CTI, CCI, CTO, CCO, T и P, равной нулю. Рис. 7 Метамодель модуля многоуровневой aNCES-сети 5 Правила перехода от многоуровневых к одноуровневым системам ФБ Переход от многоуровневой структуры системы ФБ к одноуровневой структуре производится в два этапа. На первом этапе (этапе компоновки) рекурсивно осуществляется замена ссылочных экземпляров ФБ на соответствующие им развернутые экземпляры. На втором этапе (этапе встраивания) производится встраивание развернутых экземпляров ФБ в окружающую среду. Все правила перехода к одноуровневому представлению систем ФБ можно разбить на два класса: правила компоновки и правила встраивания развернутых экземпляров. С использованием правил первого вида представляются типы ФБ. Правила второго вида делятся на правила: 1) создания КД; 2) связывания КД по событийным и информационных линиям; 3) связывания КД по WITH-связям; 4) удаления ненужных элементов. В свою очередь правила создания КД включают правила: 1) создания разветвителей (входных/выходных); 2) копировщиков (входных/выходных). Правила для создания КД являются однотипными, поэтому рассмотрим их на примере правила создания входного разветвителя DV_E (рис. 8). Вершина типа EI определяет событийный вход ссылочного экземпляра ФБ. Правило применяется при выполнении следующих условий по атрибутам: 1) EI.nameM=CEI.path; 2) EI.name=CEI.name. Слева от правила записано NAC-условие, представляющее собой граф, который определяет запрещенную графовую структуру. В данном случае условие NAC предназначено для исключения дублирования разветвителей. Рис. 8 Правило создания входного разветвителя клапана данных 6 Правила синтеза многоуровневых aNCES-сетей на основе одноуровневых систем ФБ Прави