Рис. 5. Схема связей автомата ARemote (а). Граф переходов автомата ARemote (б) В рассматриваемом примере модель Крипке для автомата, построенная по схеме ССВВ, будет изоморфна графу на рис. 6.

В модели Крипке, изображенной на рис. 6, состояния-события и состояниявыходные воздействия указаны явно. При интерактивном моделировании совместно с исполнением и визуализацией [25, 26] их целесообразно обозначать, как и в исходном автомате, просто метками на дугах.

Итак, CTL-модель готова. Приведем теперь пример CTL-формулы, справедливость которой можно устанавливать верификацией: ¬E[¬(Y=6)U(Y=1)].

Смысл этой формулы состоит в следующем: в состояние 1 нельзя попасть, минуя состояние 6 (нельзя попасть в рабочий режим, минуя сообщение на экране).

Эта формула справедлива для состояний 4, 5, 6 исходного автомата и только для них (для модели Крипке таких состояний больше).

Во второй схеме не будем абстрагироваться от входных переменных, а представим автомат моделью Крипке «со всей полнотой» относительно входных воздействий. В исходном автомате переходы могут быть заданы не полностью – могут существовать не указанные петли. Это означает, что для некоторого состояния (некоторых состояний) дизъюнкция формул, составленных из входных переменных, которые помечают переходы из него по одному и тому же событию E, не является тавтологией.

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

Это, конечно же, не изменит семантику автомата, а лишь полностью опишет его поведение. В конечном счете, в автомате из каждого состояния по каждому событию должно исходить 2n переходов, где n – общее число входных переменных автомата. При этом каждому переходу соответствует набор значений всех переменных (или множество истинных переменных). После получения полного автомата преобразуем его в модель Крипке по общей схеме (разд. 2.1) с одной модификацией: для каждого состояния-события добавим во множество его атомарных предложений набор входных переменных, истинных на том переходе, на котором находится рассматриваемое состояние-событие. Таким образом, во множество атомарных предложений по отношению к обобщенной схеме добавились еще и входные переменные. Достоинство такой схемы (несмотря на ее расточительность, освобождение от которой будет описано ниже) в том, что она и только она позволяет модели Крипке полностью отражать поведение исходного автомата.

генерируемых состояний для модели Крипке, а достоинством – полнота.

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

Множество атомарных предложений по отношению к предыдущей схеме также изменим.

Рассмотрим исходный автомат без дизъюнкций на переходах. Если такие переходы существуют, создадим эквивалентные переходы для каждого дизъюнкта, а сами переходы с дизъюнкциями удалим. В качестве примера можно разбить переход “(e4 | e1&x1) / z11” графа ARemote, изображенного на рис. 5,б, на два перехода: “e4 / z11” и “e1&x1 / z11”.

Добавим в автомат состояния, соответствующие событиям, входным и выходным переменным так, как это было сделано в первой схеме (разд. 2.2), но с одним отличием: во множества атомарных предложений на состояниях-событиях добавим входные переменные в том виде, в котором они присутствуют на переходах (вместе с отрицаниями, если они есть). Таким образом, в состав множества всех атомарных формул модели входят следующие элементы, и только они: состояния; события; выходные воздействия; все литералы, составленные из входных переменных (сами переменные и их отрицания). Кроме того, в атомарные предложения каждого полученного состояния-события добавим все литералы, составленные из несущественных входных переменных для данного перехода (несущественными будем называть те переменные исходного автомата, которые не обозначены на рассматриваемом переходе). Таким образом, будем добавлять на одно и то же состояние-событие и несущественные переменные, и их отрицания. С точки зрения синтаксиса и семантики темпоральной логики это допустимо: процесс обработки модели Крипке не предполагает совместность множества атомарных предложений состояния, так как интерпретирует эти предложения просто как строки. Причина такого обращения с несущественными переменными ясна: требуется обеспечить, чтобы любая ссылка на несущественную в данном состоянии-событии переменную, упомянутая в CTLформуле, давала истинный результат.

