автореферат диссертации по информатике, вычислительной технике и управлению, 05.13.11, диссертация на тему:Совместное использование MSC и SDL моделей при разработке событийно-ориентированных систем

кандидата физико-математических наук
Соколов, Владимир Владимирович
город
Санкт-Петербург
год
2007
специальность ВАК РФ
05.13.11
цена
450 рублей
Диссертация по информатике, вычислительной технике и управлению на тему «Совместное использование MSC и SDL моделей при разработке событийно-ориентированных систем»

Автореферат диссертации по теме "Совместное использование MSC и SDL моделей при разработке событийно-ориентированных систем"

Op*

САНКТ-ПЕТЕРБУРГСКИЙ ГОСУДАРСТВЕННОЙ

УНИВЕРСИТЕТ

UU3D55G42

На правах рукописи

Соколов Владимир Владимирович

СОВМЕСТНОЕ ИСПОЛЬЗОВАНИЕ MSC И SDL МОДЕЛЕЙ ПРИ РАЗРАБОТКЕ СОБЫТИЙНО-ОРИЕНТИРОВАННЫХ СИСТЕМ

05 13 11 — Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей

АВТОРЕФЕРАТ диссертации на соискание ученой степени кандидата физико-математических наук

Санкт-Петербург 2007

003055642

Работа выполнена на кафедре системного программирования математике механического факультета Санкт-Петербургского государственного уни верситета

Научный руководитель

доктор физико-математических наук, профессор Терехов Андрей Николаевич

Официальные оппоненты доктор технических наук,

профессор Гольдштейн Борис Соломонович

кандидат физико-математических наук, доцент Костин Владимир Андреевич

Ведущая организация

Институт системного программирования РАН

Защита диссертации состоится " дсл-у^^а 2007 года в-^-часов на заседании диссертационно1 о совета Д212 232 51 по защите диссертаций на соискание ученой степени доктора наук при Санкт-Петербургском государственном университете по адресу 198504, Санкт-Петербург, Старый Петергоф, Университетский пр , д 28, математико-механический факультет Санкт-Петербургского государственного университета

С диссертацией можно ознакомиться в Научной библиотеке Санкт-Петербургского государственного университета по адресу 199034, Санкт-Петербург', Университетская наб , д 7/9

Автореферат разослан 12,±." 2007 года

Ученый секретарь диссертационного совета доктор физико-математических наук профессор

Б К Мартыненко

Общая характеристика работы

Актуальность темы

В последнее десятилетие в развитии программного обеспечения произошел качественный скачок Электронный мир теперь распределен, параллелен и взаимосвязан Банки, авиалинии, телефонные компании не могут работать без интенсивного обмена информацией между всеми действующими объектами С возрастанием сложности протоколов взаимодействия потребовались специальные средства, нацеленные на их описание, разработку и отладку

Системы, в которых использовались сложные протоколы взаимодействия, существовали достаточно давно Это телекоммуникационные системы Соответствующие проблемы там были успешно разрешены, в результате чего были созданы стандарты SDL (Specification and Description Language) [15] и MSC (Message Sequence Chart) [14, 16] Данные стандарты были разработаны Международным Консультационным Комитетом по Телеграфии и Телефонии, ныне ITU-T MSC и SDL являются стандартом де-факто в международной телефонии Организация ITU-T использует их для спецификации других стандартов (протоколов) — UMTS, GSM, E-DSS-1, V5 2, SS7 и других MSC и SDL широко используются в известных фирмах - разработчиках телекоммуникационного оборудования

MSC и SDL применяются для описания динамического поведения системы В современных системах разработки телекоммуникационного ПО используются оба стандарта, поскольку они дают различную информацию и дополняют друг друга MSC больше относится к этапу проектирования, а SDL — к этапу программирования Возникает необходимость обеспечения их согласованности, поскольку они по-разному описывают одни и те же алгоритмы поведения Параллельное использование моделей без их согласования приводит в тому, что одна модель дает корректное описание, а другая содержит устаревшую информацию Для того, чтобы переиспользовать данные с MSC модели существует синтез SDL диаграмм по MSC [6, 20, 21] Для проверки их согласованности существует ряд алгоритмов верификации [И, 12, 13]

Выбранные алгоритмы совместного использования моделей вносят ряд ограничений на всю технологию Например, алгоритмы генерации могут как урезать MSC модель [19], так и запрещать модифицировать SDL модель [20], а так же влияют на согласование данных, описывающих структуру системы [20, 21] (то есть, на то, что непосредственно fie относится к событийному описанию системы) Алгоритмы верификации тоже имеют свои границы применимости Поэтому возникает проблема интеграции

различных подходов в рамках разрабатываемой технологии так, чтобы они обеспечивали гак описательную, так и алгоритмическую мощь

В общем виде задача сравнения MSC и SDL алгоритмически неразрешима, поэтому необходима разработка алгоритма, который бы абстрагировалсч от части информации и давал адекватные результаты Существующие подходы плохо работают при рассогласованиях моделей, допустимых с точки зрения человеческой логики, таких как добавление и удаление сообщений, цикличности частей моделей, неполнота MSC модели и тд

Существенным минусом известных алгоритмов генерации является то, что в них нет возможности влиять на генерируемый SDL код Для разработки это неудобно, поэтому автор ставит задачу о настройке SDL кода То есть, среди ряда SDL моделей, соответствующих данному MSC, выбрать наиболее удобную для технолога1

Как верификация, так и генерация базируются на том что существует MSC модель, практически полностью аналогичная SDL модели На самом деле, существующий стандарт (H)MSC [14, 16] хорошо приспособлен лишь для описания прямых веток То есть, хорошо приспособлен лишь для детализации сценариев поведения Описание ошибочных ситуаций ведет к большому количеству перерисовок сценариев вместо соответствующего их дополнения Данный момент очень неудобен для технолога Причиной этого является то, что существующая детализация является аналогом процедуры в АЯВУ, однако логика описания ошибочных ситуации ближе к функциям Необходимо разработать соответствующую MSC-подобную модель

Цели работы

Целью работы является разработка подхода по совместному использованию MSC и SDL моделей и реализация его в технологическом средстве Разработка подхода была разделена на решение следующих основных задач

- выработать структуру средства, предоставляющего набор возможностей совместного использования MSC и SDL с отслеживанием корректности разработки,

- разработать верификацию SDL диаграмм по MSC диаграммам при априорном знании о наличии расхождений,

- разработать алгоритм генерации SDL диаграмм по MSC диаграммам, позволяющий строить SDL код, отвечающий требованиям технолога,

*Так мы называем разработчика, создающего продукт с помощью технотогии

- расширить MSC модель для возможности создавать максимально полные MSC описания

Общая методика

MSC и SDL модели рассматриваются как структуры, задающие языки, состоящие из сообщений Каждый такой язык задается с помощью конечного автомата Разработаны алгоритмы перехода от предметной области MSC и SDL в конечный автомат и обратно Для разбора языков использовались контекстно-свободные (LALR(l)) грамматики Разработаны алгоритмы обработки конечного автомата на базе конечно-автоматных алгоритмов и графов, специфичные для предметной области и выбранной задачи Оценка применимости полученных алгоритмов осуществлялась экспериментально

Основные результаты

Предложена методология совместного использования MSC и SDL диаграмм

Разработана математическая модель верификации SDL по MSG, позволя ющая осуществлять проверки моделей в при наличии ряда отличий, появляющихся в течение жизненного цикла

Создан алгоритм автоматизированной генерации SDL кода по конечному автомату, позволяющий получать SDL код, удобный для технолога

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

Научная новизна

Представлен оригинальный взгляд на совместное использование MSC и SDL моделей, использующий разработанные алгоритмы верификации, генерации, расширения MSC и сочетания статических данных MSC и SDL

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

Впервые поставлена задача настройки генерируемого SDL кода под требования технолога

Разработан оригинальный алгоритм генерации SDL по MSC, реализующий данную настройку

Разработано новое расширение MSC, которое позволяет создавать описания реальных систем за счет большей описательной гибкости, чем в других моделях

Практическая и теоретическая ценность

Разработан технологический подход по совместному использованию MSG и SDL моделей, позволяющий ускорить процесс разработки и отладки ПО, существенной частью которого являются протоколы взаимодействия

Разработана новая модель верификации, новое расширение MSC диаграмм, оригинальныи алгоритм генерации SDL по MSC, используемые в данном подходе

Разработанные подходы могут быть применены для ряда других систем, сводящихся к конечно-автомагным Например, в подходах на базе UML [23]

Алгоритмы генерации SDL могут быть так же применены для систем, в которых SDL является промежуточной моделью [10], а так же для оптимизации существующего SDL кода

На практике предложенные методы были использованы при разработке; объектов и исследованиях кода реальных промышленных систем

Апробация работы

Результаты работы докладывались на семинаре Института системного программирования РАН (2006 год, г Москва)

Предложенная технологии была реализована в виде набора технологических средств, дополняющих средство REAL [2, 4]

Разработанные подходы использовались при разработке телефонной станции "Юнивер-А" — многоканального радиоудлинителя телефонных линий

Публикации

Основные результаты диссертации изложены в 3-х работах, перечисленных в конце автореферата

Структура и объем диссертации

