СОВМЕСТНОЕ ИСПОЛЬЗОВАНИЕ MSC И SDL МОДЕЛЕЙ, НОВЫЕ ПОДХОДЫ Докладчик: Соколов В.В. (СПбГУ)

2 Введение: современные системы Распределенность Сложность Параллелизм Встроенность и отказоустойчивость Различные производители Формальное описание протоколов взаимодействия Использование стандартов на протоколы

3 Введение: стандарты MSC и SDL Message Sequence Chart Specification and Description Language ITU-T Recommendation Z.100ITU-T Recommendation Z.120

4 Введение: Подходы и проблемы совместного использования MSC и SDL Подходы: MSC и SDL независимы Генерация SDL по MSC - система описывается на MSC, SDL не редактируется - одноразовый синтез - инкрементальный подход Верификация –трассы (MSC на SDL) –состояния протокола (параллельное исполнение моделей) –анализ одной модели Проблемы: Неуправляемость генерации Проблемы с верификацией при рассогласованияx моделей Слабость используемой (H)MSC модели

5 Генерация: обзор подходов Подходы и их оценка: Непосредственный (FSM модель не подвергается преобразованиям) // Robert G., Khendek F., Grogono P. Deriving an SDL specification with a given architecture from a set of MSCs + в полученной SDL модели лучше узнаваема MSC модель – невозможность синтеза в части случаев – излишне громоздкая SDL модель в части случаев С преобразованием (FSM модель изменяется) // Mansurov N., Zhukov D. Automatic synthesis of SDL models in Use Case Methodology + работает всегда + возможное улучшение SDL модели в части случаев – возможное ухудшение SDL модели в части случаев – SDL модель хуже узнаваема Инкрементальный перенос изменений с MSC // Khendek F., Vincent D. Enriching SDL Specifications with MSCs – возможен в очень малом количестве случаев Обобщенная модель генерации: MSC FSM SDL где FSM (Finite State Machine) описывает поведение только одного объекта

6 Генерация: причины появления проблем в подходе с преобразованием Обобщенная модель генерации: MSC FSM SDL Детализация преобразований: MSC FSM det_FSM min_FSM SDL Проблемы: –неуправляемость процесса (получение SDL моделей не удобных для разработчика) –возможные неоправданные усложнения SDL

7 Генерация: Пример неоправданных усложнений SDL: 1(2)

8 Генерация: Пример неоправданных усложнений SDL: 2(2) Вариант сгенерированного SDL после детерминизации и минимизации Желаемый вариант

9 Генерация: предлагаемые решения MSC FSM det_FSM min_FSM SDL Полученные результаты: –выделение SDL процедур –защита от эффектов ухудшения SDL –генерация SDL кода в виде, удобном для разработчика обратные преобразования настройка FSM для защиты от преобразований Влияния на процесс генерации: изменения автомата для улучшения генерируемого SDL

10 Генерация:переразложение автомата Автомат можно переразложить для получения того или иного варианта SDL кода, реализующего одну и ту же модель. Критерием этого является возможность провести синтез – детерминированность по входящим сигналам.

11 Генерация: выделение SDL процедур Выделяются области: 1.Граф области является гамаком (один вход и один выход) 2.Равны языки автоматов области (вход – начальная, выход – завершающая) 3.В области нет завершения автомата 4.Область достаточно велика Также данный способ применим для выделение не повторяющихся (одиночных) процедур для улучшения структуры генерируемого SDL.

12 Генерация: защита области от процедур детерминизации – минимизации Перемаркировка области неиспользуемым символом Детерминизация и минимизация Перемаркировка обратно

13 Генерация: области применения 1.Генерация SDL из (H)MSC 2.Генерация SDL из других моделей, сводящихся к конечно-автоматным (частный случай – предложенное расширение MSC) 3.Использование в других технологиях, где SDL модель является промежуточной (например, для перехода в VHDL) 4.Оптимизация имеющегося SDL кода (событийная модель сохраняется, работа с переменными утрачивается)

14 Верификация: существующие подходы и их проблемы Подходы: 1. MSC описывает трассы, которые «накладываются» на SDL модель 2. Состояния протокола - параллельное исполнение SDL и MSC моделей с некоторым ограничением потенциальной бесконечности // Holzmann G. Design and Validation of Computer Protocols Проблемы, вызванные расхождением SDL и MSC моделей, допустимых с точки зрения человеческой логики: SDL модель циклична, а на MSC сценарии цикличности нет Реализация на SDL модели нескольких MSC ролей Введение дополнительных сообщений на SDL модели Разбиение MSC роли на несколько сервисов Разрозненность MSC сценариев Отсутствие на MSC диаграммах символа завершения

15 Верификация: предлагаемый подход 1.для каждого из объектов переход от MSC и SDL диаграмм к конечным автоматам с учетом предметной области 2. модификация автоматов: разделение сообщений нарассматриваемые ине рассматриваемые расширение множества завершающих состояний 3.поиск такого состояния на модифицированном SDL-автомате, что начиная с него можно уложить все возможные трассы, задаваемые модифицированным MSC-автоматом (трасс может быть бесконечное число из-за наличия циклов) 4. интерпретация результата Вычисление автомата для алгоритма проверки Поиск одного автомата в другом

16 Верификация: нахождение вложения автоматов Соответствующая цепочка эквивалентностей обозначает, что вложение одного языка в другой мы можем проверить конструктивно. Для этого используется: 1.Склеивание начальных вершин автоматов 2.Операции детерминизации и минимизации 3.Проверка изоморфности автоматов 1.Выбор состояния, претендующего на начальное 2.Перемаркировка состояний в завершающие 3.Проведение анализа

