ЯЗЫКИ И СИСТЕМЫ ПРОГРАММИРОВАНИЯ
У л :
ЯЗЫК DYNAMIC-REAL И ЕГО ПРИМЕНЕНИЕ ДЛЯ ВЕРИФИКАЦИИ SDL-СПЕЦИФИКАЦИЙ РАСПРЕДЕЛЕННЫХ
СИСТЕМ *
© 2014 г. В.А. Непомнящий, Е.В. Бодин, С.О. Веретнов
Институт систем, информатики им. А. П. Ершова СО РАН 630090 Новосибирск, проспект Академика Лаврентьева, 6 E-mail: vnep@iis.nsk.su Поступила в редакцию 07.10.2013
Представлен язык спецификаций распределенных систем Dynamic-REAL (dREAL), который расширяет разработанный ранее язык Basic-REAL посредством динамических конструкций порождения и уничтожения экземпляров процессов. Описан программный комплекс SRDSV2 (SDL/REAL Distributed Systems Verifier), предназначенный для моделирования, анализа и верификации SDL-спецификаций распределенных систем. Этот комплекс включает транслятор из языка SDL в язык dREAL, систему автоматического моделирования dREAL-спецификаций и транслятор из языка dREAL во входной язык Promela системы верификации SPIN. Описано применение этого комплекса для верификации динамической системы управления сетью касс-терминалов.
1. ВВЕДЕНИЕ
В последние годы заметно возрастает роль формальных методов, применяемых для разработки распределенных систем, таких как, например, коммуникационные протоколы. Это связано с тем, что для современных распределенных систем усложняется документирование, анализ и верификация. Для преодоления указанных трудностей используются такие языки, как SDL, UCM и UML, принятые в качестве стандартов международной организацией ITU (International Telecommunication Union).
На практике применялись различные версии языка SDL [1, 2, 3]. Верификация выполнимых спецификаций, представленных на языке SDL, заключается в проверке корректности их ключевых свойств и является известной открытой проблемой современного программирования.
Развитие формальной семантики языка SDL необходимо для разработки формальных методов анализа и верификации. Интересный подход для описания формальной семантики SDL об-
* Работа была частично поддержана грантом РФФИ 11-07-90412-Ukr f а.
суждается в [2]. Однако при использовании этого подхода формальная семантика языка SDL остается громоздкой.
Для доказательства свойств статических SDL-спецификаций применяется метод проверки моделей [4]. Однако непосредственное применение этого метода часто приводит к значительным трудностям ввиду громоздкости моделей SDL-спецификаций. Для преодоления этих трудностей используется трансляция SDL-спецификаций в модельные языки. В работе [5] описана трансляция статических SDL-спецификаций (с ограничениями на взаимодействие процессов) в системы конечных автоматов, к которым применяется метод проверки моделей. В работах [6, 7] представлен модельный язык IF, который базируется на расширенных временных автоматах. На базе языка IF реализован программный комплекс, включающий транслятор статических SDL-спецификаций с определенными ограничениями в язык IF [6, 7]. Этот транслятор был расширен посредством добавления конструкции save языка SDL [8]. Верификация статических SDL-спецификаций с помощью промежуточного языка IF и из-
вестной системы проверки моделей SPIN [9, 10] рассматривается в работах [11, 12, 13]. В работах [12, 13] была описана верификация используемого на практике коммуникационного протокола Mascara. Таким образом, проблема применения метода проверки моделей к верификации динамических SDL-спецификаций остается открытой. Заметим, что в работе [14] описан подход, который базируется на понятии базовых протоколов и позволяет проводить дедуктивную верификацию SDL-спецификаций коммуникационных протоколов с помощью системы VRS. Идея нашего подхода к проблеме верификации SDL-спецификаций состоит в разработке модельных языков, ориентированных на верификацию, которые были бы комбинированными, т.е. включали подъязыки выполнимых и логических спецификаций. Такой комбинированный язык спецификаций BasicREAL (bREAL) был представлен в [15, 16], где описана структурная операционная семантика выполнимых bREAL-спецификаций в виде систем переходов, которая позволила доказать важные семантические свойства. В этих работах представлен дедуктивный метод верификации свойств прогресса выполнимых спецификаций языка bREAL. Упрощенные версии этого языка, названные Real92 и Elementary-REAL, представлены в [17] и [18].
Цель настоящей работы - представить язык Dynamic-RE AL (dREAL), полученный расширением языка Basic-REAL посредством динамических конструкций порождения и уничтожения экземпляров процессов, и программный комплекс SRDSV2 (SDL/REAL Distributed Systems Verifier), предназначенный для моделирования, анализа и верификации SDL-спецификаций распределенных систем, который использует язык dREAL в качестве промежуточного языка. Про-тотипная версия этого комплекса была представлена на конференции МС02009 [19].
Данная работа состоит из восьми разделов. В разделе 2 описывается язык dREAL и его формальная семантика. Раздел 3 дается обзор программного комплекса SRDSV2. Основные компоненты этого комплекса описаны в разделах 4-6. В разделе 4 описан транслятор из языка SDL в язык выполнимых спецификаций dREAL. В разделе 5 представлена система
автоматического моделирования выполнимых спецификаций dREAL. Раздел 6 посвящен описанию системы моделирования и верификации, использующей систему SPIN. В разделе 7 представлена SDL-спецификация динамической системы управления сетью касс-терминалов и описано применение программного комплекса SRDSV2 к моделированию и верификации этой системы. В разделе 8 обсуждаются достоинства нашего подхода и перспективы его развития.
2. ЯЗЫК DYNAMIC-REAL
Язык Dvnamic-REAL (dREAL) состоит из языка выполнимых спецификаций для представления распределённых систем и языка логических спецификаций для представления их свойств.
Для описания систем в языке dREAL определены две синтаксические формы - текстовая и графическая. Выполнимая спецификация состоит из блоков, соединенных между собой и с окружающей средой каналами. Средствами языка dREAL обеспечивается многоуровневое описание спецификации. Блок может содержать другие блоки и процессы, которые работают параллельно и взаимодействуют друг с другом и с внешней средой посредством обмена сигналами через каналы. С каждым действием процесса ассоциируется временной интервал, который задает продолжительность выполнения действия.
Выполнимая спецификация на языке dREAL имеет иерархическую структуру и состоит из заголовка, контекста, диаграммы и подспецифи-каций. Заголовок определяет имя и вид спецификации: блок или процесс. Контекст состоит из определений типов и описаний переменных и каналов. Диаграмма блока состоит из маршрутов, соединяющих подблоки между собой и с внешней средой. Диаграмма процесса состоит из переходов, которые включают имя состояния, тело, временной интервал и список (возможно, пустой) следующих состояний. Имя состояния служит меткой, причём одно состояние может метить несколько переходов. На переход могут накладываться условия выполнения (WHEN) такие, как проверка наличия сигнала в канале для чтения сигнала или непустоты канала для записи сигнала, а также логическое выражение, использующее значения переменных. Тело перехо-
да имеет следующие варианты: READ - чтение сигнала (с параметрами) из канала, WRITE - запись сигнала (с параметрами) в канал, CLEAN -очистка выходного канала, ЕХЕ - исполнение программы, изменяющей значения переменных, хотя содержимое каналов при этом не меняется, STOP - прекращение работы экземпляра процесса. Подробно понятие программы описано в [20].
Каждый экземпляр процесса может порождать или уничтожать экземпляры процессов в своем блоке. Подобно языку SDL, в dREAL количество экземпляров, существующих с самого начала, и максимально возможное количество экземпляров определяется в заголовке процесса. Создание процесса производится в теле перехода вида ЕХЕ посредством оператора CREATE имя_ процесса. Уничтожение экземпляра процесса осуществляется посылкой специального сигнала Kill в соответствующий канал, т.е. тело перехода имеет вид WRITE Kill INTO имя_ канала[рг<1], где pid - уникальный идентификатор экземпляра процесса. При этом сигналы, посланные уничтожаемым экземпляром процесса, не уничтожаются и могут быть прочитаны получателем сигналов. Тогда как сигналы, адресованные уничтожаемому экземпляру процесса, пропадают.
Версия языка dREAL, подробно описанная в [21], расширена за счёт добавления макроопределений-процедур, не содержащих обращений к каналам.
Процедура может быть вызвана из программы, которая находится в теле перехода вида ЕХЕ, посредством оператора CALL. Процедура может содержать вызов другой процедуры, но при этом рекурсия, явная или неявная, не допускается.
Заметим, что в язык dREAL добавлены операторы ASSERT и PRINT для отладки и тестирования спецификаций.
В языке dREAL используется единственная единица времени tick. Таким образом, временной интервал может содержать только следующие единицы времени: NOW7 ("сейчас"), INF ("временной интервал не ограничен"), tick. Также добавлена возможность использования служебной переменной ТЮК (значение глобальных часов) в выражениях.
В dREAL есть предопределённые переменные-идентификаторы типа Pid для данного процесса:
- SELF - pid данного процесса;
- OFFSPRING - последний идентификатор процесса, порожденного данным процессом;
- PARENT - идентификатор процесса-родителя;
- SENDER - идентификатор процесса, от которого был получен последний сигнал к данному процессу.
Также в dREAL можно использовать обычные переменные типа Pid.
Язык логических спецификаций расширяет конструкции логики ветвящегося времени CTL [4, 10] за счет использования временных интервалов и средств динамических логик. Формулы этого языка строятся из предикатов с помощью булевских операций, модальностей по моментам времени ("всегда" или "иногда") и по возможным поведениям выполнимых спецификаций ("для всех поведений" или "для некоторых поведений"), а также кванторов (существования и всеобщности) по выделенным переменным и по экземплярам процессов.
Формальная семантика языка логических спецификаций dREAL описана в [21].
3. ПРОГРАММ
Для дальнейшего прочтения статьи необходимо приобрести полный текст. Статьи высылаются в формате PDF на указанную при оплате почту. Время доставки составляет менее 10 минут. Стоимость одной статьи — 150 рублей.