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

На правах рукописи

Кубасов Сергей Валерьевич

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

05 13 11 - Математическое и программное обеспечение вычислительных машшт, комплексов и компьютерных сетей

АВТОРЕФЕРАТ диссертации на соискание ученой степени кандидата технических паук

□□344Э48Э

Ярославль - 2008

003449489

Работа выполнепа па кафедре теоретической информатики Ярославского государственного университета им IIГ Демидова.

Научный руководитель

Официальные оппоненты

Ведущая организация.

доктор физико-математических наук, профессор

Соколов Валерий Анатольевич

доктор физико-математических наук, профессор

Ломазова Ирина Александровна,

кандидат физико-математических наук, доцент

Дехтярь Михаил Иосифович

Санкт-Петербургский государственный университет информационных технологий, механики и оптики

Защита состоится 14 ноября 2008 г в 14 часов на заседании диссертационного совета ДМ002 084 01 при Учреждении Российской академии наук Институте программных систем РАН, расположенном по адресу: 152020, Ярославская область, Переславский район, с Веськово, ул Петра Первого, д. 4а

С диссертацией можно ознакомиться в библиотеке Учреждения Российской академии наук Института программных систем РАН.

Автореферат разослан «_» октября 2008 г.

Ученый секретарь

диссертационного совета ------Пономарева С М.

Общая характеристика работы

Актуальность работы С 90-х годов XX века в России развивамся автоматное программирование Профессор А А. Шалыто предложил использовать эи^сЬ-технологию (другое название автоматного программирования) для реше1тя задач логического управления Ее основная идея в использовании автоматов для кодирования логики программы Допускается применять дру1 ие подходы для решения отдельпых подзадач Технология автоматного программирования значительно упрощает взаимодействие различных участников процесса разработки программного обеспечения

Со времени своего шобретепия техпология претерпела некоторые нзмепе-ння Были предложены различные модификации злуйсЬ-техпологии, использующие идеи других популярных парадигм программирования, например, объектно-ориентированного программирования Расширилась область применения В результате появилось несколько вариаций АП, среди которых уже сложно выявить гтавное направление

