Верификация параметризованных моделей распределенных систем тема диссертации и автореферата по ВАК РФ 05.13.11, кандидат физико-математических наук Коннов, Игорь Владимирович

• Коннов, Игорь Владимирович
• кандидат физико-математических наук
• 2008

Оглавление диссертации кандидат физико-математических наук Коннов, Игорь Владимирович

Введение

Проверка корректности программ.

Цель диссертационной работы.

Введение диссертации (часть автореферата) на тему «Верификация параметризованных моделей распределенных систем»

Основные результаты.16

Структура работы.16

Глава 1. Постановка задачи.19

1.1. Модели распределённых систем .19

1.2. Задача верификации моделей распределённых систем .22

1.3. Задача верификации параметризованных моделей распределённых систем .22

Глава 2. Обзор литературы .25

2.1. Аналитические методы редукции^ . . • ---------------29 -2.2. Методы абстракции.31

2.3. Символьные методы.35

2.4. Методы, основанные на поиске инварианта.38

2.5. Выводы, выбор метода и декомпозиция задачи .43

Глава 3. Основные определения .45

3.1. Размеченные системы переходов.45

3.2. Асинхронная параллельная композиция .49

3.3. Описание топологии распределённых систем с помощью сетевых грамматик.50

3.4. Темпоральные логики.53

3.5. Конечные и бесконечные блоки .56

3.6. Выводы.58

Глава 4. Новые отношения симуляции .59

4.1. Блочная симуляция .60

4.2. Квазиблочная симуляция.66

4.3. Полублочная симуляция .75

4.4. Выводы.95

Глава 5. Метод сетевых инвариантов для случая асинхронных параметризованных систем .96

5.1. Метод сетевых инвариантов с использованием квазиблочной и блочной симуляций .97

5.2. Алгоритм построения полублочной симуляции.100

5.3. Оценки сложности.106

5.4. Выводы.110

- Глава-6— Практическая-реализация и проверка протокола резервирования ресурсов .111

6.1. Архитектура системы CheAPS.Ill

6.2. Протокол резервирования ресурсов .114

6.3. Предыдущие работы по верификации протокола .117

6.4. Параметризованная модель.117

6.5. Верификация параметризованной модели.120

6.6. Проверка свойств модели протокола .125

6.7. Выводы.126

Заключение .127

Литература

129

Приложение А. Некоторые существующие отношения на LTS 143

А.1. Трассовая эквивалентность.143

А.2. Бисимуляционная эквивалентность (бисимуляция) .145

А.З. Прореженная бисимуляция.147

А.4. Ветвящаяся бисимуляция.^.148

А.5. Блочная бисимуляция.150

А.6. Симуляция .151

А.7. Прореженная симуляция .155

А.8. Выводы.156

Приложение Б. Детали реализации экспериментальной системы CheAPS .157

Б.1. Описание алгоритма построения полублочной симуляции . . . 157

Б.2. Язык TinyPromela .180

Б.З. Подсистема порождения моделей по сетевой грамматике . 181

--------------Б:4г Подсистема построения полублочной симуляции.184

Б.5. Подсистема поиска контрпримеров .197

Б.6. Выводы.198

Список иллюстраций

3.1 Диграммы LTS процессов типа Root, Inner, Leaf.48

4.1 Пример LTS, находящихся в отношении блочной симуляции . . 62

4.2 Полублочная симуляция.76

4.3 Взаимосвязь между путями в Similar Siblings . .77

4.4 Диаграмма путей пункта (2а).84

4.5 Диаграмма путей пункта (26) .85

4.6 Критерий полублочной симуляции.87

6.1 Архитектура системы проверки параметризованных систем . . . 113

6.2 Время построения полублочной симуляции с различными оптимизациями .123

6.3 Потребление памяти при построении полублочной симуляции с различными оптимизациями .124

А.1 Модели Mi и М2 находятся в отношении бисимуляции.146

-------------А-.2- LTS Mf и М.2 находятся в отношении симуляции.152

А.З Отсутствие симуляции для LTS, отличающихся уровнем абстракции .153

А.4 Процессы р и q и два экземпляра параметризованного семейства 154

