«Верификация автоматных программ в контексте синхронного программирования ...»

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

Событийно-управляемые системы можно обнаружить в широком спектре задач. Например, в операционной системе Windows события используются для уведомления приложения о различных действиях пользователя, как нажатие клавиш на клавиатуре, клик кнопки мыши. Процессы широкого класса Unix-подобных операционных систем используют сигналы для уведомления о совершении некоторого события [29]. Нажатие пользователем комбинации клавиш + в программе эмуляции терминала обычно приводит к отправлению сигнала SIGINT активному процессу. В недрах операционной системы сигналы используются для реализации механизма виртуальной памяти. Бизнес-приложения содержат многочисленные примеры использования событий.

В целом, можно сказать, что потенциальная область применения АП чрезвычайно широка. Автоматный подход может быть эффективно реализован на практически любом языке общего назначения. Особенно удобно кодировать автоматы с помощью оператора выбора. Для языка программирования C++ такой оператор называется switch [34], что послужило причиной возникновения второго названия АП Switch-технология.

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

Объектно-ориентированное программирование с явным выделением состояний Популярность объектно-ориентированный методологии программирования сказалась на АП, что привело к появлению объектно-ориентированного программирования с явным выделением состояний [43].

Основная идея этого направления в представлении различных компонентов автоматной программы в виде объектов. В качестве объектов могут рассматриваться автоматы, состояния, переходы, события. Фантазия разработчика позволяет практически все рассматривать как объекты. Объектноориентированное программирование приносит с собой целый ряд новых концепций: полиморфизм, инкапсуляция, наследование. Было предложено немало вариантов, оперирующих этими понятиями. Автоматы могут наследовать друг другу, тем самым достигается повторное использование кода. Состояния могут быть сложными. Одни состояния вкладываются в другие, образуется иерархия по вложенности. Здесь можно использовать как идеи наследования, так и более традиционное отношение включения.

Повторное использование кода играет важную роль. Были предложены несколько вариантов библиотек с “заготовками” для разработки автоматных программ. Возможно сохранение и более сложной функциональности в библиотеке.

Стоит отметить несколько работ этого направления: [25, 38]. Реализованы примеры, демонстрирующие применение ООП с явным выделением состояний: система управления турникетом [1], задача “синхронизация цепи стрелков” [10], задача об обедающих философах [27].

UniMod Развитием ООП с явным выделением состояний стало появление инструментального средства разработки автоматных программ UniMod. Его можно рассматривать как заявку на то, что АП готово для широкого использования.

Наиболее удачные идеи развития switch-технологии нашли свое воплощение в этом проекте. Поэтому состояние проекта UniMod может служить показателем зрелости автоматной технологии в целом.

Интересно провести небольшое исследование на тему: “Для чего предназначен UniMod”.

Появление switch-технологии можно ассоциировать с изданием книги [41].

Switch-технология изначально предназначалась для алгоритмизации и программирования задач логического управления [41]. В работах [39, 40] АП было распространено на реактивные системы. Со временем были обнаружены другие применения АП. Инструментальное средство UniMod появилось для поддержки автоматного программирования [12]. Сложно найти точные указания на то, для построения каких программ был создан проект.

Согласно главному сайту UniMod [68], долгосрочная цель проекта заключается в создании унифицированной методологии процесса разработки приложений, призванной заполнить пропасть, лежащую между фазами проектирования (design) и разработки, существующую в настоящее время. Ключевыми технологиями проекта UniMod называются: модельно-ориентированный подход (Model Driven Architecture), язык UML и универсальные вычисления (universal computing). UniMod адаптирует switch-технологию для использования языка UML в качестве языка описания моделей. UniMod воплощает идею запускаемого, или исполняемого, UML [11]. Ивар Якобсон, один из создателей языка UML, назвал исполняемый UML одним из перспективных направлений ближайшего будущего.

На сайте проекта UniMod [68] разработчики рекомендуют применять этот инструмент для создания:

• автономных приложений на Java с графическим и консольным пользовательским интерфейсом;

• клиент-серверных приложений на Java;

• приложений для платформы Symbian.

Там же на сайте [68] не рекомендуется использовать UniMod для решения задач:

• разработки компиляторов, поскольку для этой области уже существуют специализированные инструменты;

• построения диаграмм классов (Problem domain Class Diagrams design), т.е. не стоит использовать UniMod как обычный UML-редактор.

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

В UniMod можно писать любые приложения, в том числе широко распространенные сейчас бизнес-приложения, главное, активно использовать автоматы для кодирования сложной логики. Универсализация АП это одновременно хорошо и плохо. Хорошо потому, что удачную идею теперь можно опробовать на множестве различных задач. А плохо потому, что размывается и так очень непрочное теоретическое основание switch-технологии. По UniMod не заметно, чтобы разработчики в реализации следовали какой-либо формальной модели.

1.1.3. Сложившаяся практика применения Был выполнен анализ примеров, поставляемых с плагином UniMod [68].

Кроме того, были рассмотрены некоторые UniMod-проекты с сайта [30]. По результатам анализа можно прийти к таким выводам.

Все проекты используют автоматы для реализации логики приложения.

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

Многие приложения реализуют графический пользовательский интерфейс. Используется стандартная библиотека Java Swing. Применение графической библиотеки в данном случае оправданно, т.к. она предоставляет множество готовых решений пользовательского интерфейса. Понятно также то, что АП не всегда удачно сочетается с существующими системами. Применение Swing в данном случае более важно, чем верность switch-технологии.

Этим можно объяснить значительную долю Java-кода в приложениях.

Тем не менее, в рассмотренных программах существует не мало мест, где применение АП было возможно, но не было использовано авторами проектов. Подтверждением тому служит небольшое число автоматов в программах. Большинство проектов используют один, реже два автомата.

Интеграция АП и ООП не везде прошла удачно. Некоторые проекты демонстрируют формальное использование источников событий. Действительная генерация событий происходит в различных местах программы.

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

Проблеме верификации автоматных программ стали уделять внимание сравнительно недавно. В книгах [37, 41] вопрос верификации не поднимается. В то же время, задачи логического управления часто предъявляют критические требования к надежности программного обеспечения. Цифровые устройства широко используются в современной жизни. Им отводятся ответственные роли и цена ошибки в программном обеспечении может быть очень высока.

1.2.1. Подходы к верификации автоматных программ Задача верификации автоматных программ находится в процессе исследования. Можно выделить два центра научной деятельности. Это кафедра Теоретической информатики Ярославского государственного университета и кафедра Технологий программирования Санкт-Петербургского государственного университета информационных технологий, механики и оптики. Обе группы достигли определенных результатов.