Для разработки сложных программных систем с применением йчу^сЬ-тех-нологии был создан проект 1ММо(1 В этом инструментальном средсгве можно было обнаружить множество полезных функций для разработчика Это визуальное программирование, отладчик, подсветка синтаксиса и многое другое К сожалению, не было никакой возможности верификации программ. Более того, заложенные в основу представления об автоматпой программе делали задачу добавления полноценной проверки проблематичной ишМо(1 не дает четкого определения авгоматной программе, тем более не использует математическую модель.

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

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

Задачи логического управления часто предъявляют критические требования к надежности программного обеспечения Цифровые устройства сейчас можно встретить практически во всех сферах человеческой жизни. От их бесперебойного функционирования часто зависит жизнь людей Со временем количество и сложность устройств логического управления только возрастают Поэтому задача верификации не теряет, а, наоборот, усиливает свою актуальность Ручная проверка — трудоемкое занятие Гораздо удобнее и надежнее поручить выполнение этой задачи компьютерной программе

Задача верификации возникла несколько десятилетий назад К настоящему моменту уже выработаны разнообразные подходы ее решения Среди ученых, внесших значительный вклад в решение этой задачи, можно выделить II Л Анисимова, О JI Бандман, 10 Г Карпова, И А. Ломазову, В А Непомнящего, А К Петренко, P.JI Смелянскою, В А Соколова, РА Abdulla, G. Beriy, M С Browne, К Cerans, EM Clarke, Б A Emerson, A Finkel, Ji 0 Grumberg, G L Holzmann, К Jensen, Z. Manna, A Pniieh, Pli Sthnoebelen, N Sidorova, J Sifakis

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

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

блемой В Ярославском государственном университете им П Г Демидова на кафедре теоретической информатики проводятся исследования но моделированию, спецификации и верификации автоматных программ. Результаты работ обсуждаются па семинаре "Моделирование и анализ информационных систем'1 и конференциях В работу вовлекаются студенты Команда Шалы-то Л.Л , автора технологии автоматпого программирования, также достигла определенных успехов в разработке среды для верификации автоматных программ

В работе Кузьмина Е В 1 предлагается иерархическая модель автоматных программ Модель рассматривается на примере снсгемы управления кофеваркой В рабоге Васильевой К Л к Кузьмина ЕВ.2 предлагается способ моделирования, спецификации if верификации автоматпых программ Используется верификатор SPIN, логика LTL Рассмотрен пример системы управления банкоматом Одним из развитий иерархической модели автоматных программ является модель, использующая формализм сетей Петри Разработка программы выполняется d UmMod, применяется верификатор CPN/ Tools, рассмотрен пример системы управления кофеваркой Получено свидетельство об официальной регистрации программы для ЭВМ

lía кафедре технологий программирования С116ГУ ИТМО были получены в том числе следупцте результаты. В работе Вельдера С.Э.3 рассматривается техника верификации автоматных программ, состоящих из одного конечного автомата Описывается преобразование автомата в структуру Крипке, выражение темпоральных свойств на языке CTL, верификация по модели (метод "Model Checking") и построение сценария для исходного лвто-

1 Кузьмин, Е В Иерархическая модель автоматных программ // Моделироваппс и анализ информационных систем - 2006 — Т 13, Л^ 1 - С 37-34

Васильева, К А Верификшуш ниюмащык нротрамм с использованием LTL / К А В л сил ьс на, ЕВ Kj3bMHii // Моделирование н алали) информационных систем — 2007 — Т.14, Л* 1 — С 3-14

3Вельдер, С Э О верификации простых автоматных программ на основе метода "Model Checking" / С Э Be 1ьдер, А А Шалыго / / Информационно-управляющие системы — 2007 — №3 —С 27-38

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

Можно заметить, что все авторы используют Model Checking. Главное различие наблюдается в моделях. Данная работа не является исключением Язык синхронного программирования esterel разрабатывался для аналогичного круга задач, что и автоматное программирование. В отличие от All, в esterel был изначально заложен прочный теоретический фупдамент. В esterel существует базис — подмножество языка, па котором можпо определить все его операторы Программа на языке esterel — это уже модель, готовая для верификации Существует верификатор Xeve для проверки esterel программ ЛП и язык esterel помимо общей задачи роднит тот факт, что оба они используют бинарные сигналы

АП и esterel удачпо дополняют друг друга АП предлагает средства для визуальной разработки программ, a estere! обеспечивает прочную математическую основу и средства верификации

Xeve — зто верификатор дта esterel программ, представляемых в виде конечных автоматов Xeve предлагает дружественный графический пользовательский интерфейс.

Цель диссертационной работы Главная цель диссертации — создать

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

• Разработать формальную модель автоматной программы, которая бы подходила для сложившейся практики применения автоматного программирования

• Разработать метод верификации автоматных программ

• Разработать и реализовать программные средства построения и верификации автоматных программ Исследовать работу программной си-с темы при решении практических задач

Научная новизна Все основные результаты являются новыми.

в Разработана формальная модель автоматной программы, учитывающая наиболее важные идеи автоматного прадраммирования

• К автоматному программированию был примепен синхронный подход Уточнена временная модель Поведение программы стало детермини-ровапньш Разработана вариация автоматного программирования — ашхришю-ми оматнос программирование

• Разработаны способы верификации синхронно-автоматных программ при помощи существующих программных инструментов языка оличс! Использован верификатор Хеуе

в Создана программная среда разработки и верификации синхроппо-ав-томатных про! рамм

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

Разработана и реализована программная система разработки и верификации сиихронно-автоматных программ Ее применение упрощает и ускоряет разработку и проверку указанного класса программ

Апробация работы Результаты диссертации докладывались на 7-ои международной конференции и выставке "Системы проектирования, техпо-тогической подготовки производства и управления этапами жизненного цик-

ла промышленного продукта (САБ/САМ/РОМ-2007)" (Москва, 2007), XIV-ой международной паучно-практической конференции "Современные техника и технологии" (Томск, 2008), международной научной конференции "Информация, сигналы, системы вопросы методолоши. анализа и синтеза" (Таганрог, 2008), международной научной конференции "Математика, кибернетика, ипформатика" (Ярославль, 2008)

Результаты обсуждались на семинаре "Моделирование и анализ информационных систем" кафедры теоретической информатики Ярославского государственного университета им П Г Демидова (2006-2008 гг)

Публикации По теме диссертации опубликовано 7 научных работ Из них 3 опубликованы в изданиях, входивших в перечень ВАК на момент публикации и находящихся в перечне ВАК в настоящий момент

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

Структура и объем диссертации Диссертация состоит из введения, трех глав и заключения Объем работы со( тавляех 122 страницы в формате машинописного текста Список литературы содержит 88 наименований

Краткое содержание работы

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

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

Автоматное программирование было разработано для решения задач логического управления По мнению профессора Шалыто, существующие под-

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

Идея применения автоматов была развита в многочисленных работах его последователей Предлагались различные варианты размещения внешних вызовов в автоматах. В одних случаях внешние воздействия можно вызывать только на переходах, в других — разрешаются воздействия при входе и выходе из состояния Несколько состояний группируются в одно состояпие В результате появляется иерархия состояний по вложенности Сравнительно сложная программа включает в себя несколько автоматов, поэтому важны способы их взаимодействия Предлагались библиотеки, поддерживающие автоматную разработку программ Реализованы вспомогательные утилиты Следует отметить UmMod — среду разработки автоматных программ на языке Java Она оказала важное влияние па данную работу

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

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

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

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

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

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

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

4Шалыто, А А Switch-технология Алгоригмиза1щя и программирование задач логически с о управлении -СИВ Наука, 1998 — 628 с

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

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

Верификатор Xeve использует ся для проверки esterel программ Esterel пршрамма представляется в виде набора конечных автоматов Описание сохраняется в формате BLIF (Berkeley Logical Interchange Format) Перед верификацией строится пространство состояний программы в виде BDD (Binaiy Derision Diagrams) Инструмент Xeve может выполпять две функции минимизация автомата и проверка статуса выходных сигналов Вторая функция используется для верификации Можно проверить два типа утверждений 1) выходной сигнал никогда пе генерируется, 2) выходпой сигнал генерируется в каждом инстепте

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

что тревожный сигнал никогда не геперируется Существует приложение, позволяющее описывать проверяемые свойства на языке LTL (Linear Time Temporal Logic)

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

Объединение автоматного программирования и синхронного подхода привело к созданию вариации ЛП, названной синхронно-автоматным программированием

Модель программы состоит из двух типов модулей- автоматов и синхронных сетей. Автомат А = (Q,q:,X, Y/l>) состоит из множества состояний Q, начального состояния r/i, множества входных X и выходпых Y сигналов, функции переходов Ф. Функция переходов Ф Q х L —> Q х R определяет условие перехода I е L, список генерируемых сигналов г е R и новое состояние Условие перехода представляет из себя логическую формулу над значениями входных сигналов L = 0 | 1 | j, \ L Л L \ L V L \ -iL | (L) Выходные сигналы могут генерироваться только па переходах Допускаются петли (исходное и конечное состояния совпадают)

Синхронная сеть N = (I, X, У, G) используются для группировки подсистем Подсистемами являются автоматы и сипхроппые сети Сначала синхронные сети создаются только из автоматов, затем уже созданные сети могут быть использованы при построении других сетей Все, что синхроппая сеть делает, выходные сигпалы одних подсистем с входными сигналами других X — набор синхропных подсистем, использованных для построения данной синхронной сети Синхронная сеть сама обладает интерфейсными сигналами Л и Y — множество входных и выходпых сигналов соответственно Интерфейсные сигналы сети используются наравне с сигналами ее компо-

центов С — отношение смежности па множестве (Игнатов, опреде шющее группы связанных сигналов

Синхронно-автоматная программа преобразуется в ирохрамму на языке esteiel Отдельные модули исходной модели преобразуются в апалогичиьте модули я шка esterei Сохраняют ся имена компонентов

С- \ программу можпо описать текстуально в формате XML Однако такое представление крайне неудобно для разработки программы Поэтому была создана система визуальных обозначений на основе языка UML Отображение компонентов иро1раммы на элементы UML соответствует интуитивным ожиданиям Автоматы моделируются с помощью диахрамм автоматов, состояния соответствуют состояниям UML Метки на дугах имеют специальным формат Синхронные сети изображаются с помощью диаграмм композитной структуры (Composite Structuie Diagram) Сигналы авюлытов и синхронных систем моделируются портами

Рис 1 Среда разработки сиихрошю-аитоматиых иршрамм Диа1рамма данных

Структуру среды разработки удобно представить с помощью двух диаграмм На рисунке 1 показаны пути преобразования данных в процессе работы Рисунок 2 содержит соответствующие инструменты, используемые для

Рис 2 Среда разработки синхронно-автоматных программ Диаграмма инструментов

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

Область рисунка, окруженная пунктирной рамкой, является опциональной Так, на рис 1 компонент «Проверяемые свойства LTL» является необязательным Проверяемые свойства можпо определять сразу на языке csterel (прямоугольник «Проверяемые свойства esterei»)

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

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

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

Верификация С-А программы выполняется инструментом Xeve Проверяемые свойства должны быть описаны па языке esterel в виде отдельных модулей. Взаимодействие с основной программой (полученной ранее), как правило, не представляет затруднении, тк. структура esterei программы в основном повторяет структуру С-А модели, хотя знание языка esterei определенно является необходимым. Основная щипрамма объединяется с модулями проверки Дальше процедура верификации совпадает с той, которая применяется для чистого языка esterei Процедура в большей части автоматизировала В случае получение отрицательного ответа (свойство нарушено), необходимо проинтерпретировать трассу, приводящую к ошибке Отдельно стоит отметить инструмент TempEst, служащий надстройкой процесса верификации С его помощью свойства можно задавать на языке LXL

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

Первый пример — арбитры шины Задача арбитра шины заключается в управ тении доступом к разделяемому ресурсу Только один из пользователей имеет возможность получить доступ к шине в каждый момент времени Необходимо поддерживать справедливость в предоставлении дост} па к ресурсу Пользователь, непрерывно запрашивающий ресурс, должен пе позднее чем через заданное время получить доступ

Решение этой задачи очень специфично для синхронного программирования Тем пе менее, она была успешно реализована синхронно-автоматным способом Использованы четыре автомата и две синхронных сети Решение наглядно представляется при помощи диаграмм 1ЖЬ Были проверены все важные свойства

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

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

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

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

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

Это наиболее сложный из всех реали-юваппых примеров В нем использовано 9 автоматов и одна синхронная сеть Кроме того, для проверки некоторых с войств были носгросны дополнительные элементы

Программа предполагает существование специальных внешних объектов таких, как таймеры и регистры Некоторые функции удобнее реализовать внсшпими устройствами.

Проверяемые свойс1ва, главным образом, относятся к деталям реализации программы Чем сложнее программы, тем больше деталей, за которыми трудно уследить. Разработка программы сопровождалась контролем при помощи верификатора. Описано более двух десятков свойств Выли обнаружены и исправлены ошибки Таким образом, можпо утверждать, что функция верификации способствует разработке качественной про! раммы

В заключении подводятся итоги применения синхронно-автоматною подхода для решения задачи верификации автоматных программ

Основные результаты и выводы

В рамках диссертации получепы следующие резулыаты

• Разработана формальная модель автоматной программы, основанная на синхронном подходе Получившаяся вариация автоматного программирования была названа синхронно-автоматным программированием

• Разработан метод верификации синхронно-автоматных про1 рамм с использованием верификатора Хеуе.

• Разработала графическая нотация описания и XML формат хранения синхронно-автоматпой программы Создана программная среда разработки и верификации синхронно-автоматных программ.

Публикации ио теме диссертации

1 Кубасов, С В Синхронная модель автоматной программы / С В Кубасов, В А. Соколов // Моделирование и анализ информационных систем - 2007. - Т.14, № 1 - С. 11-18

2 Кубасов, С В. Верификация синхронно-автоматных программ // Моделирование и анализ информационных систем — 2007. — Т 14, № 4 — С 20-27

3 Кубасов С.В Система разработки синхронно-автоматных программ для решения задач логического управления // Материалы международной конференции и выставки CAD/CAM/PDM-2007 — М.. Институт проблем управления РАН, 2007. — С. 53-54

4 Кубасов, С В Синхронно-автоматное программирование для задач логического управления // Вопросы современной науки и практики. — Тамбов Тамбовский государственный технический университет, 2007 — Т 2, №4(10) - С 230-233

5 Кубасов, С В Разработка и верификация синхронно-автоматных программ на примере микроволновой печи // Труды XIV международной научно-практической конференции "Современные техника и технологии". — Томск. Томский политехнический университет, 2008. — Т 2. -С 324-325

О Кубасов, С В Разработка и верификация автоматных программ средствами синхронного программировании // Материалы международной научной конференции "Информация, сигналы, системы вопросы методологии, анализа и синтеза". — Таганрог Изд-во ТТИ ЮФУ, 2008 — Т 5 Радиоэлектронные системы и устройства. - С. 26-32

7 Кубасов, С В Верификация синхронно-автоматных программ с использованием 1ЯЪ // Моделирование и анализ информационных систем -2008. — Т 15, № 2 - С 46-49

В работе [1] автором разработана синхронная модель автоматной программы Все остальные работы были выполнепы без соавторов

Лицензия ЛР № 071542 от 24 11 97 г Редакционно-издательский центр Международного университета бизнеса и новых технологий /института/ Подписано в печать 06 10 2008 Заказ № 1038

Формат А5 Уч -изд л - 1 Тираж 100 экз Отпечатано в Редакционно-издательском центре г Ярославль, уч Володарского, 103, тел 71-50-36

Введение

Глава 1. Автоматное программирование для решения задач логического управления.

1.1. Автоматное программирование или Switch-технология

1.2. Проблема верификации автоматных программ.

1.3. Синхронный подход.

1.4. Синхронный подход в языке esterel

Глава 2. Среда разработки и верификации синхронно-автоматных программ.

2.1. Формальная модель автоматной программы

2.2. Форматы данных

2.3. Верифицируемые свойства. Язык TempEst.

2.4. Структура среды разработки.

Глава 3. Примеры

3.1. Пример 1: Арбитр шины

3.2. Пример 2: Часы-будильник.

3.3. Пример 3: Микроволновая печь

3.4. Выводы.

Актуальность работы С 90-х годов XX века в России развивается автоматное программирование. Профессор А.А. Шалыто предложил использовать switch-технологию (другое название автоматного программирования) для решения задач логического управления [41]. Ее основная идея в использовании автоматов для кодирования логики программы. Допускается применять другие подходы для решения отдельных подзадач.

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

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

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

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

Задачи логического управления часто предъявляют критические требования к надежности программного обеспечения. Цифровые устройства сейчас можно встретить практически во всех сферах человеческой жизни. От их бесперебойного функционирования часто зависит жизнь людей. Со временем количество и сложность устройств логического управления только возрастают. Поэтому задача верификации не теряет, а, наоборот, усиливает свою актуальность. Ручная проверка — трудоемкое занятие. Гораздо удобнее и надежнее поручить выполнение этой задачи компьютерной программе.

Задача верификации возникла несколько десятилетий назад. К настоящему моменту уже выработаны разнообразные подходы ее решения [16]. Среди ученых, внесших значительный вклад в решение этой задачи, можно выделить Н.А. Анисимова [48], O.JL Бандман [2, 3], Ю.Г. Карпова [14, 15], И.A. JIo-мазову [23], В.А. Непомнящего [26], А.К. Петренко [22], P.JI. Смелянского [32], В.А. Соколова [33], P.A. Abdulla [46], G. Berry [52-55], М.С. Browne [58, 59], К. Cerans [45], Е.М. Clarke [61, 62], Е.А. Emerson [61, 63, 64], A. Finkel [68, 69], Jr.O. Grumberg [16, 62], G.L. Holzmann [72], K. Jensen [77-79], Z. Manna [80], A. Pnueli [80], Ph. Schnoebelen [69], N. Sidorova [83], J. Sifakis [84, 85]. Рассмотрим некоторые из подходов.

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

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

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

Темпоральные логики используются для спецификации параллельных систем. При помощи темпоральных формул удобно описывать свойства, выражающие порядок событий во времени. Спецификация системы может быть описана набором темпоральных формул. Автоматизация доказательства темпоральных формул на моделях связана с изобретением Кларка и Эмерсона [63]. Позднее алгоритм проверки был улучшен Кларком, Эмерсоном и Систлой [61].

Алгоритм проверки на моделях связан с обходом всех состояний системы. Часто количество состояний слишком велико, чтобы быть представленным в памяти компьютера. Изобретение МакМилланом в 1987 году упорядоченных двоичных разрешающих диаграмм (OBDD) позволило значительно увеличить размеры систем, поддающихся верификации. OBDD позволяют компактно представлять состояния, потребляя меньше памяти.

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

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

Задача верификации автоматных программ находится в процессе исследования. Можно выделить две группы, активно работающих над этой проблемой. В Ярославском государственном университете им. П.Г. Демидова на кафедре теоретической информатики проводятся исследования по моделированию, спецификации и верификации автоматных программ. Результаты работ обсуждаются на семинаре "Моделирование и анализ информационных систем" и конференциях [20]. В работу вовлекаются студенты [21]. Команда Шалыто А.А., автора технологии автоматного программирования, также достигла определенных успехов в разработке среды для верификации автоматных программ.

В работе [18] предлагается иерархическая модель автоматных программ. Модель рассматривается на примере системы управления кофеваркой. В работе [4] предлагается способ моделирования, спецификации и верификации автоматных программ. Используется верификатор SPIN, логика LTL. Рассмотрен пример системы управления банкоматом. Одним из развитий иерархической модели автоматных программ [18] является модель [9], использующая формализм сетей Петри. Разработка программы выполняется в UniMod, применяется верификатор CPN/Tools [60], рассмотрен пример системы управления кофеваркой. Получено свидетельство об официальной регистрации программы для ЭВМ [31].

На кафедре технологий программирования СПбГУ ИТМО были получены в том числе следущие результаты [13, 17] . В работе [7] рассматривается техника верификации автоматных программ, состоящих из одного конечного автомата. Описывается преобразование автомата в структуру Крппке, выражение темпоральных свойств на языке CTL, верификация по модели (метод "Model Checking") и построение сценария для исходного автомата, если был найден контрпример. Техника верификации демонстрируется на примере универсального инфракрасного пульта для бытовой техники [8]. Применение метода Model Checking также исследуется в работах [5, 6].

Можно заметить, что все авторы используют Model Checking. Главное различие наблюдается в моделях. Данная работа не является исключением.

Наиболее обстоятельное описание АП можно найти в книге [41]. Она была взята за основу. Было сделано несколько уточнений и ограничений, в результате получилась модель автоматной программы.

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

Язык синхронного программирования esterel разрабатывался для аналогичного круга задач, что и автоматное программирование. В отличие от АП, в esterel был изначально заложен прочный теоретический фундамент. В esterel существует базис — подмножество языка, на котором можно определить все его операторы. Программа на языке esterel — это уже модель, готовая для верификации. Существует верификатор Xeve для проверки esterel программ.

АП и язык esterel помимо общей задачи роднит тот факт, что оба они используют бинарные сигналы. Esterel допускает сигналы с дополнительными значениями. Однако значения не используются в процессе верификации, только статус сигнала ("true" — "false" или "присутствует" — "отсутствует") принимается во внимание.

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

Xeve — это верификатор для esterel программ, представляемых в виде конечных автоматов. Xeve предлагает дружественный графический пользовательский интерфейс. Компилятор языка esterel преобразует программу в систему в систему логических уравнений с защелками (latch), которые неявно определяют конечный автомат. Xeve работает с неявно заданным конечным автоматом. Внутри верификатора автомат описывается с помощью бинарных диаграмм решений (Binary Decision Diagrams).

Верификатор Xeve был разработан совместно институтом Inria1 и Ecolc des Mines de Paris2 в рамках исследовательского проекта TICK3. Технология оказалось многообещающей. Было решено адаптировать ее для промышленного использования. Так появилась компания Estercl Technologies. Сейчас Esterel Techonlogies может гордиться удачными проектами со многими известными заказчиками: Airbus, Elbit Systems, Intertechnique, Eurocopter и др4.

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

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

• Разработать метод верификации автоматных программ.

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

Научная новизна Все основные результаты являются новыми.

• Разработана формальная модель автоматной программы, учитывающая наиболее важные идеи автоматного программирования.

• К автоматному программированию был применен синхронный подход. Уточнена временная модель. Поведение программы стало детерминиро

1http://www.mria.fr/index.en.html

2http://www.ensmp.fr/

3 http: / /www .inri a. fr/recherche /equipes/tick .en .html

4http://www.esterel-technologies.com/technology/success-stories/ ванным. Разработана вариация автоматного программирования — синхронно-автоматное программирование.

• Разработаны способы верификации синхронно-автоматных программ при помощи существующих программных инструментов языка esterel. Использован верификатор Xeve.

• Создана программная среда разработки и верификации синхронно-автоматных программ.

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

Разработана и реализована программная система разработки и верификации синхронно-автоматных программ. Ее применение упрощает и ускоряет разработку и проверку указанного класса программ.

Апробация работы Результаты диссертации докладывались на 7-ой международной конференции и выставке "Системы проектирования, технологической подготовки производства и управления этапами жизненного цикла промышленного продукта (CAD/САМ/PDM-2007)" (Москва, 2007), XIV-ой международной научно-практической конференции "Современные техника pi технологии" (Томск, 2008), международной научной конференции "Информация, сигналы, системы: вопросы методологии, анализа и синтеза" (Таганрог, 2008), международной научной конференции "Математика, кибернетика, информатика" (Ярославль, 2008).

Результаты обсуждались на семинаре "Моделирование и анализ информационных систем" кафедры теоретической информатики Ярославского roсударственного университета им. П.Г. Демидова (2006-2008 гг.).

Участие в проектах Во время работы над диссертацией автор участвовал в следующих научных проектах:

1. Разработка формальных моделей распределенных систем и исследование их семантических свойств. РФФИ, грант № 07-01-00702.

2. Федеральная целевая программа "Исследования и разработки по приоритетным направлениям развития научно-технологического комплекса России на 2007-2012 годы". Проект № 2007-4-1.4-18-02 "Разработка технологии верификации управляющих программ со сложным поведением, построенных на основе автоматного подхода".

Публикации По теме диссертации опубликовано 7 научных работ. Из них 3 опубликованы в изданиях, входивших в перечень ВАК на момент публикации и находящихся в перечне ВАК в настоящий момент.

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

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

3.4. Выводы

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

В первом примере, пожалуй, было использовано слишком много компонентов для сравнительно простой задачи. Решение задачи было известно. Оно использует особенности синхронного подхода и языка esterel в частности. Программа на языке esterel значительно более компактна, чем решение в UML,диаграммах. С другой стороны, решение синхронно-автоматным подходом легче для понимания.

Декомпозиция задачи на подзадачи в соответствии с синхронно-автоматным подходом имеет неприятную особенность. Каждый компонент синхронной системы стремится инкапсулировать детали реализации. Интерфейс синхронных сетей и автоматов выставляет только набор сигналов. К сожалению, связи между сигналами не могут быть инкапсулированы. Хотя они не видны через интерфейс, они должны учитываться при разработке. Необдуманное использование компонентов может создать циклические зависимости. Esterel программа, полученная по такой программе, не будет компилироваться. Синхронно-автоматная модель не предлагает стандартных средств для описания таких зависимостей. Выход заключается в использовании комментариев на естественном языке. В том случае, если комментариев нет, единственным безопасным решением будет считать, что каждый выходной сигнал зависит от всех входных сигналов. Если необходимы более слабые условия, придется вникать в детали реализации конкретного модуля.

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

Средства проверки синхронно-автоматных программ доказали свою полезность. В совокупности было описано и проверено несколько десятков свойств. Использовался язык линейной темпоральной логики с операторами прошедшего времени. Надо заметить, что большинство проверяемых свойств относились к допущениям, принятым в процессе разработки. По техническому заданию было сформулировано намного меньше свойств. Данный факт можно объяснить тем, что постановка задачи дана неформально, в ней мало точных требований. Функция верификация позволила обнаружить и исправить ошибки, допущенные в программе. Практика показала, что процесс разработки программы и верификации свойств разумно выполнять параллельно. Как только оформляется в достаточной мере законченный фрагмент программы, следует подумать о том, какие его свойства можно проверить. Чем раньше будет обнаружена ошибка, тем дешевле обойдется ее исправление.

Заключение

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

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

Предложен и реализован алгоритм преобразования синхронно-автоматной модели в программу на языке esterel. Преобразование сохраняет структуру модели.

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

Написана программа автоматического преобразования модели синхронно-автоматной программы, сохраненной в XML формате, в программу на языке esterel. Программа прербразования выполняет полную проверку формата модели.

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

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

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

1. Ачасова, С.М. Корректность параллельных вычислительных процессов / С.М. Ачасова, 0.J1. Бандмап. — Новосибирск: Наука, Сибирское отделение, 1990. 252 с. — ISBN: 5-02-029334-2.

2. Бандман, O.JI. Проверка корректности сетевых протоколов с помощью сетей Петри // Автоматика и вычислительная техника. — № 6. — 1986. — С. 82-91.

3. Васильева, К.А. Верификация автоматных программ с использованием LTL / К.А. Васильева, Е.В. Кузьмин // Моделирование и анализ информационных систем. — 2007. — Т.14, № 1. — С. 3-14.

4. Вельдер, С.Э. О верификации простых автоматных программ на основе метода "Model Checking" / С.Э. Вельдер, А.А. Шалыто // Информационно-управляющие системы. — 2007. — № 3. — С. 27-38.

5. Вельдер, С.Э. Универсальный инфракрасный пульт для бытовой техники / С.Э. Вельдер, Ю.Д. Бедный // СПбГУ ИТМО. Кафедра «Технологии программирования» Электронный ресурс]. — Разд. «Проекты». — Режим доступа: http://is.ifmo.ru/, свободный.

6. Виноградов, Р.А. Верификация автоматных программ средствами CPN/ Tools / Р.А. Виноградов, Е.В. Кузьмин, В.А. Соколов // Моделирование и анализ информационных систем. — 2006. — Т. 13, № 2. — С. 4-15.

7. Гуров, B.C. Исполняемый UML из России / B.C. Гуров, А.С. Нарвский, А.А. Шалыто // PC Week/RE. 2005. - № 26. - С. 18-19.

8. Карпов, Ю.Г. Теория автоматов. — СПб.: Питер, 2003. — 208 с.

9. Карпов, Ю.Г. Формальное описание и верификация протоколов на основе CSS // Автоматика и вычислительная техника. — Рига, 1986. — № 6. — С. 21-30.

10. Кларк, Э.М. Верификация моделей программ. Model Checking / Э.М. Кларк, О. Грамберг, Д. Пслед. М.: МЦНМО, 2002. - 416 С.

11. Корнеев, Г.А. Верификация автоматных программ / Г.А. Корнеев,

12. B.Г. Парфенов, А.А. Шалыто // Тезисы докладов Международной научной конференции, посвященной памяти профессора A.M. Богомолова. "Компьютерные науки и технологии". — Саратов: СГУ, 2007. — С. 66-69.

13. Кузьмин, Е.В. Иерархическая модель автоматных программ // Моделирование и анализ информационных систем. — 2006. — Т.13, № 1. —1. C. 27-34.

14. Кузьмин, Е.В. Моделирование, спецификация и верификация "автоматных" программ / Е.В. Кузьмин, В.А. Соколов // Программирование. — 2008. — № 1. — С. 38-60.

15. Кузьмин, Е.В. О верификации "автоматных" программ / Е.В. Кузьмин, В.А. Соколов // Актуальные проблемы математики и информатики. Сборник статей к 20-летию факультета ИВТ ЯрГУ им. П.Г. Демидова. — Ярославль: ЯрГУ, 2006. — С. 27-32.

16. Кулямин, В. Формализация интерфейсных стандартов и автоматическое построение тестов соответствия / В. Кулямин, А. Петренко, В. Рубанов, А. Хорошилов // Информационные технологии. — № 8. — 2008. — С. 2-7.

17. Ломазова, И.А. Вложенные сети Петри: моделирование и анализ распределенных систем с объектной структурой. — М.: Научный мир, 2004. — 208 с.

18. Лукьянова, А.П. Моделирование и верификация потоков данных на диаграммах состояний: Бакалаврская работа / А.П. Лукьянова; СПбГУ ИТ-МО, каф. «Компьютерные технологии». — СПб., 2005. — 60 с.

19. Наумов, А.С. Объектно-ориентированное программирование с явным выделением состояний: Бакалаврская работа / А.С. Наумов.; СПбГУ ИТ-МО, каф. «Компьютерные технологии». — СПб., 2004. — 209 с.

20. Непомнящий, В.А. Практические методы верификации программ // Кибернетика. — № 2. — 1984. — С. 21-28.

21. Пак, С.В. Задача об обедающих философах / С.В. Пак, А.А. Шалы-то // СПбГУ ИТМО. Кафедра «Технологии программирования» Электронный ресурс]. — Разд. «Проекты». — Режим доступа: http://is.ifmo. га/, свободный.

22. Приемы объектно-ориентированного проектирования. Паттерны проектирования / Э. Гамма, Р. Хелм, Р. Джонсон, Дж. Влиссидес. — СПб.: Питер, 2004. — 366 с.

23. Робачевский, A.M. Операционная система Unix / A.M. Робачевский, С.А. Немнюгин, О.Л. Стесик. — 2-е изд., перераб. и доп. — СПб.: БХВ-Петербург, 2007. — 656 с.

24. Санкт-Петербургский Государственный Университет Информационных Технологий, Механики и Оптики. Кафедра «Технологии программирования» Электронный ресурс]. — 2002- . — Режим доступа: http://is.ifmo. ги/, свободный.

