Alf-Verifier: Eclipse-плагин для верификации Alf/UML исполняемых моделей

В данной работе предложен плагин Eclipse, который предоставляет легкий метод проверки исполняемых моделей, для помощи системным архитекторам в спецификации исполняемых моделей поведения.

Учитывая возрастающую сложность исполняемых моделей и их влияние на качество систем программного обеспечения, становится важным использование инструментов верификации подобных моделей. Главным преимуществом инструмента являются его быстрота и эффективность (не требуется ни моделирования, ни анимации поведения), а также наличие фидбэка, с помощью котороого для неисполняемых операций возможно найти источник неполадок и предложить возможные исправления.

Инструмент предназначен для верификации свойства корректности строгой исполняемости операций, определенного в Alf Action Language. Операция строго исполняема, если она исполняется каждый раз (какие бы значения ни передавались в качестве ее параметров), а результат действий, включенных в операцию, переводит исходное состояние системы в новое, удовлетворяющее всем ограничениям целостности.

В качестве примера приводится модель меню ресторана, изображенная на рис.1.

Рис.1

Операция classifyAsSpecialMenu, которая классифицирует меню как особенное, не является строго исполняемой, поскольку после ее выполнения максимальное ограничение целостности класса SpecialMenu (второе условие) может быть нарушено (в частности, когда состояние системы во время выполнения операции уже содержит три специальных меню).

Применяемый метод принимает на вход исполняемую модель (состоящую из UML- диаграммы класса и множества операций Alf) и возвращает либо положительный ответ (если операция строго исполняема), либо корректирующий отклик, представляющий собой набор действий и условий, которые должны быть добавлены к операции для того, чтобы она стала строго исполняемой. На рис.2 изображен общий вид архитектуры инструмента. Сначала системный архитектор определяет исполняемую модель UML, с которой он хочет работать. Нажатие на “Verify strong executability” вызывает ядро метода.

Рис.2

Метод представляет собой множество Java классов, расширенных библиотеками UML2Tools (для взаимодействия с входящей UML-моделью) и Xtext (для синтаксического анализа операций Alf и их преобразования в Java классы). Отклик, предоставляемый методом, интегрируется в интерфейс Eclipse На рис.3 изображена полученная обратная связь после верификации операции classifyAsSpecialMenu (рис.1).

Рис.3

Чтобы исправить ошибки, инструментом предлагается три варианта: 1) Добавить условие проверки, что существует меньше, чем три специальных меню 2) удалять существующее специальное меню 3) переклассифицировать существующее специальное меню из Special Menu.

На рис.4. показан случай, когда для исправления был выбран первый вариант. После его применения каждое выполнение операции classifyAsSpecialMenu будет сохранено.

Рис.4

Предлагаемый плагин для Eclipse можно загрузить по ссылке: http://code.google.com/a/eclipselabs.org/p/alf-verifier/