17 Верификация: алгоритм MSCSDL FSM словарь сообщений словарь сообщений словарь общих сообщений FSM _ преобразованный обработка получение и интерпретация результата FSM _ преобразованный

18 Верификация: пример 1(2) SDL реализация: удовлетворяет MSC спецификации 1, без учета спецификаций 2, 3 и 4; удовлетворяет MSC спецификации 2, без учета спецификаций 1, 3 и 4; удовлетворяет спецификациям 1 и 2 вместе, если начальной является спецификация 1; удовлетворяет спецификациям 1 и 2 вместе, если начальной является спецификация 2;

19 Верификация: пример 2(2) SDL реализация: удовлетворяет спецификации 3, учитывая остальные спецификации; не удовлетворяет спецификации 4, учитывая остальные спецификации.

20 Верификация: обработка сложных случаев (идеи) Используем несколько автоматов с переходами между ними для эмуляции работы очереди (Save и уничтожение сигналов)

21 Верификация: апробация Разрозненные MSC диаграммы SDL диаграммы MSC и SDL диаграммы были взяты из реальных проектов; SDL диаграммы были достаточно сложными после многолетнего сопровождения; были найдены ошибки и проблемные места. Их качественные характеристики: – не отслеживание человеком стыков между обычными и групповыми состояниями; – возможность удалить часть состояний; – избыточность (дублирование одинаковых фрагментов).

22 Расширение описательных возможностей MSC: обоснование 1 (3) Существующие возможности MSC. Шаг 1: описание прямых веток, стандартная декомпозиция Для эффективного использования генерации и верификации MSC модель должна быть максимально более близкой (по полноте) к SDL модели. Рассмотрим проблемы существующего стандарта MSC при создании подобной модели.

23 Расширение описательных возможностей MSC: обоснование 2 (3) Существующие возможности MSC. Шаг 2: проработка вариантов требуемые завершения после варианта исполнения

24 Расширение описательных возможностей MSC: обоснование 3 (3) Существующие возможности MSC. Шаг 3: описание вариантов на MSC Отрицательные моменты: 1.вернулись на детализируемую диаграмму, а детализирующую выкинули; 2.большое количество перерисовок; 3.полученная диаграмма громоздка.

25 Расширение описательных возможностей MSC: граничные условия Граничные условия для решения: оно должно быть удобным в использовании; оно должно быть достаточно мощным; в нем должны присутствовать графические описания; по возможности оно должно быть совместимо с имеющимся стандартом MSC; мощность модели не должна быть выше конечно-автоматной (иначе, например, не возможен переход в SDL).

26 while function_1=2 do begin if function_2=0 then return 1 else procedure_2 fi; procedure_7; end; Графические диаграммы, описывающие взаимодействия объектов Текстовые описания, задающие логику стыковки сценариев Расширение описательных возможностей MSC: идеи Как графические, так им текстовые описания делятся на два типа: процедуры (не возвращают результат; соответствует некоторому (сложному) сценарию); функции (возвращают результат; разбивают множество вариантов поведения внутри на нумерованные классы). Предлагаемая модель – это некоторое статическое описание, которое отражает логику взаимодействия объектов, и для каждого из объектов может быть превращено в конечный автомат.

27 Расширение описательных возможностей MSC: предложенное решение Предлагаемые текстовые конструкции: if then else fi case for (n) повторить n раз for () повторить 0.. раз while alt opt С Pascale-подобным синтаксисом. Возможное расширение графических возможностей MSC

28 Расширение описательных возможностей MSC: структуры для разбора Блок – конечно-автоматная структура для разбора, имеющая выделенные подмножества вершин: вершина S обозначает начало блока; вершина K обозначает конец блока; множество вершин F обозначает завершение исполнения; Z – множество вершин выхода из процедуры ; C – множество вершин выхода из функции, маркированных кодом возврата.

29 Расширение описательных возможностей MSC: сравнение с существующими решениями Ряд решений (HMSC, UML Sequence и Collaboration, Use Case Maps…) так же обладают недостаточными возможностями в части описания обратных ветвей Текстовые языки, нацеленные на описание взаимодействия различных объектов (Pascal--FC, Occam, Ada, Java, Lotos…). Они предназначены для описания поведения только одного объекта, а не группы. Поэтому они проигрывают в выразительности Похожие решения: LSCs (Life Sequence Charts) // Damm W., Harel D. LSCs: Breathing Life into Message Sequence Charts она разбивает все сценарии на несколько (3) классов по критичности завершения, а в нашем случае вариантов поведения может быть произвольное количество проигрывает по описательным возможностям требует специальных средств для исполнения, а в нашем случае мы переходим в SDL CTP является комбинацией сетей Петри и MSC //Roychoudhury A., Thiagarajan P.S. Communicating Transaction Processes предлагаемое решение выигрывает из-за использования АЯВУ против сетей Петри.

30 Интеграция подходов на базе технологии REAL

31 Результаты Впервые поставлена задача настройки генерируемого SDL кода для повышения его читабельности и соответствия решаемой задаче. Разработан оригинальный алгоритм генерации SDL по MSC, решающий данную задачу. Разработана новая математическая модель верификации SDL по MSC. Разработано новое расширение MSC диаграмм, позволяющее создавать описания реальных систем. На базе данных разработок представлен оригинальный взгляд на совместное использование MSC и SDL моделей. Данные решения были проинтегрированы на базе существующей технологии REAL. Апробация разработанных решений на промышленных задачах.