Диссертация состоит из введения, 4-х глав, заключения, списка литературы и 3-х приложений Текст диссертации изложен на 146-ти страницах Список литературы содержит 74-ре наименования

Содержание работы

Во введении показывается актуальность выбранной темы исследований, излагаются научный и исторический контексты диссертационной работы Кратко перечислены основные результаты диссертации

Диссертация начинается с рассмотрения современных систем, показывается необходимость специальных средств для описания протоколов взаимо-

действия Рассматриваются SDL и MSC модели, области их использования, технология REAL, на базе которой реализуются все предложенные решения Приводится краткое введение в SDL и MSC, указывается их сходство и различие, показываются их места в процессе разработки cucieM Доказывается, что нужны оба именно стандарта и необходимы специальные процедуры их согласованному использованию

Дается обзор существующих подходов по совместному использованию MSC и SDL моделей с указанием их сильных и слабых сторон

1 MSC и SDL независимы, что плохо из-за их несогласованности и двойного проектирования системы — сначала на MSC, потом на SDL

2 Попытки создавать системы на основе MSC диаграмм с последующим синтезом SDL

(a) Только на MSC модели с использованием SDL только как промежуточной модели без возможности ее редактирования [20] Данный подход имеет ряд недостатков, связанных с недостаточными возможностями MSG модели и с утратой выразительности SDL

(b) "Односторонний синтез" [6, 21], неудобный с точки зрения поддержки всего цикла разработки

(c) "Инкрементальные алгоритмы" [17, 19], которые требуют такого количества ограничении, что применимы лишь в очень малом классе случаев

3 Алгоритмы сравнения используемых MSC и SDL диаграмм для проверки соответствия

(a) Генерация трасс2 с MSC диаграмм с "наложением"3 их на SDL диаграммы [11, 12]

(b) Алгоритмы параллельного исполнения моделей с анализом внутренних состояний протокола [13]

Формулируются условия построения CASE системы возможность независимого использования MSC и SDL моделей, генерация SDL по MSC, верификация SDL по MSC с учетом изменении, появляющихся в течение жизненного цикла системы Описание статической части системы4 выделяется в отдельную модель, которой пользуются и MSC, и SDL Данная модель заменяет соответствующие возможности описания системы в каждом из стандартов Указываются проблемные места, которые присутствуют в существующих подходах совместного использования MSC и SDL

2Трассой называем цепочку сообщений

3Мы говорим, что трасса "наложи тась", если мы представили такой вариант выполнения SDL, что при этом была порождена цепочка входящих и выходящих сообщений, специфшшроваиная трассой

4Имеющиеся классы системы, сообщения, параметры сообщений, интерфейсы, порты и тд [15, 16]

В первой главе описывается математический аппарат, используемый во всей работе Формулируются необходимые определения и теоремы, даются комментарии к ним

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

Прежде всего, ставится задача по верификации SDL модели по MSC модели, когда они описывают одну и ту же систему, но при этом отличаются Например, на MSC отсутствует описание цикличности, добавлены или убраны некоторые сообщения, произведено расщепление или слияние MSC сценариев и тд Описывается используемая интерпретация MSC и SDL моделей с точки зрения верификации

Дается формальное определение алюритма верификации и его обоснование в терминах предметной области MSC и SDL диаграмм Сутью алгоритма являются

1 для обрабатываемого объекта выбираются его SDL диаграммы и множество MSC диаграмм, являющееся подмножеством диаграмм, в ко торых он присутствует,

2 переход от MSC и SDL диаграмм к конечным автоматам, порождающих для данного объекта такой же язык из сообщений, который бы порожда ia соответствующая модель,

3 замена в конечных автоматах части переходов, маркированных сообщениями, на е-переходы То есть, устранение соответствующих переходов из рассмотрения При автоматической работе алгоритма остаются только сообщения, присутствующие на обоих автоматах,

4 поиск такого состояния на модифицированном SDL-автомате, что начиная с него можно ' наложить' все возможные трассы, задаваемые модифицированным MSC-автоматом Количество данных трасс может быть бесконечным,

5 интерпретация результата в рамках предметной области

Сам алгоритм дается неконструктивно, поэтому переводится в конструктивную форму на базе математики конечных автоматов При этом задача поиска возможности вложения трасс сводится к задаче проверки включения одного языка в другой, затем сводится к задаче проверки равенства языков некоторых автоматов, что конструктивно проверяется изоморфно-стью их минимизированных детерминированных автоматов

Предлагаемый подход выигрывает как у проверок на основе состояний протокола [13], так и у конечно-автоматных моделей без словарей сообщений [18] за счет интеграции нескольких идей

- переход от SDL и MSC к конечно-автоматным моделям с учетом специфики SDL и MSC (конструкции параллельного исполнения MSC, уничтожение и сохранение сообщении, не обрабатываемых в текущем SDL-состояшш и тд),

- операции фильтрации, ра щеляющие общее множество сообщений на "используемые" и "неиспользуемые",

- проверки на включение языков, реализуемой с помощью математики конечных автоматов

Это дает возможность проверять соответствие MSC и SDL диаграмм на соответствие в ряде случаев, когда другие алгоритмы не применимы

В третьей главе рассматривается генерация SDL диаграмм по MSC диаграммам Дается обзор существующих алгоритмов, обсуждаются их возможности, описывается предлагаемый подход Для этого показываются принципы построения отдельных элементов SDL, после чего выводится алгоритм построения всего кода Предлагаются методы вмешательства в данный алгоритм для улучшения генерируемого SDL

Проводится обзор существующих алгоритмов по генерации SDL из MSC Фактически существует две группы — серия московских работ [3, 20] и серия канадских [6, 17, 21] Во всех данных методах сначала осуществляется переход от MSC к конечному автомату Наиболее существенное отличие между ними в том, что в канадских работах генерация начинается сразу, а в московских к конечному автомату перед эгим применяются алгоритмы детерминизации и минимизации Канадские алгоритмы выдают код, в котором лучше угадывается изначальный MSC, более точно рассчитывают правила для конструкции Save, но из-за отсутствия алгоритма детерминизации применимы не всегда, а из-за отсутствия минимизации могут выдавать менее оптимальный код Московский вариант может осуществить синтез всегда, но при этом он может как улучшать компактность SDL, так и ухудшать ее, а так же понижать степень узнаваемости MSC в SDL

Отдается предпочтение связке детерминизация - минимизация для повышения области применимости, но следует выполнить ряд действии для того, чтобы убрать негативные влияния данных алгоритмов на полученный SDL В работе приводится соответствующий пример

Основной подход работы заключается в том, что конечная SDL модель предназначается для человека, поэтому неуправляемого алгоритма синтеза мало, технолог должен иметь возможность получить тот вариант SDL кода,

который лучше удовлетворяет его требованиям, среди ряда возможных, реализующих одну и ту же задачу

Для этого вводится промежуточная модель между MSC и SDL диаграммами для настройки процедуры синтеза Это конечный автомат Он более компактен, чем MSC и SDL модели, и удобен для редактирования перед последующей генерацией SDL На результат i енерации можно повлиять используя данные из модели MSC, модели SDL и на у ровне конечных автоматов Например, два параллельно выполняющихся MSG сценария, при выполнении ряда ограничении, удобно реализовывать тремя участками SDL кода, которые выполняют каждый из сценариев и процедуру, которая создает и завершает исполнение данных "сценариев", а так же передает сообщения на них SDL модель мы используем когда работаем с уже готовым SDL кодом — например, используем описатели "*" для состоянии и сообщений, а так же описатель "-'' для состояний при выделении общих участков кода Иногда это может существенно уменьшить его объем

Наиболее существенной, с точки зрения влияния на получаемый SDL, является область работы с конечными автоматами При этом конечный автомат представляется в виде графа, с которым удобно работать визуально На данном трафе изображены состояния конечного автомата и переходы между ними Переходы несут информацию о имени сообщения и его типе — посылаемое пли принимаемое С конечным автоматом можно работать либо и до, и после связки процедур детерминизация-минимизация для защиты от изменений, либо после выполнения данных алгоритмов Работа "н до, и после" путем замены части сообщений на отсутствующие в списке, а потом замена обратно решает проблему детерминизации во выходящим сообщениям, иногда негативно влияющую на SDL код Работа "и до, и после" путем замены ценой области и замены обратно позволяет защитить ее от изменений, вносимых данными алгоритмами Работа "после" позволяет "переразложить' код нужным образом, а так же интерактивно выделять процедуры путем обнаружения гамаков [1]

При построении SDL диаграмм по MSC диаграммам для выбранною объекта проходим по следующей цепочке

1 проверка корректности MSC описания [6, 8],

2 переход от MSC диаграмм данного объекта к недетерминированному конечному автомату, порождающему все трассы данного объекта [3],

3 опциональная защита частей автомата от процедур преобразования,

4 детермшшзация автомата,

о минимизация автомата,

б "восстановление" автомата, если применялись алгоритмы пункта 3

7 опциональное "переразложение" автомата и выделение процедур,

8 построение схемы SDL кода

