2.3. Асинхронный язык проектирования sdl

В качестве примера рассмотрим язык SDL (Specification and Description Language, стандартизован ITU) основанный на CFSM с асинхронной передачей сообщений. Наряду с текстовым представлением SDL поддерживает и графическое представление проектов. Базовыми элементами SDL являются процессы, представляющие компоненты MoC как EFSM. На рис. 63 показаны графические символы, используемые для представления EFSM.

Н а рис.64 приведено графическое представление в виде процесса (Process P) на SDL временного автомата Автоответчика из примера на рис. 62. Временные переменные (часы) X и Y на SDL представляют два таймера X и Y.

Рис. 63. Символы графической формы SDL

Рис. 64. Модель Автоответчика на SDL

Оператор SET (NOW+4, X), например, запускает таймер X на интервал равный 4, а оператор RESET(X) останавливает таймер X. Процессы SDL представляют EFSM, поэтому они могут выполнять преобразования над данными. Переменные могут быть объявлены локально в процессах. Многие типы данных предопределены, так же они могут быть определены

пользователем. Синтаксис для объявлений и операций подобен другим языкам. На рис. 65 показаны объявления, оператор присвоения и условный оператор.

Рис. 65. Объявление, присвоение и условный оператор SDL

В общем, описание на SDL состоит из взаимодействующих процессов или EFSM. Процессы могут посылать сигналы другим процессам, образуя CFSM. Семантика взаимодействия процессов основана на асинхронной передаче сообщений и реализована в виде очередей типа FIFO (first-in first-out), ассоциированных с процессами (на каждый процесс своя очередь). Сигналы, посылаемые определенному процессу, поступают в соответствующую очередь как на рис. 66.

Рис. 66. Взаимодействие процессов SDL

Каждый процесс выбирает из очереди запись и проверяет, совпадает ли она с одним из входов назначенных текущему состоянию. Если да, то выполняется соответствующий переход и генерируется выход. Выбранная запись игнорируется, если нет совпадения ни с одним из назначенных входов. Запись при этом может остаться в очереди, если используется механизм запоминания SAVE.

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

На практике это не реализуемо и это одна из проблем реализаций проектов на SDL.

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

2.4. Синхронный язык проектирования Lustre

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

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

Такой идеалистический взгляд на одновременность гарантирует детерминированное поведение. Это является ограничением, если сравнивать с моделью CFSM, в которой каждая FSM имеет свой собственный «тактовый сигнал». Синхронный язык отражает принцип работы синхронных схем.

Пусть даны две переменные d и x. Каждый тик они обновляются следующим образом:

d’ = -d если x=0 ; d иначе

x’ = x + d

x: 0 -1 0 1 0 -1 0 1

d: -1 1 1 -1 -1 1 1 1

В 80-х годах прошлого века был предложен синхронный язык Lustre [28] для разработки надежных систем в таких критических областях как аэрокосмическая, ядерная энергетика, поезда без водителей.

Lustre является языком потока данных. Модель потока данных «естественным образом» отражает пути, по которым данные «перетекают» от одного компонента к другому. Каждый компонент преобразует данные от одного или нескольких путей. Программа потока данных специфицируется ориентированным графом, в котором вершины (узлы), называемые actor (узел-оператор), представляют вычисления, а дуги представляют коммуникационные каналы. Каждый процесс в графе разбивается на последовательность активаций (firing), которые являются элементарными действиями. Каждая активация производит и уничтожает специальные маркеры (token).

ESTEREL Technologies разработала коммерческий инструмент SCADE для моделирования, тестирования и верификации синхронных систем использующих Lustre. SCADE де-факто стала европейским стандартом. Она используется в Airbus, Merlin-Gerin, «Сухой», .... SCADE является комплектом программ, работающих под Windows, и состоит из следующих программных компонент:

• GUI интерфейс для графической манипуляции с моделями Lustre;

• симулятор;

• инструмент для верификации;

• генератор исполняемого кода;

• инструмент генерации отчетов.

Lustre опирается на 3 базовые концепции.

flow(поток) – последовательность значений данных. Все значения потока принадлежат к одному типу, например, integer flow: 0,1,2,3,....

node(узел) – базовый кирпич любой программы. Lustre является функциональным языком: каждый узел определяет функцию, которая получает входные потоки и производит выходные потоки, например:

node EDGE (X:bool) returns (Y:bool) ;

let

Y = false -> X and not pre(X);

tel

Оператор pre (предыдущее значение): если A = (a1,a2,a3,...,an,...) тогда pre(A) = (nil,a1,a2,a3,...,an-1,...). Оператор -> (инициализация flow): если A = (a1,a2,a3,...,an,...) и B = (b1,b2,b3,...,bn,...), то A->B = (a1,b2,b3,...,bn,...).