Б.1 Сгенерированный граф модели из пяти процессов.183

Б.2 Архитектура подсистемы проверки симуляции.185

Б.З Признаки нестабильности пар состояний .196

Введение

Лев Николаевич (Королёв) оказался прав. Программ без ошибок не бывает.

Замечание С.А. Лебедева об ошибке в программе.

Проверка корректности программ

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

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

Как заметил Дейкстра [100]: «Тестирование программ может использоваться для демонстрации наличия ошибок, но оно никогда не покажет их отсутствие». Методы верификации направлены на доказательство утверждений о свойствах поведения программы или результатов её работы. Этот подход к проверке правильности программ был впервые предложен в работах А.А. Ляпунова [103, 104], Т. Хоара [40], Э. Дейкстры [100], Пратта [81] и Флойда [25].

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

Методы верификации программ, использующие теоретико-доказательный подход, основываются на средствах автоматического доказательства теорем (САДТ, theorem prover, «прувер») [72, 73, 83, 90]. Описание программы представляется в виде множества логических утверждений. Спецификация программы также представляется в виде утверждения. САДТ строит доказательство выполнимости спецификации, исходя из утверждений, описывающих проверяемую программу.

К сожалению, при использовании САДТ в процессе построения доказательства может потребоваться участие эксперта. Одной из наиболее трудных задач, возникающих при верификации программ с помощью САДТ, является задача порождения инварианта цикла [40]. Инвариант цикла требуется при проверке выводимости постусловия функции из предусловия. Несмотря на значительный прогресс в этой области [51, 53], верификация большинства программ всё ещё требует привлечения эксперта.

Верификация программы с использованием логических утверждений, построенных непосредственно на основании исходных кодов программы, увеличивает сложность процесса доказательства. В тоже время некоторые фрагменты кода могут быть несущественными для проверки выделенных свойств программы. Свойства программы могут быть проверены на модели программы, более простой, чем исходная программа. Группа методов, основанных на верификации моделей (Model Checking, МС) [102], использует компромиссный подход между полноценной верификацией программы и тестированием, использующим формальную проверку свойств.

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

Первые примеры успешного применения МС относятся к проверке моделей аппаратных схем. В дальнейшем методы МС успешно применялись для проверки моделей сетевых протоколов, распределённых алгоритмов. В последние годы методы МС стали применяться и для верификации последовательных программ. В 2007 году за изобретение первых алгоритмов МС основоположники группы методов МС Э. Кларк, А. Эмерсон и Ж. Сифакис получили премию Тьюринга.

Применение методов МС ограничивает целый ряд недостатков, присущих этой группе методов:

• сложность построения адекватной модели,

• эффект «комбинаторного взрыва»,

• требование конечности модели.

Применение группы методов МС связано с нетривиальным вопросом построения корректной и адекватной модели. Модель строится для проверки соответствия исходной программы заданному набору спецификаций, поэтому модель должна быть адекватной, т.е. отражать все свойства исходной программы, необходимые для проверки спецификаций. Также модель должна быть корректной для выбранного набора свойств, т.е. поведение модели должно соответствовать поведению исходной программы с учётом выбранных свойств. От выбора свойств исходной программы, переносимых на модель, зависит адекватность модели^ проверяемому набору спецификаций и— -практическая применимость группы методов МС.

Если корректность модели можно гарантировать с помощью ограничений на методы построения модели по программе, то адекватность может быть проверена только после того, как проведена верификация модели. Для построения корректной модели могут использоваться методы автоматического порождения моделей (Model Extraction [45]) по заданной программе, а автоматическое построение адекватной модели достигается за счёт комбинирования методов булевой абстракции с итеративной верификацией моделей [12,14, 87]. Такой подход к построению моделей получил название Counter Example Guided Abstraction Refinement. В случае неудачной проверки построенной модели проводится уточнение модели с помощью САДТ. Стоит заметить, что в данном случае комбинируются средства МС и САДТ. Соответственно, гарантия полностью автоматической проверки моделей, вообще говоря, исчезает, так как не во всех случаях САДТ способны выдать доказательство запрашиваемого утверждения.