Данный алгоршм позволяс1 настраивать генерируемый SDL код под требования технолога, чего нет ни в одном из алгоритмов генерации Поскольку при генерации SDL диаграмм по MSC диаграммам используется переход MSC—>FSM—>SDL, то вместо MSC диаграмм может быть задана любая модель, которая сводится к конечным автоматам Это открывает возможность переноса информации из других технологии в SDL Особо следует отметить, чю исходной моделью может также служить и SDL модель Таким образом можем проводи!ь оптимизацию уже написанного SDL кода

В четвертой главе вводится предлагаемое расширение MSC Для этого сначала показываются важные недостатки существующего стандарта MSG, затем описывается предлагаемое решение на базе разработанного математического аппарата Предложеннып подход обсуждается и иллюстрируется примерами

Для резулыативнои работы алгоритмов генерации и верификации необходимо, чтобы существовало MSC описание системы, которое было бы как можно более полным Существующий стандарт MSC имеет серьезный недостаток, не позволяющий описывать в нем обратные ветви (то есть, ветви, обрабатывающие ошибочные ситуации) Он хорошо работает для описания прямых ветвей (случаев, когда все происходит без ошибок) путем постепенной декомпозиции сценариев Когда на набор сценариев, описывающих прямые ветви, начинают добавлять проработку ошибочных ситуаций, то оказывается, что изменение детализирующего сценария влияет на детализируемый Зачастую данное изменение на этом не заканчивается, а продвигается "выше" по иерархии сценариев В реальной работе это приводит к достаточно большому количеству "перерисовок" сценариев, на что тратится время

Причина данной проблемы достаточно очевидна — из сценария невозможно вернуть результат его выполнения с последующим анализом в детализируемом сценарии При этом важным граничным условием является то, что решение данной проблемы не должно быть сложнее конечно-автоматной модели для последующею использования в генерации и верификации Соответствующая модель была разработана, идеологически она является смесью графического MSC и текстовых описаний, при необходимости графические и текстовые описания могут возвращать результат выполнения, данный результат выполнения может быть проанализирован в текстовом описании с выполнением последующих действий примерно так же, как это делается на языке Pascal, полное описание на данной модели конверти-

руется в конечный автомат для каждого из объектов для последующего использования

function f2, begin

while f 1=2 do

if f3>1 then return 1

else

proc4

fi, return 2,

end

procedure mam, begin

if f2=1 then

ргосБ Рис 1 Расширение графических диа-

fi. грамм для добавления возможности

end возвращать результат

Слева от рис 1 приведен образец текстового описания предлагаемого рас гаирения MSC На самом рисунке изображено необязательное расширение графических сценариев возможностью возвращения результата его выпол нения Как графические, так и текстовые описания делятся на "процедуры' и "функции" "Процедуры" не возвращают результат "Функции" результат возвращают На примере продемонстрировано совместное использование текстовых и графических описаний, и организация "функций" на базе "про цедур" и обратно По "процедуре" для любого объекта может быть построен конечный автомат, описывающий его язык, состоящий из входящих и вы ходящих сообщений

Если проводить аналогии с обычными сценариями, то "процедура" является сценарием, а "функция" является набором нумерованных сценариев Можно считать, что сценарии в "функции" являются вариантами выпот-нения аналогично конструкции alt, и номер присвоен концу сценария При использовании "функций" в текстовом описании данный набор можно разделить необходимым образом согласно их нумерации и соединить с нужными последующими действиями Для текстовых описаний реализованы конструкции if, case, for, while, opt, alt с Pascal'e-подобным синтаксисом

При разборе "программы" на предложенном расширении MSC для фиксированного объекта используются структуры, изображенные на рис 2 В графическом изображении данной структуры вершина S обозначает начало блока (аналогия начального состояния конечного автомата) Вершина К обозначает конец блока, при последовательном соединении блоков К со-

msc f3

s

Рис 3 Блок, соответству- Рпс 4 Использование блоков при ютцни посылке одного разборе оператора if общего вида сообщения

единяется с S, на рпс 3 приведен блок дтя одного сообщения Множество вершин F обозначает завершение исполнения (аналогия множества завершающих состояний конечного автомата) Z — множество вершин выхода из "процедуры" (return без кода возврата) С — множество вершин выхода из "функции", маркированных кодом возврата (например, return 7)

Внутри блока находятся конечно-автоматные структуры, описывающие прием и посыпку сообщений В процессе разбора грамматики текстового расширения MSC происходят операции с данными блоками На них же определены проверки корректности "программы" Графические представления так же отображаются в подобные блоки Блок, получающийся в конце разбора, является "процедурой" и отображается в конечный автомат

