Верификация параметризованных моделей распределенных систем

• Автор: Коннов, Игорь Владимирович
• Шифр специальности: 05.13.11
• Научная степень: Кандидатская
• Год защиты: 2008
• Место защиты: Москва
• Количество страниц: 198 с. : ил.

Оглавление
Введение .

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

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

, 1

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

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

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

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

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

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

1.3. Задача верификации параметризованных моделей распределнных систем .
Глава 2. Обзор литературы
2.1. Аналитические методы редукции . . .
2.2. Методы абстракции.
2.3. Символьные методы.
2.4. Методы, основанные на поиске инварианта.
2.5. Выводы, выбор мегода и декомпозиция задачи .
Глава 3. Основные определения
3.1. Размеченные системы переходов.
3.2. Асинхронная параллельная композиция
3.3. Описание топологии распределнных систем с помощью сетевых грамматик
3.4. Темпоральные логики.
3.5. Конечные и бесконечные блоки
3.6. Выводы.
Глава 4. Новые отношения симуляции .
4.1. Блочная симуляция .
4.2. Квазиблочная симуляция.
4.3. Полублочная симуляция .
4.4. Выводы.
Глава 5. Метод сетевых инвариантов для случая асинхронных параметризованных систем .
5.1. Метод сетевых инвариантов с использованием квазиблочной и блочной симуляций .
5.2. Алгоритм построения полублочной симуляции.
5.3. Оценки сложности
5.4. Выводы
Глава 6. Практическая реализация и проверка протокола резервирования ресурсов .
6.1. Архитектура системы СЬеАРБ
6.2. Протокол резервирования ресурсов .
6.3. Предыдущие работы по верификации протокола .
6.4. Параметризованная модель
6.5. Верификация параметризованной модели
6.6. Проверка свойств модели протокола
6.7. Выводы
Заключение
Литература


Указаны способы абстракции [2, , , , , , ] для определённых классов систем. Как будет показано в обзоре, наиболее перспективными методами, настраиваемыми на различные виды топологии параметризованных систем, являются методы, основанные на поиске инвариантов, и символьные методы. Символьные методы верификации параметризованных систем могут потребовать участия эксперта для переработки модели и указания дополнительных подсказок. Примечательно, что примеры успешного применения метода, основанного на поиске инвариантов, относятся к классам распределенных систем синхронно-взаимодействующих процессов (9—, , , ), хотя метод инвариантов использовался и для систем асинхронно-взаимодействующих процессов в работах [, , ]. Помимо верификации моделей с произвольным числом однотипных процессов алгоритмы решения задачи РМС позволяют проводить редукцию моделей с большим числом однотипных процессов к моделям с малым числом процессов. Таким образом, решение задачи РМС имеет практический смысл даже тогда, когда рассматриваются модели с фиксированным, но очень большим числом процессов. В этом случае задача, требующая недоступных на практике вычислительных ресурсов, может быть сведена к практически решаемой задаче. Таким образом, задача верификации параметризованных моделей распределённых систем актуальна. Однако при разработке таких методов и средств желательно сохранить основное преимущество метода МС — свойство автоматической верификации модели. Необходимо, чтобы для верификации параметризованной модели не требовалась существенная перестройка модели, использованной при верификации средствами МС, или участие эксперта. Предложен новый метод верификации систем асинхронно-взаимодействующих процессов, позволяющий автоматически вычислять конечные инварианты параметризованных моделей и сводить задачу верификации бесконечных параметризованных моделей к задаче верификации конечных моделей. На основе предложенного метода разработаны новые алгоритмы верификации параметризованных систем асинхронно-взаимодсйствующих процессов, сочетающие методы верификации моделей программ и проверки отношений симуляции между моделями программ. На основе предложенного метода и алгоритмов разработана и реализована экспериментальная система автоматической верификации программ, с помощью которой доказана корректность поведения ряда распределенных алгоритмов и сетевых протоколов, применяющихся на практике. Работа состоит из введения, шести глав, заключения и двух приложений. В первой главе обсуждаются требования, предъявляемые к моделям распределённых систем, а также задача верификации моделей распределённых систем. На основе этого обсуждения формулируется задача верификации параметризованных моделей распределённых систем и формируются требования к методам решения этой задачи. Во второй главе приводится обзор и сравнительный анализ работ, в которых предлагаются решения задачи верификации параметризованных моделей распределённых систем. На основании критериев, предъявляемых к решению задачи с учётом целей настоящей работы, выбирается метод инвариантов, на основе которого разрабатывается предлагаемый в работе метод верификации параметризованных моделей распределённых систем. С учётом выбранного базового метода формулируется декомпозиция задачи. В третьей главе описываются основные понятия теории формальной верификации моделей программ: размеченные системы переходов, темпоральные логики, сетевые грамматики. В терминах введённых понятий формулируется математическая задача проверки выполнимости спецификации, заданной формулой темпоральной логики, на параметризованных моделях программ, представленных посредством размеченных систем переходов и сетевых грамматик. Исследованы основные свойства этих отношений. Показано, что введённые отношения обладают необходимым набором свойств для решения задачи верификации параметризованных моделей распределённых систем с использованием метода инвариантов. В пятой главе описывается модификация метода инвариантов с использованием отношений симуляции, введённых в четвёртой главе.