Эффект «комбинаторного взрыва» связан с экспоненциальным ростом пространства состояний при линейном росте числа взаимодействующих процессов. Последствиями экспоненциального роста пространства состояний становятся высокие требования к объему памяти, используемой верификатором моделей, и долгое время проверки модели. Для сжатия проверяемого множества состояний используются символьные способы представления моделей, например, двоичные разрешающие диаграммы (Binary Decision Diagrams, BDD) [19]. В символьном представлении модели выражаются с помощью BDD, которые реализуют функции алгебры логики. При поиске в пространстве состояний вместо перебора состояний используются операции над функциями. Алгоритмы верификации моделей с помощью BDD могут быть значительно эффективнее явного перебора состояний в том случае, когда BDD системы переходов модели и промежуточных результатов остаются компактными [65]. Для моделей аппаратных схем представление модели в виде BDD даёт хороший коэффициент сжатия по отношению к явному представлению множеств. Модели распределённых программ сжимаются несколько хуже, так как в распределённых программах используется асинхронное взаимодействие.

Для борьбы с «комбинаторным взрывом» при верификации моделей программ используются методы редукции частичных порядков [43, 76, 77]. В этих методах проверяется достаточное подмножество множества всех трасс. Такое подмножество вычисляется на основании зависимостей между переходами процессов модели. Типы проверяемых зависимостей выявляются эмпирически. Удачный выбор правил редукции может существенно ускорить алгоритм верификации модели [43].

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

При верификации моделей с бесконечным числом состояний (Infinite State-Space Model Checking) в описании модели могут присутствовать переменные с неограниченными типами данных, а порождаемая по описанию система переходов обладает бесконечным множеством состояний. Для решения этой задачи используются комбинации символьных методов верификации моделей и методов доказательства теорем [4, 18, 24, 30, 32, 36, 48, 63, 66, 69, 80, 85, 89].

Задача верификации параметризованных моделей (Parameterized Model Checking, PMC) возникает при рассмотрении моделей распределённых систем, в которых число однотипных взаимодействующих процессов зависит от начальной конфигурации системы и может быть сколь угодно большим. Как известно, увеличение числа вычислителей не всегда приводит к линейному росту производительности распределённой системы. Аналогично, выводы о выполнимости спецификации, полученные для конфигурации с одним числом процессов, нельзя переносить на конфигурации с другим числом процессов, не приводя дополнительной аргументации. Решение задачи РМС позволяет убедиться в выполнимости проверяемых спецификаций при масштабировании распределённой программы, т.е. при росте числа взаимодействующих процессов.

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

В задаче РМС рассматриваются распределённые системы взаимодействующих процессов. В этих системах присутствует фиксированное число статических процессов и неограниченное число однотипных процессов. Так как число однотипных процессов не ограничено, то по распределённой системе может быть построено бесконечное семейство моделей. Каждая модель соответствует конфигурации системы с фиксированным числом процессов. Для проверки свойств распределённой системы необходимо проверить спецификацию на всех моделях бесконечного семейства. Способы решения задачи для некоторых случаев параметризованных моделей приведены в работах [2, 711, 15, 17, 20-23, 28, 47, 49, 54-59, 61, 62, 64, 68, 71, 85, 86, 88, 89, 92, 93, 95, 97]. В последующих разделах будет проведён краткий анализ этих методов. Именно задаче верификации параметризованных моделей распределённых систем посвящена настоящая диссертационная работа.

Цель диссертационной работы

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

При этом предъявляются следующие требования к решению:

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

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

Актуальность работы

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

• распределённые алгоритмы [60, 91]: волновые алгоритмы, распределения ресурсов, взаимного исключения доступа к критической секции, избрания лидера (leader election), обнаружения завершения (termination detection), согласованного принятия транзакции (distributed commit);

• сетевые протоколы [109]: кольцо с маркером, протоколы маршрутизации, протоколы обеспечения качества сервиса, широковещательные протоколы;

• аппаратные схемы: аппаратные схемы управления доступом к шине при различном числе клиентских устройств, протоколы обеспечения когерентности кэшей [38].