На рис 4 показано использование блоков при разборе оператора if обще го вида Множество кодов возврата "функции" (Со) на основе выражения разбивается на 2 подмножества (C0_iflen и ^o-ehe^ ^ соответствующим вершинам одного подмножества присоединяется бток ветви then, а к другому — else через начальные вершины данных блоков Концы блоков ветвей (К 1 и К 2) соединяются с дополнительной вершиной q В результате из трех блоков ("функция", бпок ветви then и блок ветви else) получаем один блок, соответствующий оператору if В качестве S для него будет выступать So, в качестве С объединение и С7>, в качестве Z — Z\ и Z<i, в качестве К — q, в качестве F — объединение Fq, F\ и Fi

Рассмотрим место предложенного решения среди диаграмм, которые поз-, воляют описать алгоритмы взаимодействия нескольких объектов, и могут

давать все поведение группы объектов или системы, а не разрозненных информационных срезов Достаточно большое количество моделей, аналогично MSC, рассчитаны лишь на постепенную детализацию без проработки обратных ветвей, и имеют похожие проблемы Это и MSC-подобная группа — HMSC [14], UML Sequence [23] и UML Collaboration [23] диаграммы Some's Scenarios [24] Это и попытка представить поведение системы в виде конечного автомата Chisel Diagrams [7] Это и потоки данных — UML Activity диаграммы [23] и Use Case Maps (UCMs) [5] Предлагаемое решение превосходит их по гибкости, поскольку логика стыковки различных вариантов поведения лучше описывается текстом Так же следует упомянуть текстовые языки, нацеленные на описание взаимодействия различных объектов (Pascal-FC, Оссага, Ada, Java, Lotos и тд), но они предназначены для описания поведения одного объекта, и лежат вне рассматриваемой области

Задача по расширению MSC для описания обратных веток уже ставилась — это LSCs (Life Sequence Charts) [9] Предлагаемое решение перекрывает LSCs за счет возможности иметь произвольное множество кодов возврата, а не двух вариантов — нормального и ошибочного Так же предлагаемое решение в рамках всего подхода сводимо к широко используемому SDL, а не требует отдельной модели для исполнения, как LSCs Существует модель СТР [22], являющаяся комбинацией MSC и сетей Петри Разработанное решение лучше за счет комбинирования АЯВУ и MSC Выигрыш получается за счет того, что технологам при разработке протоколов привычно думать в терминах циклов и условных операторов, нежели в терминах сетей Петри

В заключении приведена краткая характеристика технологического подхода, разработке которого было посвящено данное исследование, и сформулированы основные полученные результаты

В Приложении А. приведены используемые элементы MSC и SDL диаграмм В Приложении В. дается грамматика предложенного расширения MSC Приложение С. содержит список иллюстраций

Список литературы

[1] Касьянов В Н Оптимизирующие преобразования программ — М Наука, 1988 - 336 с

[2] Кознов Д В Визуальное моделирование компонентного программного обеспечения Дис канд физ -мат наук — СПбГУ, 2000 — 82 с

[3] Мансуров Н Синтез исполняемых SDL спецификаций по сценарным моделям // Тр ин-та Системного Программирования — 1999

[4] Терехов АН и др REAL методология и CASE средство разработки информационных систем и ПО систем реального времени // Программирование — 1999 — № 5 — с 45-51

[5] Use Case Maps (UCMs) нотация Определения, публикации, средства http //www useCaseMaps org/mdex shtml

[6] Abdalla M , Khendek F , Butler G New Results on Deriving SDL Specifications from MSCs // Proc of 9th SDL Forum — 1999 — P 55-67

[7] Aho A , Gallagher S , Griffeth N , Scheel С , Swayne D Sculptor with Chisel Requirements Engineering for Communications Services // Proc in 5th International Workshop on Feature Interactions in Telecommunications and Software Systems (FIW'98) — Lund, Sweden IOS Press, 1998 — P 45-63

[8] Ben-Abdallah H , Leue S Syntactic detection of process diveigence and nonlocal choice in message sequence charts // Proc of the Tools and Algorithms for the Construction and Analysis of Systems, Third International Workshop (TACAS'97) - № 1217 m Lecture Notes m Computer Science — Enschede, The Netherlands Springer, 1997 — P 259-274

[9] Damm W , Harel D LSCs Breathing Life into Message Sequence Charts // Proc m 3rd IFIP International Conference on Formal Methods for Open Object-based Distributed Systems (FMOODS'99) — Kluwer Academic Publishers, 1999 — P 293-312

[10] Daveau J -M , Marchioro G , Valderrama С , Jerraya A VHDL generation from SDL specifications // Proc of the XIII IFIP Conf oil Computer Hardware Description Languages (CHDL'97) — Toledo, Spam — 1997

[11] EG 201 015 Ver 1 2 1, Methods for Testing and Specification (MTS), Specification of protocols and services, Validation methodology for standards using Specification and Description Language (SDL), Handbook — 1999 — 28 p

[12] ETR 184 Methods for Testing and Specification (MTS), Overview of validation techniques for European Telecommunication Standards (ETSs) containing SDL — 1995 — 27 p

[13] Holzmann G Design and Validation of Computer Protocols // Prentice-Hall, 1991 — ISBN 0-13-539834-7 — 512 p

[14] ITU-T MSC2000R3 Draft Z 120 Message Sequence Charts ITU-T Recommendation Z 120 — 1999

[15] ITU-T Recommendation Z 100 Specification and description language (SDL) — 1999 — 244 p

[16] ITU-T Recommendation Z 120 Message Sequence Chart (MSC) — 1999 — 136 p

[17] Khendek F , Vincent D Enriching SDL Specifications with MSCs // Proc of 2nd Workshop of the SDL Forum Society on SDL and MSC (SAM2000) — 2000 — P 305-319

[18] Kurshan R Computer-Aided Verification of Coordinating Processes // Princeton Series in Computer Science, 1994 — ISBN 0691034362 — 270 p

[19] Li J , Horgan J Applying formal description techniques to software architectural design // Computer Communications — Vol 23 — № 12 - 2000 - P 1169-1178

[20] Mansurov N , Zhukov D Automatic synthesis of SDL models m Use Case Methodology // Proc of 9th SDL Forum — 1999 — P 225-240

[21] Robert G , Khendek F , Grogono P Deriving an SDL specification with a given architecture from a set of MSCs // Proc of 8th SDL Forum — 1997 — P 197-212

[22] Roychoudhury A , Thiagarajan P S Communicating Transaction Processes // Proc in IEEE International Conference on Application of Concurrency in System Design (ACSD'2003) — 2003 — P 157-166

[23] Rumbaugh J , Jacobson I, Booch G The Unified Modeling Language; Reference Manual — Addison-Wesley, 1999 — 576 p

[24] Some S , Dssouli R , Vaucher J Toward an Automation of Requirements Engineering using Scenarios //Journal of Computing and Information 2(1) — 1996 — P 1110-1132

Работы автора по теме диссертации

1 Соколов В В Проверка SDL диаграмм по MSC диаграммам на основе частичной информации // Системное программирование — СПб 2004 - с 366-390

2 Терехов А Н , Соколов В В Новые возможности технологии REAL // Вестн С -Петербург ун-та — Сер 10 , 2005 — Вып 1-2 — с 64-77

3 Терехов А Н , Соколов В В Реализация стыка между MSC- и SDL-диаграммами в технологии REAL // Программирование — 2007 — № 1 - с 35-50

Terekhov А , Sokolov V Implementation of the Conformation of MSC and SDL Diagrams in the REAL Technology // Programming and Computer Software (Engl, Transl) - 2007 - № 1 - P 24-33 -DOI 10 1134/S0361768807010045

Подписано в печать 15 03 2007 Формат бумаги 60 х 84 1/16 Бумага офсетная Печать ризографическая Уел печ л 1,0 Тираж 100 экз Заказ 3944

Отпечатано в отделе оперативной полиграфии НИИХ СПбГУ 198504, Санкт-Петербург, Старый Петергоф, Университетский пр 26

Оглавление автор диссертации — кандидата физико-математических наук Соколов, Владимир Владимирович

Введение

1 Используемые формализмы

11 Определения, специфичные для части "Верификация"

1 2 Определения, специфичные для предложенного расширения MSC.

2 Верификация SDL диаграмм по MSC диаграммам

2 1 Сущее жующие подходы.

2 2 Постановка задачи.

2 3 Алгоритм верификации

2 3.1 Обоснование мех ода в терминах исходной задачи

2.3.2 Реализация.

2 3 3 Выбор начальной MSC диаграммы.

2 4 Пример

2 5 Обработка сложных (лучаев . . 44 2.5 1 Проверка при наличии в SDL коде конструкции Save 44 2 5.2 Уничтожение сообщений, не обрабатываемых в текущей ситуации.

2.5.3 На MSC диаграммах присутствует оператор параллельного исполнения.

2 б Возможные усовершенствования и дальнейшее развитие метода

2.7 Место подхода среди существующих методов

3 Генерация SDL диаграмм по MSC диаграммам

3 1 Текущее состояние проблемы

3.1 1 Однократный перенос

3.1.2 Согласование изменяющихся диаграмм

3.1.3 Обобщение результатов.

3 2 Предлагаемый подход

3.2.1 Статические данные.

3.2.2 Динамика.

3 3 Базовый алгоритм генерации

3 3.1 Требования по корректности автомата.

3 3.2 Идеи порождения базисных SDL элементов.

3.3 3 Основная картина расклейки.

3 3 4 Необходимость появления SDL элементов из основной картины расклейки.

3 3 5 Схема порождения описаний SDL элементов из основной картины расклейки

3.3.6 Алгоритмы порождения частей дерева кода.

3.3.7 Алгоритм порождения всего SDL кода.

3 4 Пример

3 4 1 MSC диаграммы

3 4 2 Недетерминированный автомат

3.4.3 Автомат без ^-переходов.

3 4 4 Детерминированный автомат.

3 4.5 Детерминированный и минимизированный автомат

3.4.6 Построенные SDL диаграммы

3 5 Сравнение с ручным программированием и оптимизация имеющегося SDL кода.

3 6 Улучшения базового алгоритма.

3.6.1 Краткий обзор базового алгоритма.

3.6.2 Косметические улучшения.

3 6 3 Порождение таймеров.

3.6.4 "Макроопределения"

3 6.5 Оптимальность автомата, "расщепление" деревьев

3 6 6 Выделение процедур

3 6 7 Детермишшизация по выходящим сообщениям

3 6.8 Параллелизм.

3.6.9 Обобщенный алгоритм разработки динамики системы

3.7 Выводы

4 Модификация MS С диаграмм для описания обратных веток

4 1 Пример использования текущего стандарта MSC и его обсуждение

4 2 Предложенное решение

4 2 1 Краткое описание расширения.

4 2 2 Неформальное объяснение понятий ''блок" и "суперблок"

4 2 3 Построение блоков при разборе грамматики . . 104 4.2.4 Совместное использование графического и текстового описаний

4.2 5 Построение конечного автомата но расширенному

MSC описанию для выделенною об ьекта

4 3 Примеры

4.3 1 Построение блоков по коду.

4 3 2 Описание примера из раздела 4.1 с помощью предложенного расширения MSC

4 4 Замечания к использованию . 4 4.1 Использование Condition 4.4 2 Корректное проектирование . 4 5 Сравнение с существующими работами 4 6 Выводы

Введение 2007 год, диссертация по информатике, вычислительной технике и управлению, Соколов, Владимир Владимирович

В последнее десятилетие в развитии программного обеспечения произошел качественный скачок. Электронный мир теперь распределен, параллелен и взаимосвязан Распределен — поскольку информация размещена во многих местах по всему миру. Параллелен — поскольку деятельность происходит во многих местах одновременно Одного потока управления теперь недостаточно ни для принятия делового решения, ни для выполнения программ. Взаимосвязан — поскольку действие в одном месте может значительно повлиять на окружающий мир. Возрастает число компаний, доверяющих критически значимые операции системам распределенных объектов предприятия Эти объектно-ориентированные системы содержат распределенные серверы и базы данных, объединенные для поддержки высокопараллельных бизнес-операций. Все большее число отраслей для осуществления своей деятельности вынуждены взаимодействовать в режиме реального времени Банки, авиалинии, телефонные компании не могут работать без интенсивного обмена информацией между всеми действующими объектами Наконец, усфойсгва реального времени встречаются теперь повсюду—в машинах, приборах, бытовой электронике, зданиях. Большинство современных систем являются системами реального времени. Проблемы их работы перестали быть узкой специализированной областью и касаются теперь каждого из нас Новый электронный мир несет с собой большие возможности, но они даются ценой высоких затрат на разработку. Основой сосуще* гвования параллельных распределенных систем являются протоколы их взаимодействия. Простые компьютерные системы, языки и модели прошлого не могут соответствовать современным требованиям. С возрастанием сложности протоколов взаимодействия потребовались специальные средства, нацеленные на описание, разработку и отладку соответствующих протоколов

Разумейся, системы, в которых использовались сложные протоколы взаимодействия, существовали достаточно давно, и проблемы, которые сейчас встали перед всей компьютерной областью, там проявились гораздо раньше Мы говорим о телекоммуникационных системах. Соответствующие проблемы там были успешно разрешены, в результате чего были созданы стандарты SDL (Specification and Description Language) [48] и MSC (Message Sequence Chart) [49]. Данные стандарты были разработаны Международным Консультационным Комитетом по Телеграфии и Телефонии, ныне ITU-T [27]. На русском языке стандарты были описаны в работах [7, 12, 4].

Конечно, данные языки не сразу достигли современного уровня, еще до получения статуса стандарта велась долгая предварительная работа, а после выпуска первой версии стандарты многократно перерабатывались и дополнялись. Оба стандарта являются хорошим балансом между аналитическими и выразительными возможностями. Это стало возможно только потому, что каждый из стандартов имеет как графическую, так и программную нотацию. Существенно, что между данными спецификациями нет никакой разницы и, при необходимое!и, можно использовать как один, так и другой вариант Это дает возможность использовать данные стандарты как средство проектирования для обсуждения графических нотаций с экспертами предметной области, так и использовать их для программирования и тестирования систем

Данные языки являются стандартом де-факто в международной телефонии Организация ITU-T использует их для спецификации других стандартов (протоколов) - UMTS, GSM, E-DSS-1, V5 2, SS7 и других. MSC и SDL широко используются в известных фирмах-разработчиках телекоммуникационного оборудования, таких как Alcatel, Ericson, Hewlett-Packard, Motorola, Nokia, Siemens. При этом следует упомянуть, что изначальная область применения данных стандартов шире, чем телекоммуникации, например, язык SDL был выбран языком спецификаций компании Боинг [4]. В России эти стандарты используются при разработке и сертификации телекоммуникационного оборудования [3].

В свете того, что все большее количество приложений становится распределенными, идет процесс интеграции данных языков в такую популярную методологию разработки программного обеспечения, как UML [25]. Изначально данный подход был создан авторами трех наиболее распространенных методологий Гради Буч (ВООСН), Джим Рамбо (ОМТ — Object Modelling Technique) и Айвар Якобсон (OOSE — Object Oriented Software Engineering) под эгидой Rational Software Corporation [26] Он должен был объединить все существенные и успешные разработки в данной области и стать стандартом языка объектного моделирования. Наряду с Rational в его создании участвовали представители множества компаний, таких как Microsoft, IBM, Hewlett-Packard, Oracle, DEC, Unisys и нескольких сотен более мелких и завершился созданием в январе 1997 года версии 1 0. На текущий момент UML используют в качестве стандартов такие гранды как Microsoft, Ilewlett-Packaid, Oiacle, SybaseLogic Works. Практически все мировые производители CASE систем (Computer Aided Software Engineering) либо уже поддерживают UML в своих продуктах, либо заявили об этом в своих планах. При этом реализованы переходы из UML в множество языков программирования, таких как С-г-г, Java, Delphi, VisualBasic, Ada.

Данная работа нацелена на языки SDL и MSC, но при этом полученные результаты также могут быть применены и для UML, что позволяет говорить о широкой области применимости предложенных алгоритмов в разработке сисхем.

Возвращаясь к классической области применимости данных стандартов для создания 1елекоммуникационного оборудования, можно привести ряд любопытных оценок Соответствующее ПО относится к категории сверхсложного, к которому предъявляются очень жесткие требования [3]

• время поиска неисправности не больше 15 минут,

• время воссыновления оборудования не больше 30 минут;

• наработка на 01каз — от 10000 часов,

• время простоя не больше 2 часов за 40 лет;

Большая часть эюй сложности приходится на описание распределенности и возможных отказов различных частей системы Поэтому важными проблемами данной области являются

• технология создания больших систем;

• проверка корректности,

• обработка ошибочных ситуаций взаимодействия.

Коллектив кафедры системного программирования и ГУП "Терком" многие годы занимаются созданием телефонных станций. У нас есть собственная технология разработки на базе стандартов SDL, MSC, UML. Она прошла долгую эволюцию, и в различное время была известна под именами RTST [18, 14] /RTSTt г [6, 5] /REAL [19, 16, 10]. При этом практическое использование данной технологии показало ее применимость не только для разработки телефонных станций, но и для других систем реального времени и информационных систем, в которых очень важен событийный аспект описания системы

Решения, предлагаемые в данной работе, получены автором путем расширения данной технологии. Результаты получены на базе практического ее использования, однако они применимы для любой другой технологии, содержащей в себе модели MSG и SDL, например для [29], либо допускающих их использование в качестве промежуточной модели, таких как в работах [45, 37, 61, 52]

Введение в модели MS С и SDL и необходимость их совместного использования

SDL (Specification and Description Language) диаграмма очень похожа на традиционные блок-схемы, но с несколькими важными расширениями: символ состояния, в котором процесс не занимает процессор, ожидая приема одного или нескольких сообщений1; символ приема сообщения и символ

В данной работе с чита< м шшлтш» сш нала (signal), традиционно ш но 1ы>( moi о н SDL, >киина.к нт-ным понятию сообщения (message), используемого в MSC посылки сообщения, как это изображено на рисунке 1 В SDL диаграммах основное внимание уделяется логике использования сообщений; логика выполнения действий, не связанных с сообщениями, детализируется лишь по мере необходимости Поэтому действие может быть атомарным, как показано на рисунке 1, так и достаточно сложным из десятков или сотен операторов

SO Начальное состояние перехода у Входные сообщения х и у Условие D Условие D . „ Посылка

Ы =0 Z г сообщения z

Соединитель

S1

Конечное состояние перехода

Рис 1. Пример SDL диаграммы

MSC диаграммы (Message Sequence Chart) позволяют описывать сценарии поведения системы во времени. Время течет сверху вниз, вертикальные линии представляют объекты системы, а между ними рисуются стрелки, обозначающие сообщения Элементарная MSC диаграмма изображена на рисунке 2 MSC диаграммы состоят из отдельных сценариев и структур, задающих последовательности выполнения этих сценариев Они широко применяются для описания протоколов различными международными организациями, в том числе для стандартов, разработанных организацией ITU-T, однако редко когда приводятся исчерпывающие описания поведения системы, включая обработку аварийных ситуаций, техобслуживания, тарификации и тд [39, 40]. И MSC, и SDL диаграммы применяются для описания динамическою поведения системы, их сравнительный анализ приведен в таблице 1. Используемые в данной работе элементы MSC и SDL диаграмм приведены в Приложении А.

В современных системах используются оба стандарта, поскольку они дают различную информацию о динамическом поведении объекта и дох

Оператор

Таблица 1: Сравнительные характеристики SDL и MSC.

MSC SDL

Описывает взаимодействие между различными частями системы; по 01 ношению к объекту данный стандарт является внешним Описывает внутренние алгоритмы каждого из объектов; по отношению к объекту стандарт является внутренним

Отображена логика взаимодействия нескольких объектов. Логика поведения каждого из них скрыта Отображена логика поведения каждого из объектов. Логика их взаимодействия скрыта

Информация о выборе линии поведения дается словесно Логика работы детализована вплоть до значений переменных

Создаются на этапе проектирования Создаются при программировании

Используются при обсуждении задачи с экспертами предметной области 11реимущсственно используются программистами иолняют друг друга Подчеркнем, чго они являются не просто различными представлениями одной и той же модели, а несут в себе разную информацию. Например, только из SDL диаграмм можно узнать о выборе одной либо другой ветви поведения. Соответствующая информация содержится в переменных, которые на MSC отсутствуют.

Для того, чтобы указать информацию, которая содержится только на MSC диаграммах, рассмотрим гииотегическую ситуацию с банком, когда для некоторых клиентов кассир сразу выдает деньги, а для других предвагом Sump с OI 02 (.3 ч -► г У

Рис. 2- Пример MSC диаграммы рительно консультируется у директора банка. В общем случае, имея SDL модели всех участников, нельзя восстановить, участвовал ли директор в процедуре выдачи денег конкретному клиенту. Можно показать, что эта задача родственна задаче о самоприменимости и алгоритмически неразрешима. Соответствующая информация хранится на MSC диаграммах, которые содержат информацию не только о том, как объекты обмениваются сообщениями, но и кто участвует в сценариях взаимодействия.

Поэтому за какой-то информацией приходится обращаться к MSC диаграммам, а за какой-то — к SDL диаграммам. Из-за этого в современных технологических средствах присутствуют оба типа диаграмм. Соответственно, возникает необходимость обеспечения их согласованности.

Обсуждение области

Для технолога2 было бы идеальным вариантом, если бы существовала некая объемлющая модель, на которую, как на трехмерный кубик, можно было бы взглянуть с одной стороны и увидеть SDL диаграммы, а с другой грани она бы давала представление в виде MSC диаграмм. На текущий момент времени подобная модель не существует, можно лишь выделить ряд подходов по согласованию MSC и SDL диаграмм в существующих CASE системах.

Обзор существующих подходов по совместному использованию MSC и SDL

Условно их можно разделить на следующие группы.

1. MSC и SDL независимы. a) MSC и SDL представляют собой отдельные независимые типы диаграмм. В этом случае их несогласованность ведет к потенциальным ошибкам.

2Так мы называем разработчика, создающего продукт с помощью технологии b) Переход от MSC диаграмм к SDL диаграммам осуществляется человеком, что повышает вероятность ошибки и очень часто приводит к неоптимальным решениям, лишнему и избыточному коду, особенно при длительной поддержке проекта.

2. Попытки создавать системы на основе MSC диаграмм с последующим синтезом SDL a) В случае, когда пытаются поддерживать весь цикл разработки на MSC, то это влечет за собой расширение стандарта MSC и перенос на MSC диаграммы кода, данных и других технических деталей [60]. После этого начинаются проблемы при увеличении количества сценариев и вытекающей нестыковке участков кода. Структура MSC малоприменима для задания на ней кода. MSC диаграммы больше отвечают на вопрос «Что может случиться?», чем на вопрос «Почему так случается?», вследствие чего они обладают избыточностью и мало приспособлены для использования на них "арифметических" данных. b) "Односторонний синтез". В этом случае один раз производится синтез SDL диаграмм но MSC диаграммам, а затем используются полученные структуры [62, 30, 60]. В таком случае внесение изменений вручную очень дорого стоит. Зачастую это приводит к полному отказу от MSC диаграмм, по которым был проведен синтез. c) "Инкрементальные алгоритмы" Стандарт MSC урезается до диаграмм, задающих только трассы3. Существуют алгоритмы [55], позволяющие добавить новую MSC спецификацию — трассу на SDL диаграммы. Данный подход работает лишь на специфическом классе задач из-за постоянного присутствия цикличности в реальных задачах. Для неурезанного стандарта MSC задача создания инкрементальных алгоритмов также рассматривалась, но была разрешена лишь для очень узкого набора из