В работе [7] рассматривается техника верификации автоматных программ, состоящих из одного конечного автомата. Применяется модификация языка CTL, что решает “трудности с выполнением композиции автоматов”.

Данное изменение также упрощает интерпретацию результатов проверки в том случае, когда найден контрпример. Один автомат это сравнительно простая модель, поэтому можно ограничиться использованием простых алгоритмов. Описывается преобразование автомата в структуру Крипке, написание темпоральных свойств на языке CTL, верификация по модели (метод “Model Checking”) и построение сценария для исходного автомата, если был найден контрпример. Техника верификации демонстрируется на примере универсального инфракрасного пульта для бытовой техники [8].

Работа [13] предлагает технологию верификацию автоматных программ, разработанных для UniMod. Если быть точным, то объектом верификации является не вся программа, написанная на UniMod, а только отдельный автомат, взятый изолированно. Автомат, согласно правилам построения программы, может содержать вложенные автоматы, поэтому даже один автомат обладает достаточно большими выразительными возможностями. В качестве верификатора выбран Bogor. Он позволяет расширять свой входной язык за счет описания дополнительных типов данных, к тому же удачно интегрируется с UniMod. Сам процесс верификации заключается в выполнении автоматной программы при различных входных данных. Интерпретацию автоматной программы выполняет все то же инструментальное средство UniMod. Надо заметить, что интерпретация программы, язык Java, очевидно, замедляют процесс проверки. Поэтому такая технология проигрывает по скорости проверки верификаторам, работающим с простыми типами данных. Однако, как утверждают авторы статьи, программы на практике имеют такой размер, что время проверки вполне приемлемо.

На конференцию “Компьютерные науки и технологии” [17] были представлены современные взгляды на проблему верификации автоматных программ.

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

Существует удачный опыт использования верификатора SPIN. Планируется создание верификатора автоматных программ на основе уже существующего верификатора, например, SPIN или Bogor.

Среди работ, посвященных верификации автоматных программ необходимо также отметить [6, 24].

Исследования в ЯрГУ уделяют основное внимание методу Model Checking.

Разберем несколько работ.

Работа [18] предлагает иерархическую модель автоматных программ. Это одна из первых работ, посвященных формализации понятия автоматной программы. Как уже неоднократно упоминалось, автоматное программирование предлагает технологию построения программ. Однако само понятие автоматной программы не имеет четкого определения. Если мы хотим использовать метод Model Checking для проверки, необходима формальная модель программы. Именно такая модель предлагается. Автор статьи развивает идею вложенных автоматов и объекта управления. За историю автоматного программирования предлагалось немало вариантов комбинирования различных понятий. Можно сказать, что иерархическая модель напоминает взаимодействие автоматов в UniMod. Вложенные автоматы подробно описывались в [41].

Коротко модель можно описать так. Существует главный автомат A0.

Он может управлять своими вложенными автоматами. Каждый вложенный автомат может иметь свои вложенные автоматы и т.д. В результате получается иерархическая система. Различные ветви дерева автоматов не пересекаются. Каждый автомат, кроме A0, имеет ровно одного родителя. Отдельно существует объект управления, который является источником событий для автомата A0. Все автоматы имеют возможность читать состояние объекта управления и оказывать на него предусмотренные воздействия. Отношение вложенности позволяет родительскому автомату вызывать вложенные автоматы для обработки какого-нибудь события. Отношение вызываемости напоминает идею процедурного программирования. В статье разбирается пример управления кофеваркой.

Развитие идеи можно найти в работе [19]. Автоматная программа очень удобна для применения метода проверки на моделях. Предлагается структура Крипке автоматной модели. Для спецификации свойств используется язык темпоральной логики CTL. Описание свойств демонстрируется на примере системы управления кофеваркой.

Работа [4] продолжает изучение иерархической модели автоматной программы. Исследуется возможность спецификации структурных и семантических свойств автоматных программ с помощью логики LTL. Разбирается пример системы управления банкоматом. Верификация выполняется инструментом SPIN.

Работа [9] является еще одним развитием иерархической автоматной модели. UniMod выбран в качестве инструментального средства разработки автоматных программ. Придуман и реализован механизм преобразования диаграмм UniMod в CPN-модель. В качестве верификатора используется система CPN/Tools. Подход демонстрируется на примере системы управления кофеваркой.

Разработана программа, предназначенная для преобразования моделей автоматных программ во внутренний язык программы верификатора CPN/ Tools. Поддерживается чтение и сохранение моделей автоматных программ в XML-формате, формате Microsoft Visio и т.д. Получено свидетельство о регистрации программы [31].

Результаты работы регулярно обсуждаются на семинаре “Моделирование и анализ информационных систем”.

1.3. Синхронный подход Синхронное программирование применяется для создания реактивных систем, приложений реального времени, систем управления [44, 47, 49, 50, 72, 87, 89]. Целевая система представляется синхронной моделью. В первом приближении это черный ящик с набором входных и выходных сигналов, имеющий внутреннее состояние (см. раздел 1.3.4). Синхронный подход накладывает ряд ограничений на среду функционирования системы. Ниже описываются основы синхронного подхода.

1.3.1. Сигналы Для взаимодействия с окружающий средой применяется единственный способ сигналы. Входные сигналы устанавливаются окружающей средой и читаются системой. Выходные сигналы генерируются системой, читаются окружающей средой. Обычный сигнал имеет статус присутствия. Сигнал может либо присутствовать, либо отсутствовать. В дополнение каждый сигнал может нести значение определенного типа, например, целое число. Значение сигнала может изменяться только тогда, когда статус сигнала “присутствует”. В остальных случаях значение сигнала не меняется, но оно всегда есть!

Существуют также специальные типы сигналов: чистые сигналы и сенсоры.

Первые не имеют значения, вторые статуса. Значение сенсора может свободно меняться.

1.3.2. Временная модель Синхронный подход использует дискретную временную модель. Каждый отдельный момент времени называется инстентом (от англ. instent). Работа системы в каждый инстент называется реакцией (от англ. reaction). Можно говорить: “реакция системы на входные сигналы”. Для системы время течет как строго упорядоченная последовательность инстентов. Реакция в каждый инстент заключается в вычислении значений выходных сигналов текущего инстента и состояния системы в следующий инстент. Вычисление однозначно определяется входными сигналами и внутренним состоянием системы в текущий инстент. Реакции в разные инстенты непосредственно независимы друг от друга, но связаны историей, которая хранится как состояние системы.

До этого момента мы говорили только о логическом времени. В отношение реального времени возможны две разных реализации: управляемая событиями (рис. 1.1) или таймером (рис. 1.2).