25. Смелянский P.JI. Взаимосвязь программы и вычислительной среды // Вычислительные системы и вопросы анализа решений. — М., МГУ, 1989.

26. Соколов, В. А. Моделирование распределенных систем и анализ их семантических свойств Текст]: дис. . доктора физико-математических наук : 01.01.09 : утв. 8.12.2006 / Соколов Валерий Анатольевич. — Ярославль, 2006. 318 с.

27. Страуструп, Б. Язык программирования С++: Специальное издание:

28. Пер. с англ. — М.; СПб.: «Издательство Бином» — «Невский Диалект», 2002. — 1099 е., ил.

29. Шалыто, А.А. Алгоритмизация и программирование задач логического управления. СПбГУ ИТМО, 1998. — 56 с.

30. Шалыто, А.А. Логическое управление. Методы аппаратной и программной реализации алгоритмов. — СПб.: Наука, 2002. — 784 с.

31. Шалыто, А.А. Методы объектно-ориентированной реализации реактивных агентов на основе конечных автоматов /А.А. Шалыто, Л.А. Наумов // Искусственный интеллект. — 2004. — № 4. — С. 756-762.

32. Шалыто, А.А. Программирование с явным выделением состояний / А.А. Шалыто, Н.И. Туккель // Мир ПК. 2001. - № 8. - С. 116121; № 9. - С. 132-138.

