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

Оглавление
Введение .
Проверка корректности программ.
Цель диссертационной работы
, 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. Выводы
Заключение
Литература