Рис. 1.1. Модель синхронной системы, управляемой событиями Рис. 1.2. Модель синхронной системы, управляемой таймером 1.3.3. Гипотеза нулевой задержки Считается, что все действия в пределах инстента выполняются мгновенно и одновременно. Длительность любой реакции равна нулю. Каждый инстент атомарен, т.е. все действия, запланированные в данном инстенте, выполняются как единое целое.

1.3.4. Модель синхронной системы Любая синхронная система может быть разбита на две взаимодействующие части (рис. 1.3): функциональную логику и память. Функциональная логика это правила, по которым вычисляются значения выходных сигналов и состояние в следующий инстент. Вычисление однозначно для данных значений входных сигналов и состояния системы. Вычисление повторяется в каждый инстент, имеет нулевую длительность. Память имеет специальный регистровый тип. В пределах инстента сигналы от памяти остаются постоянными. Новое значение, определяемое в текущем инстенте, ячейки памяти получат только в следующем инстенте. Таким образом удается избежать мгновенно обратной связи между входом и выходом логического блока. Заметим, что логический блок не хранит внутри себя какого-либо состояния между инстентами. Его функция только вычислительная.

1.3.5. Параллельность Использование параллельных ветвей вычислений часто является удобным при проектировании разных типов систем (реактивных, реального времени и др.). Поэтому языки синхронного программирования должны поддерживать конструкции языка, позволяющие удобно выражать параллельность такое решение было принято в 80-х годах прошлого века [50]. В зависимости от области применения, это могут быть диаграммы потока данных, иерархические автоматы или некоторый императивный вид синтаксиса, принятый в инженерном сообществе.

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

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

1.3.6. Структура системы Крупные системы удобно строить из составных блоков. Синхронное программирование позволяет использовать этот подход. Каждый составной блок является подобием целой системы. У него есть входы и выходы, блок имеет состояние. Пусть X, Y и U векторы входных, выходных сигналов и внутреннее состояние соответственно. Верхний индекс номер блока, нижний индекс номер инстента. f и g функции от входных сигналов и внутреннего состояния. Тогда можно записать:

Набор выходных сигналов в текущий инстент (n) и состояние блока в следующий инстент (n+1) вычисляется по набору входных сигналов и состоянию в текущий инстент. Это верно для любого блока (i) и любого инстента (n).

Различные блоки соединяются друг с другом посредством входов и выходов. Выходной сигнал одного блока может являться входным сигналом для одного или более других блоков. Следовательно, входной сигнал может быть общим для нескольких блоков. Пусть символ в скобках обозначает номер сигнала в векторе. Например, Y (k) k-й сигнал вектора выходных сигналов Y.

Тогда или На рис. 1.4 показана композиция двух синхронных блоков. Пунктирными стрелками отмечены связи между логическими частями разных блоков.

Здесь кроется проблема: возможно появление цикла. Таким образом, композиция синхронных блоков в общем случае не является синхронной системой. Существует несколько подходов к решению этой проблемы. Язык Esterel предлагает одно из них.

1.4. Синхронный подход в языке Esterel 1.4.1. Язык Esterel Язык Esterel относится к семейству синхронных языков [52, 53]. Это императивный язык, предназначенный в первую очередь для описания потока управления [55]. Все характеристики синхронного подхода применимы в равной степени к языку Esterel. Не будем их повторять. Обратим внимание только на те особенности, которые являются специфическими для языка Esterel.

Основным типом данных в языке Esterel является сигнал. Он может принимать два состояния: “присутствует” и “отсутствует”, или “true” и “false” или “0” и “1”. Можно использовать любое из обозначений. Присутствие сигнала является событием, отсюда терминология. Статус любого сигнала в любой реакции однозначно определен. Сигнал признается присутствующим, если он установлен окружением, либо явно генерируется программой. В противном случае, сигнал признается отсутствующим.

Система всегда ведет себя функционально [50]. Для любого допустимого состояния системы и значения входных сигналов однозначно определяется следующее состояние и выходные сигналы. Иначе говоря, каждая реакция является детерминированной. Семантическая проверка программы на языке Esterel возлагается на компилятор. Это сложная задача. Статический анализ может обнаружить мертвое состояние в программе (deadlock), однако динамическая проверка может показать, что это состояние никогда не достигается, поэтому программа имеет шансы оказаться правильной.

Проверка программы на нарушение функциональности поведения называется анализ зависимостей (causality analysis). Ее выполняет компилятор [54, 82].

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

Можно организовать сколько угодно параллельных потоков выполнения. Различные потоки взаимодействуют при помощи сигналов. Сигнал, генерируемый одним из потоков, мгновенно распространяется на все остальные потоки. Сигналы из других потоков рассматриваются наравне с сигналами из окружения. Это входные сигналы. Такое поведение называется синхронной широковещательной рассылкой сигналов (synchronous broadcast). Даже при наличии нескольких потоков выполнения поведение программы остается детерминированным. В начале каждой реакции каждый поток пробуждается в том состоянии, где он был оставлен в предыдущей реакции, выполняется обычный императивный код (вычисление выражений, операторы ветвления и присваивания), и наконец, каждый поток либо завершается, либо останавливается на одном из операторов ожидания до следующей реакции.

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

Пример разработки протокола на языке HDLC приведен в [51].

Программный пакет для разработки Esterel-программ свободно доступен на сайте института Inrea [74]. Раздел, посвященный языку Esterel: [88]. Зеркало сайта http://esterel.org (в настоящее время сайт не действует), посвященного языку Esterel: [66].

1.4.2. Верификатор Xeve Верификатор Xeve предназначен для проверки программ на языке Esterel.

Он свободно распространяется в наборе с компилятором и другими утилитами для разработки программ [67].

О работе верификатора известно мало. Описание, приводимое ниже, взято из руководства по верификатору [56].

Esterel-компилятор преобразует программу в систему логических уравнений с защелками (latchs), которая неявно определяет конечный автомат. Xeve работает с этим неявно определенным автоматом. Используется библиотека TiGeR, которая предоставляет эффективные структуры и алгоритмы для символьной манипуляции конечными автоматами, используя BDD (Binary Decision Diagrams). На входе верификатор получает набор логических уравнений, представленных в формате BLIF (Berkeley Logical Interchange Format).

Xeve предлагает две главные функции верификации.

Первая функция заключается в минимизации конечного автомата на основании понятия бисимуляционной эквивалентности (bisimulation equivalence), которая определяет группы неразличимых состояний. Минимизированный конечный автомат явно генерируется в текстовом формате FC2. При помощи инструмента ATG получившийся граф можно просмотреть в графическом виде.