33. Шалыто, А.А. Switch -технология — автоматный подход к созданию программного обеспечения «реактивных систем» / А.А. Шалыто, Н.И. Туккель // Программирование. — 2001. — № 5. — С. 45-62.

34. Шалыто, А.А. Switch-тсхиология. Алгоритмизация и программирование задач логического управления. — СПб.: Наука, 1998. — 628 с.

35. Шамгунов, Н.Н. State Machine — новый паттерн объектно-ориентированного проектирования / Н.Н. Шамгунов, Г.А. Корнеев, А.А. Шалыто // Информационно-управляющие системы. — 2004. — № 5. — С. 13-25.

36. Шопырин, Д.Г. Объектно-ориентированный подход к автоматному программированию / Д.Г. Шопырин, А.А. Шалыто // Информационно-управляющие системы. — 2003. — № 5. — С. 29-39.

37. Шопырин, Д.Г. Синхронное программирование / Д.Г. Шопырин,

38. A.А. Шалыто // Информационно-управляющие системы. — 2004. — № 3. С. 35-42.

39. Abdulla, Р.А. General Decidability Theorems for Infinite-State Systems / Parosh Aziz Abdulla, Karlis Cerans, Bengt Jonsson, Yih-Kuen Tsay // Logic in Computer Science. — 1996. — P. 313-321.

