mdd:csp_b_generation

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
Next revision		 Previous revision
mdd:csp_b_generation [2014/06/01 15:41] – anisimoffmdd:csp_b_generation [2026/08/29 07:59] (current) – external edit 127.0.0.1
Line 1: Line 1:
 +====== Автоматическая генерация спецификаций CSP | | B из моделей xUML ======
  
 +Edward Turner, Helen Treharne, Steve Schneider, Neil Evans
 +
 +Центральная тема данной статьи — генерация исполняемых и проверяемых моделей из моделей UML. Авторы работают совместно с компанией AWE и исследуют два направления автоматической генерации. Первая — с использованием инструментария Kennedy Carter, а также SPARK Ada translators. Вторая — с использованием Epsilon. Вклад данной статьи состоит в описании первого инструмента, который сейчас разрабатывается, так же статья показывает необходимость построения фреймворка для анализа спецификаций.
 +
 +===== Исполняемый UML =====
 +
 +В данной работе фокусируются на диаграммах классов и состояний (из возможных 6 в xUML). Есть ограничение на единственность диаграммы состояний. В диаграмме состояний могут быть определены только входные действия. Они записываются на языке Action Specification Language (ASL). Он поддерживает элементы вроде create, delete, → (навигация по ассоциации), link, unlink и другие. Перемещение между состояниями осуществляется посредством сигналов. Следующий пример довольно прост и показывает xUML модель лампочки соединенной с выключателем. 
 +
 +[[mdd:_detail:mdd:снимок_экрана_2014-05-26_в_21.53.15.png|]]
 +
 +[[mdd:_detail:mdd:снимок_экрана_2014-05-26_в_21.53.59.png|]]
 +
 +===== CSP || B =====
 +
 +CSP || B — подход, которых комбинирует нотации основанные на событиях и на состояниях.
 + CSP работает с процессами и включает различные операторы параллельной композиции, внешнего выбора и другие. Также используется условный оператор и локальные определения. 
 +В работает с машинами. Его операции имеют вид PRE <условие> THEN <утверждения> END. События процессов CSP вызывают операции машин B. Архитектура CSP || B предполагает машины для классов и для ассоциаций.
 +
 +===== Генерация =====
 +
 +Генерация состоит следующих основных частей: генерация B машин, генерация CSP процессов и генерация окружения.
 +Создание машины с операциями для класса Light наглядно демонстрирует следующее изображение:
 +
 +[[mdd:_detail:mdd:снимок_экрана_2014-05-27_в_1.01.14.png|]]
 +
 +Аналогичные машины создаем для класса выключателя и ассоциации между ними. Последняя, например, будет содержать операции link_R1, unlink_R1, navigate_R1_from_B, navigate_R1_from_LL. 
 +Вкратце, процессы создаются по одному на класс и представляет поведение всех экземпляров, например, выключателя. Описание начинается с B SCTRL(b)=let …, что подразумевает для каждого экземпляра b независимое поведение. 
 +В результате выходит следующее:
 +
 +[[mdd:_detail:mdd:снимок_экрана_2014-05-27_в_1.41.26.png|]]
 +
 +===== Фреймворк для анализа =====
 +
 +Фреймворк находится в стадии разработки. Авторы определяют три типа анализа, которые представляют интерес: проверка целостности модели, проверка свободы от взаимоблокировки и верификация таблицы Эффектов. В инструменте КС проверка осуществляется посредством моделирования, которое будет демонстрировать плохое поведение  в случае проведения правильного сценария. Концепция направлена на то, чтобы подтвердить, что такое плохое поведение невозможно ни при каких условиях. Например, проверка того, что, когда кнопка включена, соответствующий световой режим в результате включается, может быть проведена посредством наблюдения за проявлением сигнала, а затем проверки статуса значения параметра.