3Под трассой имеем ввиду цепочку сообщений менений [50].

Алгоритмы, используемые в пунктах 2.с и 2.Ь [62, 30], способны провести синтез не из любых MSC описаний. Алгоритм пункта 2.а способен на это всегда. Побочным эффектом этого алгоритма является то, что в процессе его работы данные могут быть преобразованы таким образом, что в получившейся SDL диаграмме будет тяжело узнать исходную MSC диаграмму. Сразу отметим, что невозможность осуществить синтез во многих разумных ситуациях является очень слабым местом, поэтому следует отдавать предпочтение вариантам алгоритма 2.а

3. Алгоритмы сравнения используемых MSC и SDL диаграмм для проверки соответствия. a) На основе MSC диаграмм строятся трассы, а затем полученные трассы "накладываются"4 на SDL диаграммы [40, 39, 41] Если трасса укладывается, то все хорошо. Если нет — это считается ошибочной ситуацией. Подобный способ недостаточно эффективен, поскольку добавление где-либо отладочного сообщения нарушает последовательность сообщений на трассе и считается, что SDL модель не соответствует MSC спецификациям [72]. Этим методом невозможно проверить случай, когда SDL модель является реализацией сразу нескольких ролей на MSC диаграммах. b) Встречалась идея модификации предыдущего алгоритма с разрешением пропускать сообщения. Она была описана в [68], но широкого распространения не получила из-за невысокой достоверности результата. c) Использование одного из алгоритмов [44], связанных с анализом внутренних состояний протокола, при этом параллельно выполняются две модели — MSC и SDL. В процессе выполнения проверяется, что принятые и посланные сообщения одинаковы.