Функция EDGE примера обнаруживает моменты изменения символов входного потока Х с 0 на 1 и формирует соответствующий выходной поток Y. Однажды определенный узел становится оператором и может быть вызван в другом узле. На рис. 67 приведено графическое представление EDGE в SCADE.

Рис. 67. Графическое представление EDGE в SCADE

cycle (цикл) – один шаг выполнения программы. В каждом цикле вычисляются новые значения и добавляются в каждый поток. Каждый цикл соответствует тику.

Модели систем могут быть смоделированы в SCADE. Симулятор вычисляет значения каждого потока в каждом цикле. Разработчик может ввести значения для входных потоков и наблюдать выходные потоки. Результаты моделирования узла EDGE:

X: F T T F F T T

Y: F F F F F T F

re(X): nil T T T F F T

not pre(X): nil T F F F T T F

X and not pre(X): nil T F F F F T F

False: F F F F F F F F

false -> X and not pre(X): F T F F F F T F

Cycle: 0 1 2 3 4 5 6 7

На рис. 68 приведена временная диаграмма работы EDGE.

Рис. 68. Временная диаграмма EDGE

Для модели, которая была отлажена с помощью симулятора, SCADE может выполнить формальную валидацию (верификацию). Для этого необходимо спроектировать поток (называемый монитором), который принимает истинное значение тогда и только тогда, когда интересуемое свойство обнаруживается. Если такой поток всегда принимает истинное значение, то свойство подтверждается. Например, для узла EDGE (или rising) мы хотим убедиться, что выходной поток никогда не будет иметь значение true во время двух соседних циклов. На рис. 69 приведен узел Monitor, формирующий потока Prop, для доказательства этого свойства.

Рис. 69. Узел Monitor для верификации EDGE

Monitor затем подключают к узлу rising (рис. 70) и убеждаются, что выход Monitor всегда принимает значение true.

Рис. 70. Верификации EDGE

Преобразование линейных систем после дискретизации в программы на Lustre является очевидной задачей. Если система выражена в форме z-преобразований, то оператор 1/z транслируется в 0.0 -> pre(). Пусть например передаточная функция второго порядка имеет вид:

H(z)= (a*z^2 + b*z +c)/( z^2 + d*z +e),

y= H(z)*x,

у=a*x+(b*x-d*y)*1/z+(c*x-e*y)*1/z^2, отсюда программа:

const a, b, c, d, e: real.

node SECOND_ODER (x: real) returns (y: real) ;

let

y = a*x + (0.-> pre(u);

u = b*x – d*y + (0.-> pre(v);

v = c*x – e*y;

tel.

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

• Как и модель является детерминированным.

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

• Чистое отображение между кодом и моделью.

• Последнее позволяет производить трассировку программы при отладке.

Рассмотрим простой пример проектирования контроллера «Газовая горелка» (рис. 71) [29]. Контроллер должен сохранять температуру внутри заданного интервала (например, между 50 и 60 градусами включительно). Изначально температура находится в заданном интервале. Контроллер преобразует входной поток Т (значения температуры) в выходной булев поток В.

Рис. 71. «Газовая горелка»

Предлагается следующий алгоритм работы: когда температура достигает 50 °С горелка включается, когда температура достигает 60 °С, горелка выключается. На Lustre это выглядит так:

B = false -> (if T=50 then true else if T=60 then false else pre(B))

На рис. 72 представлена модель газовой горелки в SCADE.

Рис. 72 Модель газовой горелки в SCADE

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

– когда горелка включается, температура повышается;

– когда горелка выключается, температура понижается.

– горелка переключается мгновенно;

– когда нагрева нет температура в баке уменьшается со скоростью 1°С в единицу времени;

– когда происходит нагрев температура в баке повышается со скоростью 3°С в единицу времени;

– датчик температуры точный.

Описание датчика температуры:

• вход temp – температура в баке, действительная величина (real);

• выход reading – отсчет;

• преобразование – temp = reading.

Описание горелки:

• вход switch – команда контроллера

• выход heating – the «пламя», булева величина (Boolean);

• преобразование – heating = switch.

Описание бака:

• вход heated – булева величина, индицирующая нагрев или его отсутствие;

• выход temp – температура;

• преобразование – temp = 55 -> (if heated then pre(temp)+3 else pre(temp)-1) .

Моделирование в SCADE позволяет найти ошибку: для некоторой начальной температуры никогда не достигается температура точно в 60 °С и горелка никогда не выключится. Это связано с ограничениями на частоту дискретизации CPU. Поэтому необходимо вместо ‘if T=60 then false’ перейти к нестрогому неравенству: ‘if T>=57 then false’, где Т – температура, вычисленная в предыдущем цикле.