40. Abdulla P. Verifying Programs with Unreliable Channels / P. Abdulla,

41. B. Jonsson // Proc. Logic in Сотр. Science (LICS'93). 1993. - P. 160-170.

42. Andre, C. Representation and Analysis of Reactive Behaviors: A Synchronous Approach / C. Andre // Computational Engineering in Systems Applications (CESA), IMACS Multiconference. Lille, France. - 1996, July. - P. 1929. - ISBN 2-9502908-7-6.

43. Anisimov, N.A. Two-Levels Formal Model for Protocol Specification Based on Petri Nets / N.A. Anisimov, A.A. Kovalenko, P.A. Postupalski // Proceedings of the IFIP TC6 Int. Symp. "Network Information Processing Systems". — 1993. P. 143-154.

44. Barros, T. Formal specification and verification of distributed component systems: PhD thesis: defence date: 25.11.2005 / T. Barros; Universite de Nice; INRIA Sophia Antipolis. — France, 2005. — 158 pages.

45. Benveniste, A. The Synchronous Languages 12 Years Later: Invited Paper / A. Benveniste, P. Caspi, S.A. Edwards, N. Halbwachs, P. le Gurnic,

46. R. de Simone // Proceedings of the IEEE. — 2003, January. — vol. 91, No. 1. — P. 64-83.