4Имеется ввиду посимвольное совпадение сообщений трассы с сообщениями диаграммы

Данные алгоритмы изначально разрабатывались для проверки непротиворечивости моделей, и перестают работать для проверки соответствия SDL диаграмм MSC при наличии разногласий между MSC и SDL, типа отсутствия цикличности на MSC документации и ее присутствия на SDL модели.

Условия построения CASE системы

Сформулируем условия, которым должна соотвествовать CASE система, в которой применяются и MSC, и SDL модели, на основе интеграции имеющихся подходов и собственного опыта разработок. Должны присутствовать следующие возможности:

1. использовать SDL модель независимо от MSC модели. Например, если некоторый стандарт задан в виде SDL диаграмм, то должна быгь возможность использовать готовую SDL модель, без того, чтобы начинать строить MSC модель;

2. автоматически строить SDL модель по MSC модели. Это существенно ускоряет скорость разработки;

3. проверять согласованность описаний на MSC и на SDL, причем с учетом изменений, появляющихся в течение жизненного цикла программы.

Проблемные места

При этом следует выделить следующие проблемные места, на которые следует обратить внимание.

• Разработать процедуру верификации5 так, чтобы она позволяла более надежно проверять соответствие моделей при их рассогласовании, что неизбежно в течение жизненного цикла. Существующие подходы по верификации являются достаточно "хрупкими", наличие даже

5Данный термин используем в качестве сокращения фразы "проверка соотвествия" незначительных изменений приводят к тому, что модели считаются несогласованными. Проверка должна быть более гибкой и учитывать возможность незначительного различия моделей, вызванного различными целями MSC и SDL моделей.

• Разработать процедуру генерации6 SDL по MSC так, чтобы можно было получить ряд SDL моделей, подходящих к текущей ситуации, а не единственный вариант, выдаваемый автоматически.

• Сущее I вующие подходы по генерации и верификации базируются на неявном предположении, что есть MSC модель, которая эквивалентна SDL модели. На самом деле это не так, и стандарт MSC крайне неудобен для создания полного описания поведения, на нем можно описать лишь несложные варианты взаимодействия. Соответственно, язык описания MSC должен быть расширен, чтобы сделать возможным и генерацию, и верификацию.

Данные проблемы были успешно решены. Предложенные решения рассматриваются в данной работе Их интеграция между собой и с технологией описана в работах [21, 20].

Работа с частями моделей, предназначенными для описания статических данных системы

Данная кандидатская работа нацелена на решение проблем в области стыковки динамик MSC и SDL моделей. То есть алгоритмов в области обмена сообщениями Хотя данные модели имеют средства описания статических частей системы, но проблем в данной области гораздо меньше, поэтому данного момента мы лишь бегло коснемся. С точки зрения автора, в рамках технологии не может быть нескольких различных описаний статик, поэтому в рамках технологии REAL статическая часть системы — это отдельная самостоятельная модель. В последствии данным описанием пользуются как MSC, так и SDL модели. На рисунке 3 изображены различные

Под генерацией понимаем создание одной модели по другой модели подходы по совместному использованию MSC и SDL в рамках технологии, а так же их интеграция с описанием статической части системы.

Рис. 3: Интеграция подходов в технологии REAL

Научная новизна

Научная новизна диссертационной работы заключается в следующем.

1. Разработана новая математическая модель верификации, которая работает в большем классе случаев, порождаемых ситуациями жизненного цикла программы, и позволяет проводить проверки, когда другие методы не могут работать.

2. Впервые поставлена задача настройки генерируемого SDL кода под требования технолога. Разработана оригинальная система генерации для построения SDL диаграмм на основе MSC модели, удобных для последующей работы с ними. Система позволяет интерактивно влиять на получаемый SDL код, так, чтобы обеспечить легкость его прочтения и понимания человеком в рамках текущей задачи. Она позволяет также провести оптимизацию уже имеющегося SDL кода.

3. Разработано новое расширение MSC, которое позволяет создавать описания реальных систем за счет большей описательной гибкости, чем в других моделях. Именно наличие данного расширения дает возможность использовать и генерацию, и верификацию, поскольку позволяет эффективно описывать обратные ветви, и на основе этого создавать реальные системы.

4. Представлен оригинальный взгляд на совместное использование MSC и SDL моделей, использующий разработанные алгоритмы верификации, генерации, расширения MSC и сочетания статических данных MSC и SDL.

Данные решения были проинтегрированы с технологией и апробированы при создании телефонной станции "Юнивер-А" — многоканального радиоудлинителя телефонных линий. Результаты 1 и 2 применимы в ряде других систем, в которых система, заменяющая MSC, сводится к конечно-автоматному описанию. Результат 2 также применим для систем, если в них SDL модель является промежуточной.

Благодарности

Автор выражает признательность следующим людям, помогавшим ему при создании данной работы.

• Терехов Андрей Николаевич — за поддержку и веру в перспективность метода;

• Булычев Дмитрий Юрьевич — за жесткие требования к формализму и структуре моих работ;

• Захаров Михаил Николаевич — за помощь в получении статей,

• Иванов Александр Николаевич — за консультации по внутренним структурам и алгоритмам технологического средства REAL;

• Алексеева Светлана Леонидовна — за консультации по применению REAL'a в реальных задачах и за критику моей кандидатской работы;

• Шалунов Леонид Борисович — реализовавшего импорт текстовых SDL диаграмм в технологическое средство REAL.

А так же благодарит всех тех, кто участвовал с создании цепочки технологий RTST — RTST-н— REAL, на базе которых и были созданы данные решения.

Заключение диссертация на тему "Совместное использование MSC и SDL моделей при разработке событийно-ориентированных систем"

4.6 Выводы

В завершение данной главы кратко перечислим все плюсы предлагаемого подхода:

• дается возможность более гибко описывать обратные ветви,

• он позволяет более понятно и компактно описывать взаимодействие сценариев, используя механизм сообщений из MSC и конструкции из операторов, подобные конструкциям из ЛЯВУ,

• после получения исчерпывающих MSC описаний в рамках технологии можно получить заготовки SDL кода, доработка которых для реального SDL минимальна;

• внедрение подобного описания как стандарта позволит более гибко использовать MSC диаграммы и создавать на базе них исчерпывающие стандарты для телекоммуникационных систем.

Данный подход значительно усиливает возможности генерации и верификации, предложенные в данной работе, и повышает возможности стадии проектирования технологии REAL.

Заключение

В диссертации предложена модель стыковки MSC и SDL диаграмм на базе технологии REAL. Последовательно рассматриваются три проблемные области верификация SDL программ по MSC документации; генерация SDL диаграмм по MSC диаграммам; получение полного описания поведения объекта на MSC модели. В данных областях были предложены следующие решения:

• разработана математическая модель верификации SDL по MSC, позволяющая осуществлять проверки в тех случаях, когда другие известные подходы не работают,

• модель верификации расширена для обработки сложных случаев предметной области,

