Конференции ИВТ СО РАН

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

27 - 29 ноября 2007 года, Новосибирск

Тезисы докладов

Информационные технологии

Моделирование и анализ SDL-спецификаций распределенных систем с помощью промежуточного языка Dynamic-REAL

Веретнов С.О.

Институт Систем Информатики СО РАН (Новосибирск)

Для разработки надежных распределенных систем применяется стандартный язык SDL, который предназначен для описания структуры и функционирования систем реального времени, в частности сетей связи. Верификация выполнимых спецификаций, представленных на языке SDL, заключается в проверке корректности их ключевых свойств и является известной открытой проблемой современного программирования. Идея перспективного подхода к проблеме верификации SDL-спецификаций состоит в разработке модельных языков, ориентированных на их верификацию, которые были бы комбинированными, т.е. включали подъязыки выполнимых и логических спецификаций. Примером комбинированного модельного языка спецификаций служит язык Dynamic-REAL (dREAl) [1], разработанный в лаборатории теоретического программирования ИСИ СО РАН как расширение языка Basic-REAL cite{NEP2}. Он базируется на языке SDL и логике ветвящегося времени CTL. Его ядро - язык выполнимых спецификаций, достоинство которого - полная структурная операционная семантика выполнимых спецификаций в виде систем переходов.

Целью данной работы является описание системы моделирования коммуникационных протоколов, представленных на языке SDL. В качестве языка для входной спецификации взято подмножество языка SDL с динамическими конструкциями такими, как порождение и уничтожение процессов. В качестве промежуточного языка взят язык dREAL. Система состоит из двух основных компонент: транслятора с языка SDL в язык dREAL и системы моделирования dREAL-спецификаций.

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

Система моделирования выполнимых спецификаций языка dREAL состоит из следующих модулей: синтаксический анализатор, семантический анализатор, графический интерфейс, управляющий модуль. Эта система содержит также модуль автоматической симуляции, который позволяет проверять выполнение некоторых условий, заданных пользователем. Система реализована на языке С++. Синтаксические анализаторы построены генератором синтаксических анализаторов Bison.

Система была успешно тестирована на следующих примерах: RE-протокол, Sliding Window Protocol, Протокол Касса-Пассажир и его динамическое расширение на сеть касс. Система является консольным приложением.

Работа частично поддержана грантом РФФИ 07-07-00173.

Литература
1. Nepomniaschy V.A., Bodin E.V. Dynamc-REAL, a language for specification and verification of distributed systems, Report of Institute of Informatics Systems, Novosibirsk, 2007(to appear).
2. Непомнящий В.А., Шилов Н.В., Бодин Е.В. REAL: язык для спецификации и верификации систем реального времени, Системная информатика, Новосибирск, Наука, т.7, 2000г, 174-224 с.

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

Ваши комментарии
Обратная связь

[Головная страница]
[Конференции]