47. Berry, G. Incremental development of an HDLC protocol in esterel: Technical report 1031 / Gerard Berry, Georges Gonthier. — France: Inria, Sophia-Antipolis, 1989. — 48 pages.

48. Berry, G. The Esterel v591 System Manual: Документация к программному обеспечению Esterel Compiler, version 5.91. Ecole des Mines de Paris (EMP), ARMINES, and INRIA. 2000, 5 June. - 132 pages.

49. Berry, G. The Esterel v5 Language Primer, version v591: Документация к программному обеспечению Esterel Compiler, version 5.91. Ecole des Mines de Paris (EMP), ARMINES, and INRIA. 2000, 5 June. - 142 pages.

50. Berry, G. The constructive semantics of pure esterel. Draft version 3 Черновой вариант документации]. — 1999, 2 July. — 160 pages.

51. Berry, G. The foundations of Esterel / Gerard Berry // Proof, Language, and Interaction: Essays in honour of Robin Milner / edited by Gordon Plotkin, Colin Stirling and Mads Tofte. MIT Press, 2000. — P. 425-454.

52. Bouali, A. Xeve: an Esterel Verification Environment : Version vl3 : Rapport technique №0214 / Amar Bouali ; Inria, Institut National de Recherche en Informatique et en Automatique. — France, 1997. — 23 pages. — ISSN 0249-0803.