Вторая функция верификации заключается в проверке статуса выходных сигналов. Можно проверить, что определенный выходной сигнал когда-либо генерируется или всегда отсутствует. Можно также проверить, что данный выходной сигнал всегда генерируется, либо существует состояние, когда сигнал отсутствует. Впрочем, ни каких новых возможностей последняя функция не добавляет. Входные сигналы программы можно зафиксировать, установить их значение в 0 или 1. Если выходной сигнал может быть сгенерирован, минимальная трасса выполнения, демонстрирующая сигнал, сохраняется в формате CSIMUL. Последовательность шагов может быть выполнена графическим симулятором языка Esterel программой Xes. Этот же файл может быть полезен для консольного симулятора.

На первый взгляд кажется, что верификатор имеет слишком ограниченные возможности. Хотелось бы проверять более сложные свойства. Сложные свойства можно проверять, если описать их отдельной программой-наблюдателем (observer) на языке Esterel, которая подсоединяется к основной программе. При нарушении свойства наблюдатель генерирует специальный сигнал. Таким образом, выполнение свойства эквивалентно утверждению, что тревожный сигнал никогда не генерируется.

Более подробное описание Xeve и процедуры проверки можно найти в главе 2, разделы 2.3.3, 2.4.6.

1.4.3. TempEst Существует приложение, позволяющие описывать проверяемые свойства на языке LTL (Liner Time Temporal Logic). Оно называется TempEst [75].

Особенность в том, что используется линейная темпоральная логика с операторами прошедшего времени. Задание свойств на языке LTL может быть удобнее, чем на языке Esterel. Намерения автора выражаются более явно.

TempEst не является верификатором. LTL-свойства преобразуются в модули на языке Esterel, которые требуется запускать параллельно основной программе. Алгоритм преобразования несложно понять [77]. В принципе, процедура проверки такая же, как при ручном написании свойств на Esterel, только свойства описываются в другом формате.

Более подробно процедура проверки описана в главе 2, раздел 2.3.4.

Среда разработки и верификации синхронноавтоматных программ 2.1. Формальная модель автоматной программы Назовем реактивную систему, реализованную синхронно-автоматным (СА) подходом к программированию, реактивной синхронной системой. Для краткости ее будем называть синхронной системой.

Синхронно-автоматная модель описывает синхронную систему. Основные компоненты модели это синхронные автоматы и синхронные сети. Каждый из них в отдельности сам представляет синхронную систему. Изоморфизм представления достигается за счет унифицированного интерфейса.

2.1.1. Интерфейс синхронной системы Интерфейс I = (X, Y ) синхронной системы определяется парой, состоящей из набора входных сигналов X = { x1,..., xm } (m 0) и выходных сигналов Y = { y1,..., yk } (k 0). Как можно видеть, оба списка сигналов могут быть пустыми. Каждый сигнал может принимать значения 0 и 1.

Для обозначения сигналов используются буквы x, y, z. Значения этих сигналов обозначаются так же. В большинстве случаев это не приводит к путанице. Так в записи z = 0 речь, очевидно, идет о значении сигнала, а в записи z = z о самом сигнале. В том случае, когда нам необходимо, чтобы были равны именно значения сигналов, будем использовать обозначение (z):

(z) = (z ), или будем оговаривать этот нюанс словами.

2.1.2. Синхронный автомат Синхронный автомат реализует синхронную систему. Пусть синхронная система имеет интерфейс I = (X, Y ), тогда реализующий ее автомат определяется следующим образом:

Здесь ное состояние автомата.

Из множества входных сигналов строится формальный язык L. Он используется для записи условий на переходах.

Константы 0 и 1 обозначают “ложь” и “истину” соответственно. Логические операции ¬,, имеют обычный смысл. Все они имеют разный приоритет, убывающий слева направо в порядке перечисления. Скобки используются для переопределения приоритета.

Пусть также множество выходных реакций. Элементы этого множества списки выходных сигналов (множества выходных сигналов). В списке каждый сигнал присутствует не более одного раза. Списки, отличающиеся только порядком сигналов, считаются одинаковыми. Допускается пустой список.

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

переход является петлей. Между любыми двумя состояниями (в том числе совпадающими) может быть любое число переходов. Все переходы, выходящие из любого состояния, должны быть помечены ортогональными формулами, чтобы для любой комбинации входных сигналов нашлось не более одного перехода. Однако не обязательно, чтобы каждому набору входных сигналов соответствовал переход. Если перехода нет, по умолчанию считаем, что система не меняет состояние и не генерирует выходные сигналы.

Пример синхронного автомата приведен на рис. 2.1.

2.1.3. Синхронная сеть Синхронная сеть реализует синхронную систему. Пусть синхронная система имеет интерфейс I = (X, Y ), тогда реализующая его синхронная сеть определяется следующим образом:

Синхронная сеть объединяет несколько синхронных систем. Как они реализованы не имеет значения, доступен только интерфейс. Детали реализации полностью скрыты за интерфейсом. Набор синхронных систем определяется только их интерфейсами:

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

Более подробно различие будет описано в разделе 2.1.4.

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

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

Пример синхронной сети приведен на рисунке 2.2.

Рис. 2.2. Пример синхронной сети. Здесь I1, I2, I3, I4 некоторые синхронные подсистемы. Синхронная сеть имеет три входных и три выходных сигнала 2.1.4. Типы и экземпляры Синхронные сети и автоматы описывают типы, модели синхронных систем. Каждый ранее определенный тип может быть использован при определении других типов (только синхронных сетей). Типы отражают статическую структуру соответствующих моделей.

Для описания поведения системы вводится понятие экземпляра. Под экземпляром понимается конкретная синхронная система в процессе выполнения. Экземпляром является вся моделируемая синхронная система в целом, так и ее отдельные подсистемы. Каждый экземпляр имеет тип. Это определенный тип автомата или определенный тип синхронной сети. Один и тот же тип может иметь несколько экземпляров в синхронной системе.

Экземпляр характеризуется текущим состоянием, значениями входных, выходных и внутренних сигналов. Для экземпляров типа автомат состояние определяется значением одной переменной q. Состояние экземпляра синхронной сети определяется состоянием всех его синхронных подсистем.

Экземпляр автомата A обозначим где q состояние автомата, X и Y вектора значений входных и выходных сигналов соответственно.

Экземпляр синхронной сети N обозначим где R = {r1,...} вектор синхронных подсистем, используемых данным экземпляром синхронной сети. ri имеет интерфейс Ii. В отличие от определения типа синхронной сети, при определении экземпляра нам необходимо знать не только интерфейс, но и всю используемую синхронную подсистему. Как уже упоминалось, состояние экземпляра синхронной сети включает в себя состояния всех используемых ей синхронных подсистем. X, Y вектора значений входных и выходных сигналов.

