Виды описания языка базовых протоколов

Преимущество языка SDL – в удобстве создания больших моделей. Он обладает такими востребованными и и полезными для разработки свойствами, как наглядность и модульность, оснащен расширенным набором упрощающих описание вспомогательных конструкций (которые сводятся к более простыми – так называемый «синтаксический сахар»). Однако именно эти преимущества затрудняют анализ и верификацию.

Формальное описание модели системы также можно задать в виде базовых протоколов. Базове протоколы представляют собой выражения Хоаровских троек: α →< и > β, α-предусловие, и –процесс (действие), β – постусловие. Преимущество этого формализма – в простоте и эффективности использования методов верификации: язык использует базовый набор структур данных и операций над ними и в тоже время обладает достаточной выразительной мощностью для описания систем, специфицированных в таких инженерных языках, как MSC, SDL, UML. Однако такой подход затрудняет процесс построения больших моделей, так как одним базовым протоколом описывается всего один переход системы.

Представление требований в форме базовых протоколов базируется на теории взаимодействия агентов и сред. Базовый протокол представляет собой выражение вида ∀x(α →< u > β), где x – список (типизированных) параметров, α иβ – формулы базового логического языка, u – процесс протокола (конечное поведение композиции нескольких агентов и среды, обычно задается с помощью MSC диаграмм). Формулаα называется предусловием, а формулаβ – постусловием базового протокола. Сам базовый протокол может рассматриваться как формула темпоральной логики, выражающая тот факт, что если состояние системы имеет разметку, удовлетворяющую условию α, то процесс u может быть инициирован и после его завершения состояние системы будет удовлетворять условию β. В качестве базового языка используется язык многосортного исчисления предикатов первого порядка.

35) Трансляция SDL – спецификаций в язык базовых; 36) Структурная часть языка БП (базовый протокол)

SDL имеет описание как структурной, так и функциональной части модели.

В языке базовых протоколов (БП) структурная часть специфицируется в описании среды, а функциональная часть определяется переходами состояний среды и агентов, заданными пред- и постусловиями БП.

Семантика поведения агентов соответствует поведению процессов – они

работают асинхронно; язык предусматривает создание/уничтожение агентов (операции create(), stop()).

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

Структурная часть языка БП является двухуровневой – среда со взаимодейст-

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

37) Статистический анализ и преобразование SDL – модели; 38) Процесс аннотирования SDL – модели

Разделим нормализацию на 6 этапов, приведенных ниже. Каждый этап

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

На первом этапе нормализации строятся траектории (последовательности

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

Результатом данного этапа нормализации является множество отношений сигнал – отправитель – получатель, и далее все сигнальные маршруты (signalroute) и каналы без задержек (nodelay channel) могут быть элиминированы.

На втором этапе нормализации осуществляется так называемое выравнивание, во время которого все процессы, процедуры и каналы выносятся из блоков на

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

Третий этап – элиминация конструкций input *, input *(x), save *, save *(x). Переход input * копируется для всех возможных входных сигналов процесса кроме тех, которые явно указаны на других переходах вида input s из данного состояния (здесь s – имя сигнала). Save * транслируется в save z, где z – это, в противопоставление input *, список всех возможных входных сигналов процесса кроме тех, которые явно указаны на других переходах вида input s из данного состояния. В одном состоянии

конструкции input * и save * встречаться не могут.

Конструкции input *(x) и save *(x) элиминируются аналогичным образом,

принимая во внимание то, что сигналы из списка x исключаются.

Следующий, четвертый этап – нормализация выражений с вызовами процедур (procedure). Пусть есть следующая SDL-конструкция:

task a:= E(x₁, …, x_n, f₁(y¹₁, …, y¹_n1), …, f_m(y^m₁, …, y^m_nm));

где E – выражение, все x_i, y^j_k – локальные переменные процесса (или выражения,

которые посредством этой нормализации свернутся в переменные), fj – вызываемые процедуры. Для нормализации такой конструкции вводятся переменные f’1, …,f’m.

Далее она транслируется в последовательность операторов task:

task f’1:= call f1(y11, …, y1n1);

task f’m:= call fm(ym1, …, ymnm);

task a:= E(x1, …, xn, f’1, …, f’m);

Здесь в последовательности присваиваний f’j сохранен порядок вызовов процедур fj в выражении E. В последнем операторе task выражение E уже не содержит вызовов. Такая нормализация допускает и обрабатывает аналогичным образом использование выражений с вызовами в качестве фактических параметров процедур.

Пятый этап – преобразование средств мониторинга переменных других про-

цессов (import/export). В соответствии с Z.100 [4], для интерпретации этих операций создаются неявные переменные, сигналы и состояния. Фактически выполнение экспортно-импортной операции берет на себя конкретная реализация SDL и делает это с помощью обмена сигналами между процессом-экспортером и процессом-импортером. Операция export вызывает сохранение значения экспортируемой переменной в неявной переменной. Операция import транслируется в посылку сигналазапроса и переход в состояние ожидания сигнала-ответа со значением импортируемой переменной. При этом процесс-экспортер отсылает значение, сохраненное во время операции export (а не текущее).

На шестом, последнем этапе нормализации выделим главный (control flow – «управленческий») атрибут, неявно присутствующий в SDL-спецификации – поток управления процесса. Его можно ввести явно, если добавить в исходную модель метки и операторы join так, чтобы иметь возможность объединить линейную последовательность выполнения операторов в один базовый протокол (последовательность без конструкций, вызывающих ветвление или интерливинг с другими процессами), не нарушая при этом семантики SDL. Так, одноуровневые конструкции state помечаются одной меткой, аналогично одноименные метки используются для одноуровневых конструкций input. Единственным нарушением семантики SDL является транслирование конструкции decision. Мы задаем одноименные метки для одноуровневых конструкций для выявления недетерминизма (по семантике SDL выполняется первый удовлетворенный переход) и неполноты (конец конструкции задает неявный переход по умолчанию). Такие свойства могут стать потенциальной причиной ошибки целевого кода. Так, например, в современных промышленных стандартах рекомендуется явно задавать значения по умолчанию.

Предложенный процесс нормализации предусматривает возможность

аннотирования SDL-модели. Аннотации могут быть расставлены на любых

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

Дата добавления: 2015-08-13