В дальнейшем под словами «распределённый алгоритм» мы будем понимать как системы из первого, так и из второго пункта.

Довольно часто при построении модели распределённой системы, которая может потенциально содержать любое количество однотипных процессов, ограничиваются моделью с небольшим, фиксированным числом процессов. При этом предполагается, что свойства, проверенные на модели с фиксированным числом процессов, автоматически масштабируются для моделей с большим числом процессов. Однако этот приём не является вполне корректным: известны примеры, когда спецификация была верна на модели с одним числом процессов и нарушалась при изменении числа процессов [102, с- 161], [7].

Это означает, что для верификации параметризованных моделей программ недостаточно проверить спецификацию на нескольких моделях с фиксированным числом процессов: необходимо обоснование масштабируемости проверенной спецификации на остальные модели. Так как число процессов в моделях не ограничено, то спецификация должна быть проверена на бес конечном семействе моделей с конечным числом состояний. В работе [1] показано, что в общем случае задача РМС сводится к задаче останова машины Тьюринга и, следовательно, алгоритмически неразрешима.

Тем не менее, для некоторых практически интересных классов параметризованных моделей задача РМС может быть решена. Так, показана разрешимость задачи для однонаправленных колец с маркером одного типа [20], колец с произвольным типом маркера и дополнительными ограничениями на LTS процесса [23, 93], симметричных систем с глобальными предусловиями переходов [21, 24], широковещательных систем [21, 22, 61], систем с произвольной топологией и одним маркером [95]. Предложены различные полуразрешающие процедуры: подходы, основанные на поиске инвариантов [911, 52, 55, 64, 86, 97]; подходы, основанные на проверке достижимых состояний регулярных моделей [2, 30, 59, 88]; символьные методы верификации [4, 80, 85]. Указаны способы абстракции [2, 36, 47, 50, 57, 61, 95] для определённых классов систем.

Как будет показано в обзоре, наиболее перспективными методами, настраиваемыми на различные виды топологии параметризованных систем, являются методы, основанные на поиске инвариантов, и символьные методы. Символьные методы верификации параметризованных систем могут потребовать участия эксперта для переработки модели и указания дополнительных подсказок. Примечательно, что примеры успешного применения метода, основанного на поиске инвариантов, относятся к классам распределённых систем синхронно-взаимодействующих процессов [9-11, 52, 55, 97], хотя метод инвариантов использовался и для систем асинхронно-взаимодействующих процессов в работах [11, 64, 86].

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

Таким образом, задача верификации параметризованных моделей распределённых систем актуальна. Однако при разработке таких методов и средств желательно сохранить основное преимущество метода МС — свойство автоматической верификации модели. Необходимо, чтобы для верификации параметризованной модели не требовалась существенная перестройка модели, использованной при верификации средствами МС, или участие эксперта.

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

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

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

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

Структура работы

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

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

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

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

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

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

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

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

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

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

Заключение диссертации по теме «Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей», Коннов, Игорь Владимирович

6.7. Выводы

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

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

Заключение

В диссертационной работе получены следующие основные результаты:

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

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

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

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

Методы инвариантов, за исключением [7] и [102, стр. 307], проверялись на простых примерах: взаимного исключения процессов в критической секции в кольце и звёздообразной топологии, распространении сообщения в дереве и т.д. В настоящей работе с помощью предлагаемого метода проверяется параметризованная модель протокола резервирования ресурсов (RSVP). Число состояний проверяемых моделей параметризованного семейства варьируется от нескольких десятков тысяч до нескольких миллионов.

Предложенные в данной работе ослабленные отношения симуляции могут быть применены не только для решения задачи верификации параметризованных моделей распределённых систем, но и для обоснования модульного подхода к верификации моделей [35], редукции частичных порядков [43, 76, 77], т.е. там, где используется отношение симуляции.

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

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

Список литературы диссертационного исследования кандидат физико-математических наук Коннов, Игорь Владимирович, 2008 год

1. Apt К., Kozen D. Limits for automatic verification of finite-state concurrent systems // 1.formation Processing Letter. — 1986. — Vol. 15. — Pp. 307309.