53. Bouali, A. Xeve, and esterel verification environment // Computer aided verification. Berlin: Springer, 1998. - P. 500-504. — ISBN 978-3-54064608-2.

54. Browne, M.C. Characterizing finite Kripke structures in propositional temporal logic / M.C. Browne, E.M. Clarke, O. Grumberg // Theoretical Computer Science. — 1988. — Vol. 59, No. 1-2. — P. 115-131.

55. Browne, M.C. Reasoning about networks with many identical finite-state processes / M.C. Browne, E.M. Clarke, O. Grumberg // Information and Computation. — 1989. — Vol. 81, No. 1. — P. 13-31.

56. CPN Tools. Computer Tool for Coloured Petri Nets Электронный ресурс] / CPN Group, University of Aarhus, Denmark. — 2001- . — Режим доступа: http://wiki.daimi.au.dk/cpntools/cpntools.wiki, свободный.

57. Clarke, E.M. Automatic verification of finite-state concurrent systems using temporal logic specifications / E.M. Clarke, E.A. Emerson, A.P. Sistla // ACM transactions on Programming Languages and Systems. — Vol. 8, No. 2. 1986. - P. 244-263.

58. Clarke, E.M. Model Checking / E.M. Clark, O. Grumberg, D.A. Peled. -The MIT Press, 1999. — 314 pages.