Условимся для обозначения экземпляров использовать строчные буквы, а для обозначения типов заглавные. Экземпляр и тип будут обозначаться одной и той же буквой в разных регистрах, при этом сохраняются все модификаторы, такие как индексы, штрихи, волны и т.п. Например, в высказывании “Пусть Ei A такой, что ei.x1 = 1... ” подразумевается, что существует экземпляр ei типа Ei.

2.1.5. Модель в целом Синхронно-автоматная модель состоит из автоматов A = {A1,...} и синхронных сетей N = {N1,...}. Допускается, чтобы N =, но A =.

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

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

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

Вся синхронная система в целом есть экземпляр. Обозначим его r, а соответствующий тип R (R A N ). Иначе говоря, r является экземпляром 2.1.6. Динамика синхронно-автоматной модели Выполнение синхронно-автоматной модели происходит по законам синхронной системы. Время представляется последовательностью дискретных инстентов. В каждый инстент вычисляется реакция системы. Изначально известно текущее состояние системы и значения входных сигналов. Нужно вычислить следующее состояние и значения выходных и внутренних сигналов.

Состояние изменяется при переходе в следующий инстент. Правила “вычисления” будут описаны ниже в разделе 2.1.9.

2.1.7. Иерархические обозначения Необходимо иметь возможность ссылаться на каждый экземпляр автомата и синхронной сети, составляющий синхронную систему. Важно указать на относительное положение экземпляра в модели. Для этого удобно воспользоваться записью с точкой: A.Q множество состояний автомата A, a.x первый входной сигнал экземпляра автомата a и т.д. Синхронно-автоматная модель имеет иерархическую структуру, поэтому имена компонентов модели также будут формироваться иерархически: r.r2 вторая подсистема синхронно-автоматной системы (предполагаем, что R N ), r.r2.r1 первая подсистема, указанной выше подсистемы (предполагаем, что r.R2 N ) и т.п.

Для краткости конкретный экземпляр будем обозначать ei, зная, что ему соответствует некоторое полное имя: ei = r.ri1.....ril, где l 0. Тип экземпляра ei обозначим Ei = r.ri1.....ril1.Ril.

2.1.8. Состояние и сигналы синхронно-автоматной системы Текущее состояние синхронной системы r определяется состоянием всех ее автоматов: (ei1.q,...), где eij экземпляр автомата (Eij A), q текущее состояние экземпляра eij.

Входные и выходные сигналы синхронной системы r соответственно: r.X, r.Y.

Внутренние сигналы синхронной системы r: ei={ei.X, ei.Y }. Каждый внутренний сигнал играет двойную роль. Во-первых, это входной или выходной сигнал соответствующего экземпляра (назовем его ei ), во-вторых, это внутренний сигнал экземпляра синхронной сети, которая содержит экземпляр ei.

Следующее состояние синхронной системы: N ext(ei1.q,...), где Eij A.

Оператор N ext используется для обозначения значения сигналов и состояний автоматов в следующий инстент.

2.1.9. Конструктивная поведенческая семантика синхронноавтоматной модели Семантика синхронно-автоматной программы определяется семантикой соответствующей Esterel-программы, полученной по известному алгоритму.

Для облегчения интерпретации модели описана конструктивная поведенческая семантика языка синхронно-автоматного программирования, оперирующая только в терминах С-А модели. Надо заметить, что она не используется в каких-либо инструментах проверки и ее справедливость не доказывается.

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

Правила вывода следующего состояния и значений сигналов составляют суть семантики С-А программирования. Семантика описывается через процедуру вычисления реакции системы. Решение о синтаксической корректности программы дается на основании применения указанной процедуры “во всех возможных случаях” (ниже будет дано точное определение).

Процедура вычисления реакции системы Для работы с сигналами воспользуемся трехзначной логикой. Значение сигнала z {0, 1, }, где 0 ложь, 1 истина, неопределенное значение.

Состояние экземпляра автомата a может принимать значения из множества A.Q {}, где снова обозначает неопределенное значение.

В начале процедуры значения сигналов и состояния автоматов устанавливаются следующим образом.

• Текущее состояние системы известно: (ei1.q,...), где Eij A, eij.q • Определены значения всех входных сигналов системы: r.xi {0, 1}.

• Значения всех остальных сигналов не определены: r.yi = ; ei.xj = • Следующее состояние системы тоже не определено: N ext(ei.q) =, для Правила изменения значений 1. Для автоматов текущее состояние экземпляра ei, l = 1. Тогда (1) положим N ext(ei.q) = ei.q ; (2) для каждого ei.yj Ei.Y, такого что ei.yj текущее состояние экземпляра ei, верно l = 0. Тогда положим 2. Для синхронных сетей а. Пусть z Ei.X, причем z =. Пусть g Ei.G такой, что z g.

б. Пусть r ei.R. Пусть z R.Y такой, что z =. Пусть g Ei.G в. Пусть z Ei.Y, причем ¬g Ei.G такого, что z g. Тогда пусть Ограничения на применение правил изменения значений • Правило 1а нельзя применять дважды для одного перехода f.

• Правило 1б нельзя применять дважды для одного сигнала y.

• Правило 1в нельзя применять дважды для одного экземпляра автомата ei.

• Правила 2а, 2б, 2в, 2г нельзя применять дважды для одного сигнала z.

Определение синтаксической корректности программы Если в процессе применения правил делается попытка изменить значение сигнала или состояние автомата, значение которого = 0, то процедура завершается и программа считается синтаксически некорректной.

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

2.2. Форматы данных Для описания синхронно-автоматной модели необходим специальный язык. Важное требование к языку разработки он должен быть удобен для набора на компьютере. Система обозначений, предложенная в разделе 2.1, удобна для восприятия, но сложна для набора на компьютере. Синтаксический анализ таких формул оказывается непростым занятием. Возникает необходимость в создании специального языка для описания синхронноавтоматных программ. Такой язык был создан.

2.2.1. Описание в формате XML Язык XML удачно подходит для решения данной задачи. Элементы являются строительным блоком языка XML. Они разделяют документ на иерархию областей. Одни элементы служат контейнерами для других. У элементов есть атрибуты. Область применения XML достаточно велика. Он содержит большое число компонентов, которые не были использованы для описания синхронно-автоматной программы. К счастью, язык не навязывает использование дополнительных возможностей, мы можем использовать только то, что действительно необходимо.