2. Browne M. C., Clarke E. M., Grilmberg O. Characterizing finite kripke structures in propositional temporal logic // Theor. Comput. Sci. — 1988. — Vol. 59, no. 1-2,- Pp. 115-131.

3. Bultan Т., Gerber R., Pugh W. Symbolic model checking of infinite state systems using presburger arithmetic // CAV '97: Proceedings of the 9th International Conference on Computer Aided Verification. — London, UK: Springer-Verlag, 1997.- Pp. 400-411.

4. Bulychev P., Konnov I., Zakharov V. Computing (bi)simulation relations preserving ctlx logic for ordinary and fair kripke structures // Труды Института системного программирования РАН. — Vol. 12. — 2007. — Pp. 59-76.

5. Calder M., Miller A. Five ways to use induction and symmetry in the verification of networks of processes by model-checking // Automated Verification of Critical Systems (AvoCS 2002). — 2002. — Pp. 29-42.

6. Calder M., Miller A. Using spin to analyse the tree identification phase of the ieee 1394 high performance serial bus (firewire) protocol // Formal Aspects of Computing. 2003. - Pp. 247-266.

7. Calder M., Miller A. Detecting feature interactions: how many components do we need? // Objects, Agents and Features. — 2004. — Vol. 2975. — Pp. 4566.

8. Clarke E., Grumberg 0., Browne M. Reasoning about networks with many identical finite-state processes // PODC '86: Proceedings of the fifth annual ACM symposium on Principles of distributed computing. — New York, NY, USA: ACM, 1986. Pp. 240-248.

9. Clarke E., Grumberg O., Jha S. Verifying parameterized networks using abstraction and regular languages // 6-th International Conference on Concurrency Theory. — 1995. — Pp. 395-407.

10. Clarke E., Grumberg O., Jha S. Verifying parameterized networks // ACM Transactions on Programming Languages and Systems. — 1997. — Vol. 19, no. 5. Pp. 726-750.

11. Cleaveland R., Sokolsky O. Equivalence and preorder checking for finite-state systems // Handbook of Process Algebra / Ed. by J. Bergstra, A. Ponse, S. Smolka. North-Holland, 2001. — Pp. 391-424.

12. Counterexample-guided abstraction refinement / Б. Clarke, O. Grumberg, S. Jha et al. // Computer Aided Verification. 2000. - Pp. 154-169.

13. Creese S., Reed J. Verifying end-to-end protocols using induction with csp/f-dr // IPPS/SPDP Workshop. 1999.- Pp. 1243-1257.

14. De Nicola R., Vaandrager F. Three logics for branching bisimulation // ,7. ACM. 1995. - Vol. 42, no. 2. - Pp. 458-487.

15. Delzanno G. Constraint-based verification of parameterized cache coherence protocols // Form. Methods Syst. Des. — 2003. — Vol. 23, no. 3. — Pp. 257301.

16. Drechsler R., Becker B. Binary Decision Diagrams — Theory andlmple-mentation. — Kluwer Academic Publishers, 1998.

17. Emerson E., Namjoshi K. Reasoning about rings // Proceedings of 22th ACM Conf. on Principles of Programming Languages. — 1995.— Pp. 8594.

18. Emerson E. A., Kahlon V. Exact and efficient verification of parameterized cache coherence protocols // 12th IFIP Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME). — LAquila, Italy: 2003. Pp. 247-262.

19. Emerson E. A., Kahlon V. Model checking guarded protocols // LICS.— IEEE Computer Society, 2003. — Pp. 361-370.

20. Emerson E. A., Kahlon V. Parameterized model checking of ring-based message passing systems // Computer Science Logic. — Vol. 3210/2004 of LNCS. 2004. - Pp. 325-339.

21. Emerson E. A., Namjoshi K. S. On model checking for non-deterministic infinite-state systems // LICS '98: Proceedings of the 13th Annual IEEE Symposium on Logic in Computer Science. — Washington, DC, USA: IEEE Computer Society, 1998. P. 70.

22. Floyd R. Assigning meanings to programs // Proc. AMS Symp. on Applied Mathematics. — Vol. 19.— Providence: Amer. Mathematical Soc., 1967.— Pp. 19-31.