59. Emerson, E.A. Branching Time Temporal Logic and the Design of Correct Concurrent Programs. PhD thesis. — Harvard University, 1981.

60. Emerson, E.A. Temporal and modal logic // Handbook of Theoretical Computer Science, vol. B. — 1991. — P. 995-1072.

61. Esterel synchronous language web main page Электронный ресурс]: [Зеркало сайта, посвященного синхронному языку esterel] / Inria Sophia Antipolis — Mediterranee. — Режим доступа, http://www-sop.inria.fr/ esterel.org/files/, "свободный.

62. Esterel verification environment Электронный ресурс]: [Главная страница раздела, посвященного верификатору Xcvc] / Inria Sophia Antipo-lis — Mediterranee. — Режим доступа, http://www-sop.inria.fr/meije/ verification/esterel/index.html, свободный.

63. Executable UML. UniMod Электронный ресурс]: [Сайт проекта UniMod] / eVelopers Corporation. — 2003- . — Режим доступа: http://unimod. sourceforge.net/, свободный.

64. Finkel, A. Reduction and covering of infinite reachability trees // Information and Computation. — Vol. 89, Issue 2. — 1990. — P. 144-179.

65. Finkel, A. Well-structured transition systems everywhere! / A. Finkel, Ph. Schnoebelen // Theoretical Computer Science. — Vol. 256, № 1-2. — 2001. P. 63-92.

66. Functional Description. Warm-up & prelubrication logic. Generator Control Unit. / copyright Norcontrol as, 1993. — № AO-0054-A/11/10/93.

67. Holzmann, G.J. Design and Validation of Computer Protocols. — Prentice Hall, New Jersey, 1991. P. 512.

68. Inrea Sophia Antipolis — Mediterranee Электронный ресурс]. — Режим доступа, http://www-sop.inria.fr/, свободный.

69. Jagadeesan, L.J. On the bounded-fairness support in TempEst 1.2: Документация к программному обеспечению TempEst / L.J. Jagadeesan, С. Puchol. 1995, 10 March.

70. Jensen, K. Coloured Petri Nets: Basic Concepts, Analysis Methods, and Practical Use. — Springer, 1997.

71. Jensen, K. Coloured Petri Nets. Basic Concepts, Analysis Methods and Practical Use // Vol. 1: Basic Concepts. EATCS Monographs on Theoretical Computer Science. — Springer-Verlag, 1992.

72. Jensen, K. Coloured Petri Nets. Basic Concepts, Analysis Methods and Practical Use // Vol. 2: Analysis Methods. EATCS Monographs on Theoretical Computer Science. — Springer-Verlag, 1994.

73. Manna, Z The Modal Logic of Programs / Z. Manna, A. Pnueli // Proceedings of the 6th Colloquium, on Automata, Languages and Programming. — 1979. — P. 385-409.

74. Potop-Butucaru, D. Compiling Esterel / D. Potop-Butucaru, S.A. Edwards, G. Berry. Springer, 2007. - 335 pages. - ISBN 978-0-387-70626-9.

75. Puchol, С The TempEst program verification toolset: Слайды: Документация к программному обеспечению TempEst. — 1995.

76. Sidorova, N. Surface measures on paths in an embedded Riemannian manifold. — PhD thesis. — 2003.

77. Sifakis, J. Building models of real-time systems from application software / J. Sifakis, S. Tripakis, S. Yovinc // Proceedings of the IEEE, Special issue on modeling and design of embedded. — Vol. 91, № 1. — 1993. — P. 100-111.

78. Sifakis, J. Modeling Real-Time Systems-Challenges and Work Directions // Lecture Notes in Computer Science. Vol. 2211. - 2001. — P. 373-389.

79. Synchronous programming of reactive systems / Nicolas Halbwachs. — Springer, 1993. 192 pages. — ISBN 0792393112.

80. The csterel language Электронный ресурс]: [Главная страница раздела, посвященного языку estcrel] / Inria Sophia Antipolis — Mediterranee. — Режим доступа, http://www-sop.inria.fr/meije/esterel/esterel-eng.html, свободный.