Автоматическая генерация спецификаций CSP | | B из моделей xUML

Edward Turner, Helen Treharne, Steve Schneider, Neil Evans

Центральная тема данной статьи — генерация исполняемых и проверяемых моделей из моделей UML. Авторы работают совместно с компанией AWE и исследуют два направления автоматической генерации. Первая — с использованием инструментария Kennedy Carter, а также SPARK Ada translators. Вторая — с использованием Epsilon. Вклад данной статьи состоит в описании первого инструмента, который сейчас разрабатывается, так же статья показывает необходимость построения фреймворка для анализа спецификаций.

В данной работе фокусируются на диаграммах классов и состояний (из возможных 6 в xUML). Есть ограничение на единственность диаграммы состояний. В диаграмме состояний могут быть определены только входные действия. Они записываются на языке Action Specification Language (ASL). Он поддерживает элементы вроде create, delete, → (навигация по ассоциации), link, unlink и другие. Перемещение между состояниями осуществляется посредством сигналов. Следующий пример довольно прост и показывает xUML модель лампочки соединенной с выключателем.

CSP || B — подход, которых комбинирует нотации основанные на событиях и на состояниях. CSP работает с процессами и включает различные операторы параллельной композиции, внешнего выбора и другие. Также используется условный оператор и локальные определения. В работает с машинами. Его операции имеют вид PRE <условие> THEN <утверждения> END. События процессов CSP вызывают операции машин B. Архитектура CSP || B предполагает машины для классов и для ассоциаций.

Генерация состоит следующих основных частей: генерация B машин, генерация CSP процессов и генерация окружения. Создание машины с операциями для класса Light наглядно демонстрирует следующее изображение:

Аналогичные машины создаем для класса выключателя и ассоциации между ними. Последняя, например, будет содержать операции link_R1, unlink_R1, navigate_R1_from_B, navigate_R1_from_LL. Вкратце, процессы создаются по одному на класс и представляет поведение всех экземпляров, например, выключателя. Описание начинается с B SCTRL(b)=let …, что подразумевает для каждого экземпляра b независимое поведение. В результате выходит следующее:

Фреймворк находится в стадии разработки. Авторы определяют три типа анализа, которые представляют интерес: проверка целостности модели, проверка свободы от взаимоблокировки и верификация таблицы Эффектов. В инструменте КС проверка осуществляется посредством моделирования, которое будет демонстрировать плохое поведение в случае проведения правильного сценария. Концепция направлена на то, чтобы подтвердить, что такое плохое поведение невозможно ни при каких условиях. Например, проверка того, что, когда кнопка включена, соответствующий световой режим в результате включается, может быть проведена посредством наблюдения за проявлением сигнала, а затем проверки статуса значения параметра.