Автомат описывает одним элементом “automata”. С элементом связаны атрибуты: “name” имя автомата, “nodes” число узлов, т.е. число состояний автомата, “inputs” и “outputs” число выходных и выходных сигналов. Переходы описываются отдельными элементами “edge”, вложенными в автомат.

Переход имеет атрибуты: “start” номер начального состояния, т.е. откуда выходит дуга, “end” номер конечного состояния, т.е. куда осуществляется переход, “label” метка перехода, содержит условие перехода и выходное воздействие, разделенное прямым слешем. Нет необходимости описывать состояния автомата. Достаточно только знать их общее число. По соглашению первое состояние является начальным.

Синхронная сеть описывает отдельным элементом “net”. У нее есть атрибуты “name”, “nodes”, “inputs”, “outputs”. Их значение такое же, как у элемента автомат. “nodes” обозначает число внутренних подсистем. Подсистемы и группы сигналов описываются вложенными элементами “node” и “group” соответственно.

Все автоматы и синхронные сети содержатся в универсальном контейнере “model”. Его единственный атрибут “top” содержит имя главного элемента модели. Это имя автомата или синхронной сети, описанной внутри элемента “model”.

Описание синхронно-автоматной программы в формате XML выглядит достаточно понятно, если соблюдать определенные соглашения о форматировании тегов. Большой плюс XML в том, что для этого языка существуют парсеры для практически всех популярных языков программированию. Задача лексического, синтаксического анализа, построение своего парсера выглядит устрашающее. Разработка программы занимает много времени. А типичные ошибки в таких программах очень сложно находить. Принимая во внимание все эти факторы, становится понятно, насколько желателен выбор языка, для которого парсер уже разработан. Мы можем сэкономить много времени, используя XML, и скорее проверить теоретическую модель на практике. Так и было сделано.

К сожалению, формат XML подходит для разработки только небольших программ. Причина в том, что описание автоматов в виде набора тегов не наглядно. Когда компонентов в системе много, невозможно их всех держать в голове, а восстановление описания автомата по его теговому описанию требует времени. Формат XML не был отвергнут окончательно. Требуется надстройка, которая будет представлять описание автоматов и синхронных сетей в наглядной форме. В то же время, XML-описание удачно подходит для хранения описания программы.

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

Автоматы и синхронные сети в целом представляются классами UML.

Входные и выходные сигналы моделируются с помощью портов класса. Порты являются дочерними элементами класса.

Внутренняя структура синхронной сети описывается диаграммой составной структуры (Composite Structure Diagram). На диаграмме изображается класс синхронной сети со всеми портами-сигналами. Внутри класса располагаются синхронные подсистемы. Они обозначаются элементами часть (Part).

Каждая подсистема выставляет все порты-сигналы. Порты синхронной сети и ее составных частей соединяются ассоциациями. Необходимо соблюдать правила именования.

Описание синхронно-автоматной модели набором UML-диаграмм наглядно представляет модель. Тем самым демонстрируется одно из самых важных достоинств, которое заявляет switch-технология наглядность. Разработка программы может быть выполнена в обычном UML-редакторе. Программ такого типа разного качества и условий распространения достаточно много. Ни каких специфических характеристик от редактора не требуется. Используется небольшое подмножество элементов UML версии 2.0.

2.2.3. Описание на языке Esterel Языки описания на основе XML и UML являются высокоуровневыми средствами представления синхронно-автоматной программы. Один из них применяется для хранения и быстрой интерпретации программы, другой как наглядное преставление программы и удобное средство разработки. Синхронно-автоматная программа реализует синхронную систему, ей присущи многие особенности языка Esterel, поэтому не кажется удивительным, что язык Esterel используется для реализации синхронно-автоматной программы. Синхронно-автоматная программа в конечном итоге преобразуется в программу на языке Esterel.

Между синхронно-автоматной моделью и программой на языке Esterel существует четкое соответствие. Автоматы и синхронные сети реализуются отдельными модулями языка Esterel. Этот язык не имеет конструкции, аналогичной интерфейсу. Интерфейсные сигналы компонентов модели отображаются в просто сигналы модуля. По соглашению, входные сигналы называются x1, x2 и т.д., а выходные y1, y2 и т.д.

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

Тело модуля автомата заключено в бесконечный цикл, выполняющийся каждый инстент. Тело цикла состоит из двух вложенных switch-подобных конструкций. Внешний оператор выбирает текущее состояние, соответствующее единственному присутствующему сигналу из набора q1, q2,... Внутренний оператор выбирает исходящий из данного состояния переход. Если активный переход найден, то в следующем инстенте генерируется сигнал нового состояния, в противном случае в следующем инстенте сохраняется прежний сигнал состояния. При срабатывания перехода генерируются необходимые выходные сигналы.

Реализация синхронной сети, также как и автомата, содержит бесконечный цикл, срабатывающий каждый инстент. Тело цикла содержит последовательность проверок для каждой группы связанных сигналов. Если ведущий сигнал группы присутствует, то генерируются все ведомые сигналы данной группы. Параллельно с основным циклом запускаются модули, соответствующие подсистемам данной синхронной сети.

Файлы с Esterel программой содержит описания всех автоматов и синхронных сетей, использованных в синхронно-автоматной программе. Помимо перечисленных модулей, в файле присутствует еще один модуль, имя которого совпадает с именем файла. Это точка входа в программу. Обычно этот модуль только вызывает корневой элемент модели и перенаправляет сигналы.

По Esterel-программе, сформированной в соответствии с действующими соглашениями, можно без труда восстановить исходную модель. Синхронноавтоматную программу можно писать сразу на языке Esterel, хотя вряд ли в этом есть смысл.

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

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

Можно выделить три класса ошибок.

2.3.1. Нарушение формата модели Описание синхронно-автоматной модели должно подчиняться определенным правилам. Например, в текущей реализации требуется, чтобы имя автомата состояло из заглавной буквы A и следующего за ним номера. Аналогичные соглашения именования существуют для других элементов модели. Или другой пример: в каждую группу сигналов синхронной сети должен входить ровно один ведущий сигнал. Ошибки нарушения формата модели отлавливаются на этапе интерпретации синхронно-автоматной программы, т.е. чтения набора UML-диаграмм или XML-файла. Обнаружение ошибок этого класса выполняется автоматически, проверка не занимает много времени, причины ошибок несложно понять.

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

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

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

Проверка пользовательских свойств выполняется верификатором Xeve [56, 57] компании Inria. Он создан для проверки программ на языке Esterel. При этом фактически проверяется Esterel-программа, построенная по синхронно-автоматной модели. Опишем технику проверки (рис. 2.3).