• создан алгоритм автоматизированной генерации SDL кода по конечному автомату с возможностью улучшения структуры генерируемого кода;

• разработаны алгоритмы по выделению процедур и обработке параллельных учасхков MSC при генерации SDL кода;

• разработана математическая модель, на базе которой было создано расширение MSC диаграмм. Данное расширение позволяет создавать полное описание поведения объекта в реальных системах.

Эти решения были реализованы, интегрированы с технологией REAL, произведено их использование в реальных промышленных системах

Библиография Соколов, Владимир Владимирович, диссертация по теме Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей

1. Ахо А., Сети Р., Ульман Д. Компиляторы. Принципы, технологии, инструменты - М Вильяме, 2003 - 1.BN 5-8459-0189-8, 0-201-10088-6. - 768 с.

2. Гагарский Р.К Комплекс средств визуализации для модели параллельных процессов — дипл. р., каф. системного программирования, мат-мех ф-т, СПбГУ 2004 - 26 с.

3. Гойхман В К)., Гольдштейн Б С., Дымарский Я С, Сибиряко-ва Н.Г. Сертификационные испытания коммутационного оборудования средств связи — СПб : Вестник МАИСУ, 2002. — № 4.

4. Гольдштейн B.C. Сигнализация в сетях связи. — М., 1997. — 423 с.

5. Иванов А.Н , Кознов Д В., Мурашова Т.С Поведенческая модель RTST // Записки семинара кафедры системного программирования «CASE-средсгва RTSTV-r» СПб., Издательство СПбГУ, 1998 -Вып. 1 - с 37-49

6. Иванов А.П., Кознов Д.В., Мурашова Т.С., Парфенов В.В., Терехов А.Н. Объектно-ориентированное расширение технологии RTST // Записки семинара кафедры системного программирования «CASE-средства RTST—т » СПб, Издательство СПбГУ, 1998 - Вып. 1. -с 17-36

7. Карабегов А В., Тер-Микаэлян Т.М. Введение в язык SDL — М.: Радио и связь, 1993 184 с.

8. Касьянов В.Н Оптимизирующие преобразования программ — М Наука, 1988 336 с

9. Касьянов В Н., Евстигнеев В Л Графы в программировании: обработка, визуализация и применение — СПб.: БХВ Петербург, 2003. -1104 с

10. Кознов Д.В. Визуальное моделирование компонентного программного обеспечения' Дис канд физ -мат. наук — СПбГУ, 2000 — 82 с.

11. Кузнецов О.П , Адельсон-Вельский Г.М. Дискретная математика для инженера — М.: Энергоатомиздат, 1988 — 480 с.

12. Мансуров Н Н., Майлингова O.JI. Методы формальной спецификации программ- языки MSC и SDL — Издательство АО "Диалог-МГУ", 1998. 125 с.

13. Мансуров II. Синтез исполняемых SDL спецификаций по сценарным моделям // Тр ин-та Системного Программирования — 1999.

14. Парфенов В В , Терехов А П. RTST — технология программирования встроенных систем реального времени // Системная информатика. — СПб.: 1997 — N°5. — с. 228-256.

15. Рейуорд-Смит В Дж Теория формальных языков. — М.: Радио и связь, 1988. 128 с.

16. Романовский К Ю., Ивановский Б Д., Кознов Д В., Долгов П.С Обзор нотаций методологии Real // Технический огчег — 1999.

17. Соколов В.В. Проверка SDL диаграмм по MSC диаграммам на основе частичной информации // Системное программирование. — СПб.: 2004.-с 366-390.

18. Терехов А Н RTST — технология программирования встроенных систем реального времени // Записки семинара кафедры системного программирования «CASE-средства RTST t » » — СПб., Издательство СПбГУ, 1998. Выи 1. - с. 3-17.

19. Терехов А Н и др. REAL методология и CASE средство разработки информационных систем и ПО систем реального времени // Программирование 1999. - №5. — с. 45-51.

20. Терехов А Н., Соколов В.В. Новые возможности технологии REAL // Вести. С -Петербург, ун-та Сер 10 , 2005 - Вып 1-2. - с 64-77.

21. Терехов А.П., Соколов В.В Реализация стыка между MSC- и SDL-диаграммами в технологии REAL // Программирование 2007 — № 1. - с. 35-50

22. Terekhov A., Sokolov V. Implementation of the Conformation of MSC and SDL Diagrams in the REAL Technology // Programming and Computei Software (Engl., Transl) 2007 - № 1. - P. 24-33. -DOI. 10 1134/S0361768807010045.

23. Аннотация средства KLOCWork на сайте SDL Forum. http://www sdl-forum oig/Tools/klocwork.htm

24. Проекты Института Сис1емного Программирования Российской Академии Наукhttp: / / www.ispras.ru / groups / case / projects.html?27/2

25. Сайт компании, представляющей средство KLOCWork. http.//www klocwork.com/

26. Сервер группы OMG, занимающейся развитием методологии UML. Стандарты, публикации, средства. http://www omg com

27. Сервер компании Rational Rose, одной из ведущих компаний средств разработки для методологии UML http.//www rational.com

28. Сервер организации по стандартизации ITU-T http://www.itu-t.org

29. Concurrent Languages in the Heterogeneous Specification, http //mint сь man не uk/Projuts/UPC/Ldiiguagtb/CoiKiirrentLriiigudges html

30. Use Case Maps (UCMs) нотация. Определения, публикации, средства. http://www.useCaseMaps org/index.shtml

31. Abdalla M., Khendek F., Butler G. New Results on Deriving SDL Specifications fioin MSCs // Proc. of 9th SDL Foiuni — 1999. — P. 55-67.

32. Battista G., Eades P., Tamassia R., Tollis I. Algorithms for drawing graphs: An annotated bibliography. // Proc. in Computational Geometry: Theory and Applications 4 — 1994. — P. 235-282.

33. Ben-Abdallah H., Lone S. Syntactic Analysis of Message Sequence Chart Specifications // Technical Report 96-12 — University of Waterloo — Electrical and Computer Engineering — 1996. — 39 p.

34. Bourduas S., Khendek F., Vincent D. From MSC and UML to SDL // Proc. of IEEE Annual International Conference on Computer Software and Applications (COMPSAC'2002) — Oxford, UK — 2002. — P. 153-158.

35. Damm W., Harel D. LSCs: Breathing Life into Message Sequence Charts // Proc. in 3rd IFIP International Conference on Formal Methods for Open Object-based Distributed Systems (FMOODS'99) — Kluwer Academic Publishers, 1999. — P. 293-312.

36. Daveau J.-M., Marchioro G., Valderrama C., Jerraya A. VHDL generation from SDL specifications // Proc. of the XIII IFIP Conf. on Computer Hardware Description Languages (CHDL'97) — Toledo, Spain — 1997.

37. Dulz W., Gruhl S., Lambert L., Sollner M. Early performance prediction of SDL/MSG specified systems by automated synthetic code generation // Proc. of 9th SDL Forum — 1999. — P. 457-472.

38. EG 201 015 Vei. 1.2.1, Methods for Testing and Specification (MTS); Specification of protocols and services; Validation methodology for standards using Specification and Description Language (SDL); Handbook — 1999. — 28 p.

39. ETR 184 : Methods for Testing and Specification (MTS); Overview of validation techniques for European Telecommunication Standards (ETSs) containing SDL 1995. — 27 p.

40. ETS 300 414, Methods for Testing and Specification (MTS); Use of SDL in European Telecommunication Standards Rules for testability and facilitating validation — 1999. — 99 p.

41. Elkoutbi M., Khriss, I., Keller R.K. Generating User Interface Prototypes from Scenarios // Proc. in 4th IEEE International Symposium on Requirements Engineering (RE'99) — Limerick, Ireland — 1999. — P. 150-158.

42. Formal Methods Specification and Analysis Guidebook for the Verification of Software and Computer Systems, Volume II: A Practitioner's Companion. — 1997. — NASA-GB-001-97. — 245 p.

43. Holzmann G. Design and Validation of Computer Protocols // Prentice-Hall, 1991 — ISBN 0-13-539834-7. — 512 p.

44. Horn W., Svantesson В., Kumar S., Jantsch A., Hemani A. Hardware synthesis of an ATM multiplexer from SDL to VHDL: A case study // Proc. of the IEEE Computer Society Workshop On VLSI '99 — Orlando, FL, USA. 1999. P. 100-105.

45. ITU-T MSC2000R3 Draft Z.120: Message Sequence Charts ITU-T Recommendation Z.120. — 1999.

46. ITU-T Recommendation Z.100: Appendices I and II: SDL Methodology Guidelines, SDL Bibliography. — 1993. — 129 p.

47. ITU-T Recommendation Z.100: Specification and description language (SDL). 1999. - 244 p.

48. ITU-T Recommendation Z.120: Message Sequence Chart (MSC). — 1999. — 136 p.

49. Khendek F. Vincent D. Enriching SDL Specifications with MSCs // Proc. of 2nd Workshop of the SDL Forum Society on SDL and MSC (SAM 2000) — 2000. — P. 305-319.

50. Koskimies K., Makinen E. Automatic Synthesis of State Machines from Trace Diagrams // Software Practice and Experience, 24(7) — 1994. — P. 643-658.