23. Fokkink W. Introduction to Process Algebra / Ed. by W. Brauer, G. Rozen-berg, A. Salomaa. — Secaucus, NJ, USA: Springer-Verlag New York, Inc., 2000.

24. Fossaceca J., Sandoz J., Winterbottom P. The pathstar access server: facilitating carrier-scale packet telephony // Bell Labs Technical Journal. — 1998. Vol. 3, no. 4. - Pp. 86-102.

25. German S. M., Sistla A. P. Reasoning about systems with many processes // J. ACM. 1992. - Vol. 39, no. 3. - Pp. 675-735.

26. Ghemawat S., Gobioff H., Leung S.-T. The google file system // SOSP '03: Proceedings of the nineteenth ACM symposium on Operating systems principles. New York, NY, USA: ACM, 2003. - Pp. 29-43.

27. Gregoire J. State space compression in spin with gets // Proc. Second Spin Workshop. Vol. 32 of DIMACS. - 1996. - Pp. 90-108.

28. Gribomont E. P., Zenner G. Automated verification of szymanski's algorithm // TACAS '98: Proceedings of the 4th International Conference on Tools and Algorithms for Construction and Analysis of Systems. — London, UK: Springer-Verlag, 1998. Pp. 424-438.

29. Griffioen D., Vaandrager F. Normed simulations // Computer-Aided Verification, CAV '98 / Ed. by A. J. Ни, M. Y. Vardi. Vol. 1427. - Vancouver, Canada: SV, 1998.- Pp. 332-344.

30. Grumberg 0., Long D. E. Model checking and modular verification // ACM Trans. Program. Lang. Syst.— 1994. — Vol. 16, no. 3. — Pp. 843-871.

31. Gyuris V., Sistla A. P. On-the-fly model checking under fairness that exploits symmetry // CAV '97: Proceedings of the 9th International Conference on Computer Aided Verification. — London, UK: Springer-Verlag, 1997.- Pp. 232-243.

32. Hennessy J. L., Patterson D. A. Computer architecture: a quantitative approach. — San Francisco, CA, USA: Morgan Kaufmann Publishers Inc., 2002.

33. Hennessy M., Milner R. Algebraic laws for nondeterminism and concurrency // J. ACM. — 1985. — Vol. 32, no. 1.- Pp. 137-161.

34. Hoare C. An axiomatic basis for computer programming // С ACM.— 1969.- Vol. 12, no. 10.- Pp. 576-585.

35. Hoare T. The verifying compiler: A grand challenge for computing research // J. ACM. 2003. - Vol. 50, no. 1. - Pp. 63-69.

36. Holzmann G. Design And Validation Of Computer Protocols. — Prentice-Hall, 1991.-512 pp.

37. Holzmann G., Peled D. An improvement in formal verification // FORTE 1994 Conference. 1994. - Pp. 197 - 211.

38. Holzmann G., Puri A. A minimized automaton representation of reachable states // Software Tools for Technology Transfer, Vol. 3, No. 1. — 1998.

39. Holzmann G., Smith M. Software model checking: Extracting verification models from source code // Formal Methods for Protocol Engineering and Distributed Systems. — Kluwer Academic Publ., 1999. — Pp. 481-497.

40. Holzmann G. J. The SPIN Model Checker : Primer and Reference Manual. — Addison-Wesley Professional, 2003. — September. — 596 pp.

41. Ip С. N.} Dill D. L. Verifying systems with replicated components in mur-phi // Form. Methods Syst. Des. 1997. - Vol 14, no. 3.- Pp. 273-310.

42. Kahlon V. Model checking: beyond the finite: Ph.D. thesis / The University of Texas at Austin. — 2004. — Supervisor-Ernest Allen Emerson, II.

43. Kesten Y., Pnueli A. Control and data abstraction: The cornerstones of practical formal verification // International Journal on Software Tools for Technology Transfer. 2000. — Vol. 2, no. 4. - Pp. 328-342.

44. Lesens D. Invariants of parameterized binary tree networks as greatest fixpoints // Algebraic Methodology and Software Technology. — 1997. — Pp. 337-350.