Рис. 2.3. Проверка пользовательских свойств синхронно-автоматной модели Проверяемая программа представляет собой синхронную систему. У нее есть входные x1,..., xn и выходные y1,..., ym сигналы. Выходные сигналы проверяемой системы подаются на вход тестовой программы. Тестовая программа на основании получаемых сигналов может решить, нарушается свойство или нет. Выходных сигналов проверяемой системы не всегда достаточно для описания проверяемого свойства. Можно внедрить тестовую программу в проверяемую систему, или, специально для целей отладки, расширить набор выходных сигналов исходной системы. В любом случае исходная система модифицируется, поэтому встает вопрос об адекватности проверки. Действительно ли результаты проверки для модифицированной системы отвечают на вопросы, поставленные для исходной системы?

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

До сих пор не было сказано, как тестовая программа сообщает о нарушении свойства. На каждое проверяемое свойство выделяется отдельный выходной сигнал. Этот сигнал генерируется, когда проверяемое свойство нарушается. Задача проверки определенного свойства сводится к вопросу, существует ли история входных сигналов, которая приводит к генерации тревожного сигнала. Для ответа на такие вопросы как раз предназначен верификатор Xeve.

Практически проверка пользовательских свойств реализуется следующим образом. У нас есть программа на языке Esterel, полученная из синхронно-автоматной программы. Пишется код на языке Esterel, который выражает проверяемые свойства. Обычно это несколько модулей. Если необходимо ограничить входные сигналы программы, пишется дополнительная программафильтр. Все части кода компилируются в одну программу, которая подается на вход верификатору.

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

2.3.4. TempEst для выражения пользовательских свойств Проверяемые свойства для программы можно определять не только на языке Esterel. Существует специальный инструмент TempEst [76, 83], предназначенный для описания и интерпретации свойств на языке темпоральной логики. Каждое свойство описывается в отдельном файле. Применяется линейная темпоральная логика с небольшими синтаксическими улучшениями (например, части формулы можно дать имя и повторно использовать его при составлении других формул). Описание формулы транслируется в отдельный модуль языка Esterel, который должен запускаться параллельно основной программе.

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

Основная часть языка линейной темпоральной логики TempEst Опишем язык LTL, используемый в TempEst [75, 77].

Пусть Sig будет фиксированный алфавит используемых сигналов. Существуют специальные сигналы T RU E и F IRST. Первый из них присутствует в любом инстенте, второй только в первом инстенте.

Пусть PAST класс темпоральных формул, ссылающихся на прошедшее время. Формулы множества PAST являются формулами состояния, т.е.

значение формулы может быть определено для каждого состояния любого пути. Каждый отдельный сигнал алфавита Sig и каждая константа являются формулой. Если p, q PAST, тогда p q, p q, ¬p, p q PAST. Логические операторы,, ¬, имеют обычный смысл. Язык Esterel не позволяет обращаться к будущему, поэтому используются темпоральные операторы прошедшего времени. Если p, q PAST, то P p, pS q, G p, O p, pB q PAST.

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

Значение данной формулы равно значение формулы p в предыдущий инстент.

В первый инстент значение формулы равно false.

Значение формулы true, когда формула q принимает значение true. Формула сохраняет значение true, после того как q true, пока p остается true.

Во всех остальных случаях значение формулы false.

Формула принимает значение true, если p true непрерывно с первого инстента. Значение false получается начиная с момента, когда p обращается в false.

Значение формулы true, если p в текущий инстент или когда-то в прошлом принимало значение true.

Формула определяется через ранее определенные формулы: p B q (p S q) G p. Значение формулы true, если p непрерывно true, начиная с первого инстента, или с последнего инстента, где q было true.

Еще одно множество формул обозначается SAF E. Формулы множества SAF E являются формулами пути. Это также формулы безопасности. Если p PAST, то A p SAF E. Здесь A квантор пути. Формула A p истина тогда и только тогда, когда формула p истина в каждом состоянии пути.

Дополнительные операторы TempEst TempEst предлагает также несколько дополнительных формул.

Здесь p, q PAST формулы состояния, b целое неотрицательное число, один из сигналов, например, tick. Эта формула выражает задержку реакs ции (bounded response) системы на некоторое воздействие. В ответ на событие p система должна отреагировать событием q в течении не более чем b отсчетов времени. Отсчетом времени считается получение сигнала s. В данном определении под событием понимается инстент, в котором какая-то формула принимает значение true, p или q. Вся формула принимает значение false в тот инстент, когда приходит b-ый сигнал s, а q имеет значение false. При этом, с момента отсчета времени, т.е. когда p true, q принимала только значения false. После начала отсчета времени появление других инстентов, когда p true, не играет ни какой роли. Они не изменяют текущий отсчет времени и не начинают дополнительный отсчет времени.

Реализацию данной формулы на языке Esterel можно описать так. Из инстента в инстент мы ждем, когда формула p обратится в true. Если в этот же инстент формула q обращается в true, то продолжает ждать дальше, иначе входим в состояния ожидания реакции. В данном состоянии мы пребываем до тех пор, пока либо q обратится в true, либо мы пронаблюдаем b сигналов s. В первом случае мы выходим из состояния ожидания нормально, т.е. вся формула остается true. Во втором случае, формула обращается в false на один инстент. Если оба условия выполняются одновременно, мы поступаем как в первом случае.

Практически данная формула представляет интерес, только когда она вкладывается в формулу A, т.е. нам интересно знать, нарушается ли когданибудь условие задержки или нет.

H(p, q, b, s) Здесь снова p, q PAST формулы состояния, b целое неотрицательное число, s один из сигналов, например, tick. Эта формула выражает связь между сигналом s и формулой q. Алгоритм, рассчитывающий эту формулу, можно описать так. Ждем, когда p примет значение true и будет сохранять его в течение b сигналов s. Затем переходим в специальное состояние, когда приход сигнала s сопоставляется с значением формулы q. Данное состояние заканчивается тогда, когда формула p перестает быть true. Каждый инстент, когда приходит сигнал s, необходимо, что бы q обращалась в true. Если этого не происходит, вся формула обращается в false.

Точно так же, как и предыдущая формула, эта представляет практический интерес, когда находится под действием квантора A.

Особенности языка TempEst Для описания формул в TempEst на самом деле используются ключевые слова, а не математические символы (таблица 2.1). Например, логическое “или” можно записать либо Or, либо |, или оператор B записывается словом BackT o. Язык для TempEst позволяет, а в некоторых случаях настаивает на использовании дополнительных идентификаторов для обозначения частей формул.

Чтобы обозначить формулу при помощи идентификатора id используется синтаксис:

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