Не обязательно хранить все литералы, составленные из несущественных переменных в состоянии в явном виде. Важно лишь то, что во время обработки модели существенные и несущественные входные переменные интерпретируются раздельно: первые – в том виде, в каком они записаны на переходах исходного автомата, а вторые – «в двух экземплярах» (в прямом и инверсном виде).

Результат конвертации графа переходов автомата ARemote, выполненного с применением данной схемы, изображен на рис. 7.

0. Начальное состояние Размер модели на рис. 7 совпадает с размером модели, созданной по схеме «Состояния на событиях и выходных воздействиях». Вообще говоря, первая схема может рассматриваться по аналогии с третьей или второй, в которой полностью исключены входные воздействия. Аналогично, третью схему можно рассматривать как видоизменение второй, при котором отождествляются наборы значений несущественных переменных.

для «редуцированных» моделей.

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

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

Рассмотрим пример для автомата ARemote. Пусть требуется проверить свойство: «существует способ провести инициализацию устройства, не нажимая кнопку Reset». В терминах языка CTL с исходной семантикой данное свойство может быть записано следующим образом: E[(InEvent ¬ x0) U z00].

Эта формула не выполняется в состоянии Y=0 (рис. 7). На это, правда, и не стоило рассчитывать. Преобразуем формулу согласно третьей схеме:

!x0) U z00]. Вместо отрицания в языке CTL в формулу было внесено E[(InEvent другое атомарное предложение, являющееся отрицанием исходного.

Преобразованная формула уже верна для состояния Y=0 автомата.

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

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

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

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

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

Приведем несколько альтернативных способов моделирования автоматов.

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

Например, для автомата ARemote результатом будет модель на рис. 8.

2. Режим энергосбережения 1. Рабочий режим 4. Режим записи 3. Выбор раскладки 6. Сообщение на экране 5. Ожидание сигнала Рис. 8. Сокращенная модель ARemote (без событий и выходных переменных) 2. Для выделения существенных свойств автомата можно удалять части его графа переходов, оставляя только подграф, следя при этом за тем, чтобы не нарушалась качественная структура модели, обеспечивающая выполнение ее проверяемых свойств.

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

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

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

Примером задачи, иллюстрирующей эту проблему, является так называемая [27–31]: сгенерировать сигнал O (Output), как только одновременно возникнут два сигнала A и B. Сигнал R (Reset) инициализирует систему заново. На рис. 9 приведен автомат Мили, формализующий решение задачи ABRO.

Два управляющих сигнала и Reset ведут к четырем состояниям («A1A2…AnRO»), то для автомата Мили потребуется 2n состояний. Это означает, что размер автоматной модели растет экспоненциально по отношению к размерности задачи.

Итак, на этом обзор методов моделирования и спецификации завершен.

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

Глава 3. CTL-верификация автоматных программ Широко известные эффективные алгоритмы верификации CTL базируются на применении так называемой теории неподвижной точки [1, 33] совместно с существенным уменьшением размера модели. Такое уменьшение, как правило, происходит за счет применения технологии упорядоченных двоичных разрешающих деревьев. С другой стороны, пока используется программирование с явным выделением состояний, существенное уменьшение модели не всегда целесообразно, так как бывает связано с расходами на реализацию эффективных алгоритмов, в то время как их выигрыш во времени незаметен.

совершенствованию использования «автоматного» подхода к ветвящейся темпоральной логике. Временная сложность их подхода линейна по отношению к длине CTL-формулы и размеру спецификации системы. Интересный аспект этого подхода заключается в том, что пространственная сложность их алгоритма принадлежит классу алгоритмов NLOGSPACE по отношению к размеру модели M.

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

Несмотря на то, что данные исследования интересны и многообещающи, существует эффективный и твердо устоявшийся метод (Clarke, Emerson, 1981), основанный на другой парадигме (теории неподвижных точек), которая является концептуально более простой. Из этого метода рассматривается только «каркас», так как ниже будет описан другой, еще более простой, алгоритм CES (Clarke, Emerson, Sistla, 1986), который основан на переформулировке синтаксиса языка CTL. В этом (более простом) методе алгоритм дополнен таким образом, что позволяет строить подтверждающие сценарии для проверяемых формул.

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

Под локальной задачей верификации обычно понимается вопрос: выяснить для данных M, s,, справедливо ли M, s.

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

Когда число состояний невелико, как в нашем случае, это множество можно строить в явном виде.

Опишем идею их алгоритма на псевдокоде (рис. 10).

Как следует из рассмотрения текста программы, множество состояний, выполняющих формулу, строится индукцией по построению. Для подформул вида E[1U2] и A[1U2] множество выполняющих состояний получается с использованием методов неподвижной точки. При этом модель Крипке кодируется в упорядоченную бинарную разрешающую диаграмму.

Упорядоченные бинарные разрешающие диаграммы (OBDD – Ordered Binary Decision Diagram) – это мощная техника сжатия обрабатываемых данных, которая позволяет выполнять манипуляции над объектами прямо в сжатом виде, минуя распаковку, преобразование и обратную упаковку. Она заключается в том, что обрабатываемый объект неявно кодируется в непрерывный битовый поток из 2n бит, который потом интерпретируется как булева функция n переменных.

Именно для этой функции и строится корневой направленный ациклический граф, представляющий собой разрешающую диаграмму. Изначально этот граф может представлять собой полное двоичное дерево высоты n, уровень i которого соответствует i-й переменной, а каждый путь от корня к листу в нем соответствует определенному двоичному набору и значению функции на этом наборе (основное свойство). Очевидно, что для многих битовых строк, применяемых на практике, такое представление сильно избыточно, так как в полном дереве только число вершин уже равно 2n – число, равное длине битового образа. Однако, преобразуя (редуцируя) этот граф и не утрачивая при этом его основного свойства, можно добиться очень эффективного представления (сжатых) данных. Над разрешающими диаграммами можно выполнять логические операции.

Таким образом, многие задачи могут решаться прямо на ROBDD (Reduced OBDD), без составления таблиц истинности и без представления графов в явном виде. В частности, к таким задачам относится задача верификации (Model checking), для которой технология ROBDD успешно применяется, так как она позволяет работать с весьма обширными пространствами состояний.

3.3. Верификация модели в языке CTL (алгоритм CES) В разд. 1.3 дано определение синтаксиса языка CTL и введены несколько дополнительных темпоральных операций в нем. Сейчас одну из этих операций преобразуем в базовую – выразим темпоральную часть синтаксиса языка CTL через операции EX, EU, EG:

Алгоритм CES [1, 32], который описывается далее, наследует идею Кларка и Эмерсона: множество выполняющих состояний строится для каждой подформулы входной формулы (для каждого состояния создается список выполненных в нем подформул). Ввиду изменения набора базовых правил языка CTL, псевдокод, записанный на рис. 10, превращается в текст на рис. 11.

Рис. 11. Индукция по построению формулы в алгоритме CES что из исходного графа Крипке построен симметричный ему граф – граф, в котором все переходы заменены на противоположные.

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

2. Если известно выполняющее множество для формулы f, то можно построить его и для формулы ¬ f.

3. Аналогично, если известны выполняющие множества для f и g, то построим их 4. Сделаем «один шаг назад» от выполняющего множества для f – получим выполняющее множество для EX f.

5. Для построения выполняющего множества формулы E[f U g] вначале отмечаем в качестве выполняющих все вершины, в которых соблюдается формула g, а потом построим от них деревья «обратных путей» вдоль тех вершин, в которых выполнена формула f. Для этого пригодится симметричный граф.

6. Осталось только научиться строить выполняющее множество для EG f.

Это построение выполняется в три этапа:

исключаем из графа вершины, которые не выполняют формулу f;

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

строим обратные деревья, начиная от этих компонент, попутно помечая все посещенные вершины как выполняющие формулу f.

Трудоемкость итогового алгоритма составляет O( |f| (|S| + |R|) ) – растет билинейно относительно длины формулы и размеров модели.

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

3.4. Построение сценариев в модели Крипке Итак, требуется показать, что в данном состоянии s модели M выполняется (или не выполняется) формула f.

Алгоритм генерации сценария для CTL-формулы f 1. Если f – атомарное предложение, то просто предъявим описание состояния s в модели M – множество его атомарных предложений. В нем, в частности, содержится информация о выполняемости формулы f в данном состоянии s.

2. Доказательство ¬ f сводится к опровержению формулы f, и наоборот.

3. Для доказательства формулы f g докажем одну из формул f или g, а для опровержения – опровергаем обе формулы f и g.

4. Для доказательства EX f предъявим вершину в модели Крипке, в которую из вершины s есть переход и которая выполняет f. Такая вершина обязательно существует, иначе на этапе верификации не обнаружилось бы, что формула EX f верна. Опровержение EX f (доказательство AX¬ f ) подтверждается весьма просто, так как любой переход, который ведет из вершины s, будет вести только в вершину, выполняющую ¬ f. Таким образом, любой переход из этой вершины можно предъявить пользователю в качестве опровержения.

5. Доказательство формул E[f U g] и EG f выполняется рекуррентным способом с использованием методов 1–4 рассматриваемой схемы. Выполним рекуррентное разложение для этих формул:

Тогда для доказательства E[f U g] достаточно построить путь в графе, применяя шаг за шагом пункты 1–4 к рекуррентному разложению этой формулы, до тех пор, пока не попадем в вершину, выполняющую g.

Для доказательства EG f сделаем то же самое, пока не попадем в вершину, в которой уже были. Путь в этом случае, начиная с некоторого состояния, становится периодическим (рис. 12).

Опровержение формул E[f U g] и EG f выполняется аналогично опровержению EX f. Любой (бесконечный) путь, который начинается в текущей вершине, можно предъявить пользователю для рассмотрения, так как он (путь) не выполняет введенную формулу. Иначе говоря, вместо доказательства CTL*-формул A¬[f U g] и A¬G f следует доказывать формулы E¬[f U g] и E¬G f. Проще всего предъявлять пути, замыкающиеся начиная с некоторого состояния в цикл, так как такие пути однозначно задаются конечным числом вершин.

На этом изложение алгоритма завершено.

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

Утверждение.

выполняющий заданную CTL-формулу или являющийся контрпримером к ней, опровергающий ее), представимый в виде объединения «предциклической» и «циклической» частей (рис. 12).

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

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

Отметим, что в работе не рассматривались алгоритмы верификации линейных моделей (PLTL), основанные на применении -автоматов, называемых также автоматами Бюхи (Bchi). Подробнее об автоматах Бюхи и верификации моделей, описанных в логике PLTL, изложено в работах [1, 33–40].

Глава 4. Преобразование сценария для модели Крипке Переходим к последней фазе процесса верификации в автоматном программировании (рис. 3). Ниже будет описано, как представлять путь автомата Мили. Отметим сразу, что на протяжении этой главы предполагается, что модель Крипке была сгенерирована по «редуцированной» схеме, изложенной в разд. 2.4. Остальные схемы, для которых было дано описание, позволяют применять к себе аналогичный интуитивно ясный способ перехода от модели к автомату. Исключение составляют лишь специфические элементы разд. 2.5, в котором описывались нетрадиционные методы моделирования, применяемые для случаев слишком больших автоматов. При использовании этих методов интерпретировать результаты разработчику приходится самому – ему придется проводить анализ путей прямо на модели Крипке, которую он сам (вручную) и построил.

После того, как отработала программа-верификатор, необходимо определить выполнимость формул спецификации на определенных участках автомата. Среди этих участков могут быть состояния, события, выходные воздействия. Будем считать, что недостаточно лишь знать ответ, верна или неверна формула на некотором участке. Требуется, чтобы сценарий, предъявленный программой, был представлен в исходном автомате. Сценарий для любой подформулы спецификации представляет собой бесконечный путь в модели Крипке, иллюстрирующий справедливость или ошибочность данной подформулы. Изображать этот путь следует конечным – вспомним утверждение из разд. 3.4.

Что касается «переноса» пути из модели Крипке в автомат, то данная операция (скажем, для редуцированной схемы) выполняется однозначно.

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

Рассмотрим пример для автомата ARemote. Пусть для состояния выполняется верификация формулы ¬E[¬(Y=6)U(Y=1)], которая, как описано в разд. 2.2, трактуется следующим образом: в состояние 1 нельзя попасть, минуя состояние 6. Эта формула в состоянии 3 не выполняется. Верификатор сгенерировал (кратчайший и единственный в данном случае) контрпример, который на рис. 13,а выделен серым цветом. Это конечный путь, любое продолжение которого удовлетворяет формуле E[¬(Y=6)U(Y=1)].

Этот же путь, но представленный в исходном автомате, можно увидеть на рис. 13,б.

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

На этом процесс верификации автоматных программ завершен.

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

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

Исходя из изложенного выше, можно кратко сформулировать основные достоинства автоматных программ в части их верификации [41]:

класс автоматных программ является наиболее удобным для верификации методом Model checking, так как в этом случае модель программы может быть автоматически построена по спецификации ее поведения, задаваемой в общем случае системой взаимодействующих конечных автоматов, в то время как для программ других классов модель приходится строить структура автоматных программ, в которых функции входных и выходных воздействий почти полностью отделены от логики программ, делает доказательств с использованием пред- и постусловий [42, 43].

С математическим аппаратом, используемым в настоящей работе, на русском языке можно ознакомиться в работе [44].

1. Katoen J.–P. Concepts, Algorithms, and Tools for Model Checking. Lehrstuhl fr Informatik VII, Friedrich-Alexander Universitt Erlangen-Nrnberg. Lecture Notes of the Course (Mechanised Validation of Parallel Systems) (course number 10359). Semester 1998/1999.

2. Clarke E. M., Grumberg O., Peled D. A. Model Checking.

http://mitpress.mit.edu/catalog/item/default.asp?ttype=2&tid= 3. Clarke E. M, Jr. Lectures on Model Checking. Computer Science Department, Carnegie Mellon University, 2005.

4. Соколов В. А., Чалый Д. Ю. Методы исследования поведения транспортных протоколов в условиях интенсивного сетевого трафика. Ярославль:

Ярославский государственный университет, 2004.

http://www.teletraffic.ru/public/pdf/Sokolov_Chalyi_2004.pdf 5. Покозий Е. А. Методы спецификации и верификации параллельных моделей с непрерывным временем. Автореферат диссертации на соискание ученой степени кандидата физико-математических наук. Институт систем информатики Сибирского отделения РАН. Новосибирск, 1999.

6. Джексон Д. Программы проверяют программы //В мире науки. 2006. №10, с.52–57.

7. Вудкок Дж. Первые шаги к решению проблемы верификации программ //Открытые системы. 2006. № 8, с.36–57.

8. Quielle J., Sifakis J. Specification and verification of concurrent systems in CESAR /Proceedings 5-th International Symposium on Programming, LNCS 137, pp. 337–351, 1982.

for branching time logic /Logic of Programs, LNCS 131, pp. 52 – 71, 1981.

10. Pnueli A. The temporal logic of programs /Proceedings 18th IEEE Symposium on Foundations of Computer Science, pp. 46 – 57, 1977.

11. Шалыто А. А. SWITCH-технология. Алгоритмизация и программирование задач логического управления. СПб.: Наука, 1998. http://is.ifmo.ru/books/switch/ 12. Шалыто А. А. Логическое управление. Методы аппаратной и программной реализации СПб.: Наука, 2000. http://is.ifmo.ru/books/log_upr/ 13. Кузьмин Е. В., Соколов В. А. Моделирование, спецификация и верификация «автоматных» программ. Ярославский государственный университет им. П. Г. Демидова, 2006.

14. Кормен Т., Лейзерсон Ч., Ривест Р, Штайн К. Алгоритмы: построение и анализ, 2-е издание. Перевод с английского – М.: Издательский дом «Вильямс», 2005.

15. Вельдер С. Э., Бедный Ю. Д. Универсальный инфракрасный пульт для бытовой техники. СПбГУ ИТМО. Курсовая работа. 2005. http://is.ifmo.ru/projects/irrc/ 16. Kripke S. A. Semantical considerations on modal logic //Acta Philosophica Fennica 16: 83 – 94, 1963.

17. Clarke E. M., Draghicescu I. A. Expressibility Results for Linear-Time and Branching-Time Logics. Computer Science Department. Carnegie Mellon University, 2005.

18. Finite state machine. http://en.wikipedia.org/wiki/Finite_state_machine 19. Mealy machine. http://en.wikipedia.org/wiki/Mealy_machine 20. Moore machine. http://en.wikipedia.org/wiki/Moore_machine 21. Sebastiani R. Introduction to Formal Methods, 2005–2006.

http://dit.unitn.it/~rseba/DIDATTICA/fm2005/02_transition_systems.pdf 22. Margaria T. Model Structures. Service Engineering – SS 06.

https://www.cs.uni-potsdam.de/sse/teaching/ss06/sveg/ps/2-ServEng-Model-Structures.pdf 23. Roux C., Encrenaz E. CTL May Be Ambiguous when Model Checking Moore Machines. UPMC LIP6 ASIM, CHARME, 2003.

http://sed.free.fr/cr/charme2003-presentation.pdf 24. Hull R. Web Services Composition: A Story of Models, Automata and Logics.

Bell Labs, Lucent Technologies, 2004. http://edbtss04.dia.uniroma3.it/Hull.pdf 25. Сайт проекта UniMod. http://unimod.sf.net 26. Сайт eVelopers Corporation. http://www.evelopers.com 27. Шопырин Д. Г., Шалыто А. А. Синхронное программирование //Информационно-управляющие системы. 2004. № 3, с. 35–42. http://is.ifmo.ru/works/sync_prog/ 28. Von Hanxleden R. Modeling/Distributed RT Systems – Lecture 03, 2005.

http://www.informatik.uni-kiel.de/inf/von-Hanxleden/teaching/ss05/v-rt2/lectures/lecture03handout4.pdf 29. Berry G. The Esterel v5 Language Primer, April, 1999.

ftp://ftp-sop.inria.fr/meije/esterel/papers/primer.pdf 30. Potop D., de Simone R. Optimizations for Faster Execution of Esterel Programs, 31. Edwards S. A. The Synchronous Language Esterel. Columbia University, Department of Computer Science, 2002.

http://www1.cs.columbia.edu/~sedwards/classes/2002/w4995-02/esterel.pdf Лекция №3 курса «Современные задачи теоретической информатики».

СПбГУ ИТМО, 2005. http://logic.pdmi.ras.ru/~yura/modern/03modernnote.pdf 33. Лифшиц Ю. Символьная верификация программ. Лекция №4 курса «Современные задачи теоретической информатики». СПбГУ ИТМО, 2005.

http://logic.pdmi.ras.ru/~yura/modern/04modernnote.pdf Ярославский государственный университет. 2004.

http://www.ict.nsc.ru/ws/dicr/7629/rep7629.pdf 35. Puppis G. Automata for Branching and Layered Temporal Structures. Thesis.

Universit degli Studi di Udine, Dipartimento di Matematica e Informatica.

Dottorato di Ricerca in Informatica, 2006.

36. Mller-Olm M., Schmidt D., Steffen B. Model Checking: A Tutorial Introduction, 1999.

http://eti.informatik.uni-dortmund.de/imperia/md/content/publikationen/muss99-it.pdf 37. Lerda F. LTL to Bchi Automata. Carnegie, Mellon University, 2005.

38. Lerda F. LTL Model Checking. Carnegie, Mellon University, 2005.

39. Lerda F. SPIN, An explicit state model checker. Carnegie, Mellon University, 40. Biere A., Cimatti A., Clarke E., Zhu Y. Symbolic model checking without BDDs.

School of Computer Science, Carnegie Mellon University, 1999.

41. Switch-technology. http://en.wikipedia.org/wiki/Switch-technology 42. Дейкстра Э. Заметки по структурному программированию /Дал У., Дейкстра Э., Хоор К. Структурное программирование. М.: Мир, 1975.

43. Мейер Б. Объектно-ориентированное конструирование программных систем.

М.: Русская редакция. 2005.

44. Миронов А. М. Математическая теория программных систем.

http://intsys.msu.ru/study/mironov/mthprogsys.pdf