45. Lesens D., Saidi H. Abstraction of parameterized networks. — 1997.

46. Lesens D., Saidi H. Automatic verification of parameterized networks of processes by abstraction // 2nd International Workshop on the Verification of Infinite State Systems (INFINITY'97). 1997. - Pp. 268-278.

47. Lynch N. A. Distributed Algorithms. — San Francisco, CA, USA: Morgan Kaufmann Publishers Inc., 1996.

48. Maidl M. A unifying model checking approach for safety properties of parameterized systems // CAV '01: Proceedings of the 13th International Conference on Computer Aided Verification. — London, UK: Springer-Verlag, 2001.- Pp. 311-323.

49. Manna Z., Pnueli A. An exercise in the verification of multi-process programs // Beauty is our business: a birthday salute to Edsger W. Dijkstra. — 1990.- Pp. 289-301.

50. Manolios P. Mechanical Verification of Reactive Systems: Ph.D. thesis / University of Texas at Austin. — 2001.

51. Marelly R., Grumberg 0. Gormel — grammar oriented model checker // Tech. Rep. 697. — Haifa, Israel: The Technion, 1991.

52. McMillan K. Symbolic Model Checking. — Kluwer Academic Publishers, 1993.

53. Meyer A., Stockmeyer L. The equivalence problem for regular expressions with squaring requires exponential space"//' 13th IEEE Sympron Switching -and Automata Theory. — 1972. — Pp. 125-129.

54. Namjoshi К. S. A simple characterization of stuttering bisimulation // Proceedings of the 17th Conference on Foundations of Software Technology and Theoretical Computer Science. — London, UK: Springer-Verlag, 1997. Pp. 284-296.

55. Nilsson M. Structural Symmetry and Model Checking: Ph.D. thesis / Uppsala University, Uppsala, Sweden. — 2005.— 157 pp.

56. Nipkow Т., Paulson L. C., Wenzel M. Isabelle/HOL — A Proof Assistant for Higher-Order Logic. Springer, 2002. - Vol. 2283 of LNCS.

57. Page R., Tarjan R. Three partition refinement algorithms // SI AM Journal on Computing. — 1987. — Vol. 6, no. 16. — Pp. 973-989.

58. Park D. Concurrency and automata on infinite sequences // Proceedings of the 5th Gl-Conference on Theoretical Computer Science. — London, UK: Springer-Verlag, 1981.-Pp. 167-183.

59. A partial order approach to branching time logic model checking / R. Gerth, R. Kuiper, D. Peled, W. Penczek // Inf. Comput.- 1999,- Vol. 150, no. 2,- Pp. 132-152.

60. Partial order reductions preserving simulations / W. Penczek, M. Szreter, R. Gerth, R. Kuiper // Proc. of Concurrency, Specification and Programming (CSP'99).-Warsaw: 1999.-Pp. 153-172.

61. Peled D. Partial order reduction: linear and branching temporal logics and process algebras // POMIV '96: Proceedings of the DIMACS workshop on Partial order methods in verification. — New York, NY, USA: AMS Press, Inc., 1997.-Pp. 233-257.

62. Peled D. A. Software Reliability Methods / Ed. by D. Gries, F. B. Schneider. — Secaucus, NJ, USA: Springer-Verlag New York, Inc., 2001.

63. Pratt V. Semantical considerations on floyd-hoare logic // Proc. 17th Ann. IEEE Symp. on Foundations of Computer Science. — 1976. — Pp. 109-121.

64. Braden R., Zhang L., Berson S. et al. Resource reservation protocol (rsvp). — 1997. http://tools.ietf.org/html/rfc2205.

65. Riazanov A., Voronkov A. The design and implementation of vampire // Al Commun. 2002. - Vol. 15, no. 2. - Pp. 91-110.

66. Rudd Т., Orr M., Bicking I. Cheetah: The python-powered template engine // 10th International Python Conference.— 2002. http://www. python.org/workshops/2002-02/papers/08/index.htm.