Таблица 2.1. Соответствие символьных обозначений, описаний на естественном языке и обозначение естественном языке 2.4. Структура среды разработки Рис. 2.4. Среда разработки синхронно-автоматных программ. Диаграмма данных Структуру среды разработки удобно представить с помощью двух диаграмм. На рис. 2.4 показаны пути преобразования данных в процессе работы. Рис. 2.5 содержит соответствующие инструменты, используемые для создания или преобразования данных с рис. 2.4. Каждой стрелке, символизирующей операцию преобразования данных, на рис. 2.4 соответствует прямоугольник инструмента на рис.2.5.

Рис. 2.5. Среда разработки синхронно-автоматных программ. Диаграмма инструментов Область рисунка, окруженная пунктирной рамкой, является опциональной. Так, на рис. 2.4 компонент Проверяемые свойства LTL является необязательным. Проверяемые свойства можно определять сразу на языке Esterel (прямоугольник Проверяемые свойства Esterel ).

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

Более подробно, что было сделано по каждому компоненту, будет рассказано ниже.

Компилятор языка Esterel, верификатор Xeve и другие инструменты, обеспечивающие основную функцию верификации, спроектированы для работы на нескольких платформах. Дистрибутив компилятора предлагается для Windows NT, Linux, Sun Solaris, IBM AIX, Dec OSF1. Xeve поддерживает платформы: Linux, Sun Solaris, Dec Alpha OSF. В связи с этим при разработке программной среды большое внимание уделалось переносимости. MagicDraw UML, выбранный в качестве UML-редактора, работает на Java-платформе.

Скрипты MDUML2SAM, SAM2strl написаны на языке Perl.

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

2.4.1. UML-редактор Разработка программы начинается в UML-редакторе MagicDraw UML.

Его внешний вид приведен на рис. А.1. Используются стандартные возможности инструмента. Мы ограничиваем себя определенным набором диаграмм UML. Выполняется обычное UML-моделирование. Однако, для того чтобы результирующий набор диаграмм воплотился в синхронно-автоматную программу, необходимо соблюдать определенные правила именования компонентов модели и придерживаться соглашений об использования элементов. На данном этапе отсутствует контроль за выполнением правил. Ошибки обнаружат себя на более поздних этапах разработки.

Использование стандартного редактора имеет то преимущество, что нам не пришлось его разрабатывать. Это, конечно, сэкономило много времени.

Стандартный редактор также содержит множество возможностей, которые облегчают, ускоряют разработку, например, функции копирования/вставки, отмены. Крайне удобна функция комментирования практически любого элемента модели.

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

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

2.4.2. Преобразование из UML-описания в XML-описание Следующим шагом разработки синхронно-автоматной программы является преобразование набора UML-диаграмм в файл XML. В этот момент выполняется минимальная проверка формата модели. Более тщательная проверка будет выполнена позже. Многие ошибки не являются критическими, например, мы можем без опасений проигнорировать неизвестный тип диаграммы.

Существенные нарушения формата модели прерываются процесс генерации.

Распознанная модель сохраняется в XML-файле.

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

MDUML2SAM. Он на входе получает файл с UML-диаграммами, а на выходе выдает файл XML. Синтаксис команды приведен в листинге А.5, а пример ее использования приведен в листинге А.7.

2.4.3. Построение Esterel-программы по XML-описанию Для чтения XML-описания модели используется готовый XML-парсер1.

При интерпретации модели приходится иметь дело с программными структурами, а не со строками, которые нужно разбирать. Применение готового парсера существенно упрощает программу преобразования. Выполняется полная, насколько это возможно, проверка модели. Если программа прошла проверку, генерируется Esterel-программа. Программа преобразования имеПакет Perl XML::Parser ет несколько режимов генерации. В специальном режиме, предназначенном для проверки модели, экспортируются все внутренние сигналы синхронноавтоматной программы.

Данный этап полностью автоматизирован. Разработан скрип SAM2strl.

Он на входе получает файл в формате XML, а на выходе генерирует файл.strl с описанием программы на языке Esterel. Синтаксис команды приведен в листинге А.6, пример ее использования в листинге А.8. Фрагмент скрипта приведен на листинге А.3.

2.4.4. Проверка синхронных свойств Файл, созданный на предыдущем этапе, содержит полноценную программу. Вероятно, что в ней присутствуют ошибки. Процедура генерации Esterel-программы практически гарантирует отсутствие синтаксических ошибок.

Первая проверка, которую мы выполняем обычная компиляция программы. Сложно представить случай, когда компиляция будет провалена. Вторая проверка это проверка на конструктивность. Типичная ошибка, которая может быть обнаружена на этом этапе существование циклической зависимости между сигналами, которая не позволяет однозначно проинтерпретировать программу. Компилятор Esterel в специальном режиме осуществляет такую проверку.

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

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

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

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

2.4.6. Проверка пользовательских свойств верификатором Xeve Верификатор Xeve требует специальный формат входного файла.blif (Berkeley Logical Interchange Format). Его производит компилятор языка Esterel. Перед использованием верификатора имеет смысл выполнить проверку на конструктивность. Кроме того, сама компиляция может выявить ошибки, допущенные при написании свойств.

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

На рис. А.2, А.3 показан внешний вид графической версии верификатора Xeve. Листинг А.11 демонстрирует вызов консольного варианта верификатора CheckBLIF.

Если проверяемое свойство выполняется, то на этом проверку можно закончить. Если проверяемое свойство нарушается, то верификатор генерирует последовательность входных сигналов, приводящих к ошибке. Эту последовательность можно анализировать либо вручную, либо при помощи одного из двух отладчиков Esterel-программ.

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

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

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

Основной критерий оценки состоит в числе обнаруженных ошибок.

3.1. Пример 1: Арбитр шины 3.1.1. Введение Пример демонстрирует использование синхронно-автоматного программирования для реализации простого контроллера шины. Пример взят из руководства по верификатору языка Esterel программы Xeve. Главная идея решения связана с особенностями синхронного подхода. Пример интересен с точки зрения декомпозиции синхронной системы на блоки.

3.1.2. Описание задачи Арбитр шины управляет доступом к разделяемому устройству. Есть несколько пользователей, но только один из них может обращаться к шине в один момент времени. С каждым пользователем связывается сигнал request.

В данном примере их три, однако система легко масштабируется для случая произвольного числа пользователей. Каждому сигналу request соответствует сигнал ask, подтверждающий получения доступа для данного запроса.

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

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

Алгоритм, решающий данную задачу, указан в первоисточнике [56]. Новизна данной работы в том, что решение адаптировано для синхронно-автоматного подхода.

3.1.3. Реализация Для решения указанной задачи было использовано четыре автомата и две синхронные сети. Таблицы с описанием основных компонентов системы приведены в приложении Б.