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

Оглавление
Введение б
Идея формальных методов.
Принципы формальной верификации.
Цель работы
Основные результаты
Структура работы.
1 Современные средства формальной верификации
1.1 Классификация моделей программ и языков спецификации.
1.2 Верификация моделей программ.
1.2.1 Методы верификации
1.2.2 Обзор современных систем верификации моделей программ.
1.2.3 Тенденции развития средств верификации программ.
1.3 Формальная постановка задачи.
. 1.3.1 Распределенные программы
1.3.2 Модели распределенных программ
1.3.3 Логика ветвящегося времени СТЬ
1.3.4 Формальная постановка задачи
Общая схема алгоритмов верификации программ
2.1 Теоретикомножественная схема верификации программ методом проверки на
модели.
2.2 Поиск подтверждающего вычисления.
2.2.1 Линейные трассы
2.2.2 Циклические трассы
2.3 Алгоритмы верификации справедливых моделей программ
2.3.1 Формальное определение справедливости .
2.3.2 Верификация слабо справедливых моделей программ
ОГЛАВЛЕНИЕ
2.3.3 Верификация сильно справедливых моделей программ.
2.3.4 Модификация алгоритма восстановления трасс.
3 Построение моделей распределенных программ
3.1 язык описания распределенных программ
3.1.1 Основные конструкции языка ММ .
3.1.2 Понятие временного автомата
3.1.3 Временные автоматы контекста.
3.1.4 Семантика языка ММ.
3.2 Язык спецификаций
3.3 Язык представления моделей .
3.3.1 Основные конструкции языка .
3.3.2 Семантика языка
3.3.3 Композиционная семантика программ
3.4 Построение модели распределенной программы.
3.4.1 Абстракция ММпрограмм.
3.4.2 Трансляция элементарных конструкций языка ММ.
3.4.3 Моделирование взаимодействия.
3.5 Корректность трансляции .
3.6 Извлечение контрпримера вычисления на ММ.
4 Графовая реализация алгоритмов верификации
4.1 Графовое представление модели.
4.2 Графовый алгоритм.
4.3 Алгоритм восстановления трасс.
4.4 Справедливая верификация.
4.4.1 Графовый алгоритм верификации в ограничениях слабой справедливости
4.4.2 Графовый алгоритм верификации в ограничениях сильной справедливости
5 Символьная реализация алгоритмов верификации
5.1 Представления булевых функций
5.1.1 Базовые сведения о .
5.1.2 Операции над .
5.2 Символьное представление модели .
5.3 Алгоритм символьной верификации.
5.3.1 Методы повышения эффективности символьной верификации
ОГЛАВЛЕНИЕ
5.4 Алгоритм восстановления трасс
5.5 Справедливая верификация
5.5.1 Алгоритм символьной верификации в ограничениях слабой справедливости
5.5.2 Алгоритм символьной верификации в ограничениях сильной справедливости .
6 Система верификации в среде ДИАНА
6.1 Устройство системы верификации в среде ДИАНА.
6.2 Практические результаты применения системы верификации.
Литература