67. Shahar E. Tools and Techniques for Verifying Parameterized Systems: Ph.D. thesis / Weizmann Institute of Science, Israel. — 2001. — 120 pp.

68. Shtadler Z., Grumberg O. Network grammars, communication behaviors and automatic verification // Proceedings of the International Workshopon Automatic Verification Methods for Finite State Systems. — London, UK: Springer-Verlag, 1990. Pp. 151-165.

69. Software verification with blast / T. A. Henzinger, R. Jhala, R. Majumdar, G. Sutre // 10th SPIN Workshop on Model Checking Software (SPIN).-LNCS 2648. Springer-Verlag, 2003. - Pp. 235-239.

70. A survey of regular model checking / P. Abdulla, B. Jonsson, M. Nils-son, M. Saksena // Proc. 15th Int. Conf. on Concurrency Theory.— Vol. 3170/2004 of Lecture Notes in Computer Science. — 2004. — Pp. 35-48.

71. Symbolic model checking with rich assertional languages / Y. Kesten, O. Maler, M. Marcus et al. // CAV '97: Proceedings of the 9th International Conference on Computer Aided Verification. — London, UK: Springer-Verlag, 1997. Pp. 424-435.

72. System description: Spass version 3.0 / C. Weidenbach, R. Schmidt, T. Hillenbrand et al. // Automated Deduction CADE-21 : 21st International Conference on Automated Deduction. — 2007. — Pp. 514-520.

73. Tel G. Introduction to Distributed Algorithms. — Cambridge University Press, 2000.

74. Thistle J., Nazari S. Analysis of arbitrarily large networks of discrete-event systems // 44th IEEE Conference on Decision and Control (CDC'05).— Seville, Spain: 2005.

75. Thistle J., Nazari S. Structural conditions for model-checking of parameterized networks // 7th International Conference on Application of Concurrency to System Design (ACSD'07).— Bratislava, Slovak Republic: 2007.

76. Van Glabbeek R. J., Peter Weijland W. Branching time and abstraction in bisimulation semantics // J. ACM. — 1996. — Vol. 43, no. 3. — Pp. 555-600.

77. Verification by network decomposition / E. Clarke, M. Talupur, T. Touili, H. Veith // CONCUR 2004. Vol. 3170. - 2004. - Pp. 276-291.

78. Villapol M. Modelling and Analysis of the Resource Reservation Protocol using Coloured Petri Nets: Phd thesis / Institute for Telecommunications Research and Computer Systems Engineering Centre, University of South Australia. 2003. — 362 pp.

79. Ахо А., Хопкрофт Д., Ульман Д. Построение и анализ вычислительных алгоритмов. — М.: Мир, 1979.

80. Царьков Д. Верификация распределённых программ методом проверки на модели: Дис. канд. физ.-мат. наук: 05.13.11 / Московский Государственный Университет им. М.В. Ломоносова. — 2002.— 185 с.

81. Дейкстра Э. Дисциплина программирования. — М.: Мир, 1978.

82. Дейт К. Введение в системы баз данных. — М.: Вильяме, 2006. — 1328 с.

83. Кларк Э., Грамберг О., Пелед Д. Верификация моделей программ: Model Checking. — М.: Издательство Московского центра непрерывного математического образования, 2002.

84. Ляпунов А. О логических схемах программ // Проблемы кибернетики. Т. 1. - М.: Физматгиз, 1958. - С. 46-74.

85. Ляпунов А., Янов Ю. О логических схемах программ // Труды конференции «Пути развития советского математического машиностроения и приборостроения». — Т. 3. — М.: 1956. — С. 5-8.

86. Никифоров Б. Электроника на службе безопасности движения // Современные технологии автоматизации. — 2006. — JN® 1. — С. 40-45.

87. Смелянский Р. Математическая модель функционирования распределённых ВС // Вестник МГУ. 1990. - Т. 15, № 3.

88. Страуструп Б. Язык программирования С++. — М.: Бином, 1999.— С. 991.

89. Таненбаум Э. Компьютерные сети.— СПб.: Питер, 2007.

90. Таненбаум Э., ван Стеен М. Распределённые системы. Принципы и парадигмы. — СПб.: Питер, 2003.