51. Svantesson В., Kumar S., Hemani A., A methodology and Algorithms for efficient interprocess communication synthesis from system descriptions in SDL // Proc. of VLSI Design — Chennai, India — 1998. — P. 78-84.

52. Kurshan R. Computer-Aided Verification of Cooidinating Processes // Princeton Series in Computer Science, 1994. ISBN 0691034362. — 270 p.

53. Leue S., Mehrmann L., Rezai M. Synthesizing ROOM models from message sequence chart specifications // Proc. in 13th IEEE Conf. on Automated Software Engineering — Honolulu, Hawaii — 1998. — P. 192-195.

54. Li J., Horgan J. Applying formal description techniques to software architectural design // Computer Communications — Vol. 23 — №12. — 2000 -P 1169-1178

55. Ilelouet L., Jard C., Conditions for synthesis of communicating automata from HMSCs // Proc. in 5th International Workshop on Formal

56. Methods for Industrial Critical Systems (FMICS) — Berlin — 2000. — P. 203-224.

57. Mansurov N. Automatic Synthesis of SDL from MSC in Forward and Reverse Engineering // Publ. in 1st International Conference on Visual Formal Methods — Eindhoven Technical University, 1999. — P. 44-64.

58. Mansurov N. Formal methods for accelerated development of telecommunications software // Publ. in Collected Research Papers of the Institute for System Programming — 1999.

59. Mansurov N., Vasura D. Approximating (H)MSC semantics by Event Automata // Proc. SDL and MSC workshop (SAM 2000) — 2000.

60. Mansurov N., Zhukov D. Automatic synthesis of SDL models in Use Case Methodology // Proc. of 9th SDL Forum — 1999. P. 225-240.

61. Muth A. SDL-based Design of Application Specific Hardware for Hard Real-Time Systems // Dissertation. — Lehrstuhl fur Realzeit-Computorsysteme, Technische Universitat Miinchen — 2002. — 208 p.

62. Robert G., Khendek F., Grogono P. Deriving an SDL specification with a given architecture from a set of MSCs // Proc. of 8th SDL Forum — 1997. P. 197-212.

63. Roychoudhury A., Thiagarajan P. Communicating Transaction Processes // Proc. in IEEE International Conference on Application of Concurrency in System Design (ACSD'2003) 2003. — P. 157-166.

64. Rumbaugh J., Jacobson I., Booch G. The Unified Modeling Language Reference Manual — Addison-Wesley, 1999. — 576 p.

65. Schonberger S., Keller R., Khriss I. Algorithmic Support for Model Transformation in Object-Oriented Software Development // Proc. in: Theory and Practice of Object Systems (TAPOS). — John Wiley and Sons. — 1999.

66. Sehmid R., Ryser J., Berner S., Glinz M., Reutemann R., Fahr E. A Survey of Simulation Tools for Requirements Engineering // Technical Report 2000.06 — Zurich, Institut fur Informatik, 2000.

67. Schumann J., Whittle J. Automatic Synthesis of Agent Designs in UML // Proc. in 1st Goddard Workshop on Formal Approaches to Agent-Based Systems — NASA Goddard — 2000. — P. 148-162.

68. Sinclair D., Stone В., Clynch G. An Object Oriented Methodology from Requirements to Validation // Proc. of the 2nd Object Oriented Information Systems Conference (OOIS'95). — Springer, 1995. — P. 265-286.

69. Some S., Dssouli R. An Enhancement of Timed Automata generation from Timed Scenarios using Grouped States // The Electronic Journal on Networks and Distributed Processing — 1997.

70. Some S. Dssouli R., Vaucher J. Prom scenarios to timed automata: building specifications fiom useis requirements // Pioc. in Asia Pacific Software Engineering Conference (APSEC'95) — 1995. — P. 48-57.

71. Some S., Dssouli R., Vaucher J. Toward an Automation of Requirements Engineering using Scenarios //Journal of Computing and Information 2(1) — 1996. — P. 1110-1132.

72. Telelogic Tau 4.2 documentation, March 2001.

73. Turner K. Formalising the Chisel Feature Notation // Proc. in 6th International Workshop on Feature Interactions in Telecommunications and Software Systems (FIW'00) — Glasgow, Scotland, UK : IOS Press, Amsterdam, 2000. — P. 241-256.

74. Whittle J., Shumann J. Generating Statechart Designs From Scenarios // Proc. in: 22th International Conference on Software Engineering (ICSE 2000) — Limerick, Ireland : ACM Press — 2000. — P. 314-323.

75. Используемые элементы MSC и SDL диаграмм

76. MSC и SDL стандарты достаточно объемлющи и различаются в зависимости от года издания, поэтому приведем список элементов, которые используем в данной pa6oie

77. А.1 Поддержанный синтаксис MSC

78. Посылка сообщения от объекта 01 объекту 02 Графически изображена на рисунке А.2 Над стрелкой обычно пишется название сообщения.

79. Прием сообщения объектом 01 от объекта 02 Графически изображен на рисунке А.З. Над стрелкой обычно пишется название сообщении

80. Ссылка на диаграмму. Подразумевается, что эта диаграмма специфицируется в другом месте Графически изображена на рисунке А 4.

81. Возможность склейки нескольких диаграмм (Condition) Графически изображена на рисунке А.5.

82. Возможность выбора одного варианта поведения из нескольких возможных Графически изображена на рисунке А.6.

83. MSC диаграммы часто сопровождаются пояснительными комментариями на естественном языке.

84. А.2 Поддержанный синтаксис SDL

85. Данная модель обычно содержит вставки на АЯВУ и, в частности, работу с переменными, соответствующими АЯВУ, в который осуществляется генерация. В рамках данной работы этот вопрос не является существенным.

86. А.2.1 Графическое описание1 Состоянияa) Начальное состояние Изображено на рисунке А.7.b) Обычное сосюяние Изображено на рисунке А.8c) Завершающее состояние Изображено на рисунке А.9

87. Посылка сообщения Изображена на рисунке А 10.1.т

88. Рис А.1 Экземпляр объекта на MSC диаграмме с завершением существования (справа) и без (слева)

89. Рис. А 2. Посылка сообщения от объекта 01 обьек!у 02 на MSC диаграмме

90. Рис. А.З* Прием сообщения от обьекта 02 объектом 01 на MSC диаграмме

91. Рис. A.4 Ссылка на другую MSC диаграмму

92. Рис. А.5: Возможность склейки нескольких MSC диаграммjj (asc 1 (а« 2 lax !

93. Рис. А.6' Возможность выбора одного варианта поведения из нескольких возможных на MSC диаграмме1. CUD

94. Рис. A.7: Начальное состояние SDL1. CiD

95. Рис. A.8 Обычное SDL состояниеX

96. Рис А.9. Завершающее состояние SDL

97. Прием сообщения. Изображен на рисунке All.

98. Ветвление в коде в зависимости от условия (условий) Изображено на рисунке А 12.

99. Соединитель (Connector) Изображен на рисунке А 13 б Соедини 1ельные линии Изображены на рисунке А. 141.Menage 1

100. Рис. А.10: Посылка сообщения на SDL диаграмме1. Manage 1

101. Рис. А 11: Прием сообщения на SDL диаграмме

102. Рис А. 12 Всмвчение в SDL коде в зависимости от условия (условий).1. Connector31. Рис А 13' SDL соединитель

103. Рис А. 14: Соединительные линии SDL диаграммы

104. А.2.2 Формат текстового описания

105. Определим текстовое описание SDL. Для этого приведем пример используемого текстового описания SDL комментариями в С-нодобном стиле. Полноценная грамматика SDL дана в стандарте 48.start,output Query, nextstate State.l;

106. Описание стартового состояния //Посылка сообщения //Переход в состояние State,1state Statel; input Reply;join Conn2,

107. Описание (обычного) состояния Statel //Прием сообщения //Переход на соединительstate State3, input Bl;output CI; join Conn2, input B2,output C2; join Conn2,

108. Ниже описываются действия после приема //сообщения В1

109. Ниже описываются действия после приема //сообщения В2state State5,input Finishreply, stop;

110. Переход в завершающее состояниеconnection Conn2; decision,

111. Приведем грамматическое описание для синтаксического анализатора уасс. У,st art program /*

112. Procedure should return nothing

113. KALTBEGIN statement KALTEND »listaltstatement : listaltstatement altstatement I altstatement ialtstatement : KALT statement jmscoptstatement : KOPTBEGIN statement KOPTEND1. Список иллюстраций1 Пример SDL диаграммы.102 Пример MSC диаграммы.11

114. Интеграция подходов в технологии REAL . . .172 1 MSC диаграммы 1, 2 для проверки соответствия.42

115. Преобразования автомата для уничтожения сообщений . 482 9 Пример MSC диаграммы с параллельным исполнениемучастков.49

116. Место SDL и MSC моделей в технологии REAL . . 523 2 Главная MSC диаграмма для генерации.59

117. Детализирующие MSC диаграммы для генерации.593 4 Автомат, полученный из MSC диаграмм с рисунков 3 2 и 3.3 6035 „Классический"результат генерации .603 6 Наш результат генерации.60

118. Порождение SDL состояния (слева) и аналогия происхождения данного рисунка (справа).663.83.113 123 133 143 153163.173.183.193.203.214 1