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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Пусть даны две переменные d и x. Каждый тик в синхронной модели они обновляются следующим образом (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 [25] для разработки надежных систем в таких критических областях как аэрокосмическая, ядерная энергетика, поезда без водителей.

Lustre базируется на парадигме программирования, которая представляет преобразования в виде модели синхронного потока данных. Эта парадигма полагается на следующие моменты:

• Модель встроена в цикл, состоящий из трех фаз: прием множества текущих входных данных, вычисление выходных данных и их выдача.

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

• Предполагается, что эти потоки имеют одинаковую длину. Они синхронизируются на временной шкале, основанной на максимальном времени вычисления.

• Модель описывается просто списком выходных выражений для второй фазы периодического режима выполнения. Благодаря синхронизации можно однозначно ссылаться на текущие и прошлые значения внутри выражений.

Вычисления выходов могут потребовать предыдущих входных значений входов и выходов. В этом случае отношение между входами и выходами не являются функциональными, а зависят от истории сигналов. Если v есть выражение потока, то последовательность обозначается как v1, v2, v3, ... .

• 3 означает поток констант 3, 3, 3, ... .

• a+b означает поток a1+b1, a2+b2, a3+b3, ... .

• Пусть v = expr есть выражение для потока v. Тогда в других выражениях v может быть безопасно заменен на expr в соответствии с принципом замещения.

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

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

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

• симулятор;

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

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

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

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

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

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

node rising (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,...).

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

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

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

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

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

.

Рис. 73. Временная диаграмма rising

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

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

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

Рис. 75. Верификации rising

Преобразование линейных систем после дискретизации в программы на 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.0-> pre(u) );

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

v = c*x – e*y;

tel.

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

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

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

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

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

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

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

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

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

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

Рис. 77 Модель газовой горелки в 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’, где Т – температура, вычисленная в предыдущем цикле.