Методы верификации программ

Содержание книги "Методы верификации программ "

1.Введение
1.1.Проблема верификации программ
1.2.Необходимые математические понятия
1.2.1. Термы и связанные с ними понятия
1.2.2. Примеры типов и функциональных символов
1.2.3.Подстановки
1.2.4. Массивы
1.2.5.Истинностные значения утверждений
I. Верификация последовательных и распределённых программ
2. Программы,.представленные в виде блок-схем
2.1.Понятие блок-схемы
2.2.Выполнение блок-схемы
2.3.При меры блок-схем
2.4.Задача верификации.блок-схем
3. Метод инвариантов для верификации.блок-схем
3.1.Базовые множества и базовые пути
3.2.Описание метода инвариантов
3.3.Обоснование метода инвариантов
3.4.При меры фундированных множеств
3.5.Применение метода инвариантов
3.5.1.Верификация блок-схемы вычисления суммы
3.5.2.Верификация блок-схемы деления с остатком
3.5.3.Верификация блок-схемы извлечения корня
3.5.4.Верификация блок-схемы возведения в степень
3.5.5. Верификация блок-схемы сортировки
4. Процессные.представления блок-схем
4.1.Понятие процесса
4.1.1.Действия
4.1.2. Процессы и их выполнение
4.2.Процессы, соответствующие блок-схемам
4.3.Верификация процессных представле ний блок-схем
5. Верификация операторных программ
5.1.Понятие операторной программы
5.2.Примеры операторных программ
5.3.Метод инвариантов для верификации операторных программ
5.4.Пример верификации операторной программы
6. Распределенные программы
6.1.Понятие распределенной программы
6.1.1.Действия
6.1.2. Процессы
6.1.3.Распределенные программы
6.1.4. Каналы в распределенных.программах
6.1.5.Переходы в распределенных программах
6.1.6. Выполнение распределенной программы
6.2.Спецификация и верификация распределенных программ
6.3.Примеры распределенных программ
6.3.1.Вычисление факториала
6.3.2. Передача сообщений через буфер
6.3.3.Избрание лидера
6.3.4.Параллельная сортировка
6.4.Распределенная программа перемножения матриц
6.4.1.Неформальное описание распределенной программы перемножения матриц
6.4.2. Спецификация программы перемножения матриц
6.4.3.Определение распределённой программы перемножения матриц
6.4.4. Дополненные процессы
6.4.5.Верификация программы перемножения матриц
7. Задачи и исследовательские проблемы
7.1.Верификация программ без массивов
7.1.1.Произведение двух чисел
7.1.2. Возведение в степень
7.1.3.Извлечение квадратного корня
7.1.4.Извлечение логарифма
7.1.5.Вычисление частного и остатка от деления целых чисел
7.1.6. Наибольший общий делитель
7.1.7.Представление наибольшего общего делителя линейной формой
7.1.8.Наибольший общий делитель и наименьшее общее кратное
7.1.9. Приближенное решение уравнения
7.1.10. Проверка на простоту
7.1.11. Проверка, является ли число совершенным
7.2.Верификация программ с массивами
7.2.1.Инвертирование массива
7.2.2.Минимальный элемент массива
7.2.3.Двоичный поиск
7.2.4. Наибольший общий делитель компонентов массива
7.2.5. Список простых чисел от 2 до n
7.2.6. Сортировка массива
7.2.7.Перестановка массива с заданным условием
7.2.8.Перестановка массива в заданном порядке
7.2.9. Вычисление определителя матрицы
7.3.Задачи на составление программ
7.4.Верификация распределенных программ
7.5.Исследовательские проблемы
II. Верификация функциональных программ
8. Введение в функциональное программирование
8.1.Парадигма функционального программирования
8.2.Примеры функциональных программ
8.2.1. Конкатенация строк
8.2.2. Инвертирование строки
8.2.3. Поиск подстроки
9. Функциональные программы
9.1.Пополненные домены и функции на них
9.1.1. Пополненные домены
9.1.2.Монотонные функции
9.1.3. Естественные продолжения
9.1.4.Частично упоря доченные множества монотонных функций
9.1.5.Полные частично упорядоченные множества
9.2.Функциональные программы
9.2.1. Понятие функциональной программы
9.2.2.Функционал, соответствующий функциональной программе
9.2.3. Непрерывные функционалы на полных частично упорядоченных множествах
9.2.4.Неподвижные точки функционалов на полных частично упорядоченных множествах
9.2.5.Непрерывность функционалов, соответствующих функциональным программам
9.2.6. Нахождение наименьших неподвиж ных точек функциональных программ
9.2.7. Примеры неподвиж ных точек функциональных программ
9.2.8. Немонотонные функциональные программы
9.3.Алгоритмическая полнота функциональных программ
10. Вычисление значений наименьших неподвижных точек
1О.1.Постановка задачи
10.2.Метод решения
10.3.Вычислительные правила
10.4.Упрощение терма
10.5.Функция С
10.6.Вспомогательные понятия
10.6.1. Полные раскрытия
10.6.2. Индексированные термы
10.6.3. n-переходы
10.7.Безопасные вычислительные правила
10.8.Свойства правил РО , LO , PI , LI
10.8.1. Безопасность правила РО
10.8.2. Безопасность правила LO
10.8.3. Пример небезопасности правила LO
10.8.4.Пример небезопасности правил PI и LI
11. Верификация.функциональных программ
11.1.Задача верификации функциональных программ
11.2.Метод вычислительной индук ции
11.2.1. Описание метода
11.2.2. Примеры верификации функциональных программ методом вычислительной индукции
11.3.Метод структурной индукции
11.3.1.Описание метода
11.3.2. Примеры верификации функциональных программ методом структурной индукции
11.4.Другие методы верификации функциональных программ
11.4.1. Оценка наименьшей неподвижной точки функциональной программы сверху
11.4.2. Эквивалентные преобра:зования функциональных программ
12.Задачи.и исследовательские проблемы
12.1.Нахождение наименьших неподвижных точек функциональных программ
12.2.Вид наименьших неподвижных точек
12.3.Функции, определяемые функциональными программами
12.4.Свойства наименьших неподвижных точек
12.5.Исследовательские проблемы
III. Model checking
13. Модели распределённых программ
13.1.Верификация распределённых программ
13.1.1. Математические модели распределённых рограмм
13.1.2. Спецификация
13.1.3. Построение формальных докfзательств
13.2.Системы переходов
13.2.1. Понятие системы переходов
13.2.2. Пути в системах переходов
13.2.3. Построение системы переходов, соответствующей распределенной программе
14. Model checking на основе CTL
14.1.Темпоральная логика CTL
14.1.1.Формулы темпоральной логики CTL
14.1.2. Значения СТL-формул
14.1.3.Эквивалентность СТL-формул
14.1.4. Примеры свойств распределённых программ, выражаемых СТL-формулами
14.2.Задача moclel checking для CTL
14.3.MC-CTL.на основе понятия неподвижной точки
14.3.1.Неподвижные точки монотонных операторов
14.3.2. Вычисление множеств.(E U (B,.С)) '"ⁱ.и.( EG B )'"ⁱ на основе понятия неподвижной точки
14.3.3. Алгоритм.решения задачи MC-CTL на основе понятия неподвижной.точки
14.4.µ-исчисление
14.4.1. Jt-формулы
14.4.2. Значения µ-формул
14.4.3.Ускоренное вычисление значений µ-формул
14.4.4. Вложение CTL в µ-исчисление
15. Бинарные диаграммы решений
15.1.Бинарные диаграммы решений и их свойства
15.1.1. Определение бинарной диаграммы решений
15.1.2. Эквивалентность и изомо рфность бинарных диаграмм решений
15.1.3. Представлениемножеств зам кнутых подстановок бинарными диаграммами.решений
15.1.4. Редукция бинарных диаграмм решений
15.1.5. Представление булевых функций
15.1.6. Подстановка значений вместо переменных
15.2.Согласованность с порядком переменных
15.3.Алгебраические операции на BDD
15.3.1. Булевы операции
15.3.2. Произведение
15.4.MC-CTL с использованием бинарных диаграмм решений
15.5.Оптимизирующие преобразования
16. Model checking на основе LTL
16.1.Формулы темпоральной логики LTL
16.2.Квантифицированные LТL-формулы
16.3.Задачи model checking для.LTL
16.3.1. Система переходов Ел
16.3.2. Система переходов Е х Ел
16.3.3. Первая задача model checking для LTL
16.3.4. Вторая задача model checking для LTL
16.4.Автоматы Бюхи
16.4.1. Понятие автомата Бюхи
16.4.2. Язык автомата
16.4.3. Эквивалентность автоматов
16.4.4. Пересечение автоматов
16.4.5. Исполь зование автоматов Бюхи для MC-LTL
16.4.6. Оптимизация построения автомата Ел
17. Вероятностный model checking
17.1.Введение
17.2.Вероятностные.системы.переходов
17.2.1. Понятие вероятностной системы переходов
17.2.2. Примеры.вероятностных систем переходов
17.3.Темпоральная логика PCTL
17.3.1. Свойства вероятностных систем переходов
17.3.2. Формулы логики PCTL
17.3.3. Значения формул логики PCTL в состояниях вероятностных систем переходов
17.3.4. Интерпретация значений формул логики PCTL
18. Задачи и исследовательские проблемы
18.1.Задачи
18.2.Исследовательские проблемы
IV. Теория процессов
19. Понятие процесса
19.1.Неформальное понятие процесса и примеры процессов
19.1.1.Неформальное понятие процесса
19.1.2. Пример процесса
19.1.3.Другой пример процесса
19.2.Действия
19.3.Определение понятия процесса
20. Операции на процессах
20.1.Префиксное действие
20.2.Пустой процесс
20.3.Альтернативная композиция
20.4.Параллельная композиция
20.5.Ограничение
20.6.Переименование
20.7.Свойства операций на процессах
21. Эквивалентности процессов
21.1.Простая эквивалентность
21.1.1.Поведение процесса
21.1.2. Понятие простой эквивалентности
21.1.3. Примеры процессов, находящихся в отношении простой эквивалентности
21.2.Сильная эквивалентность
21.2.1.Понятие сильной эквивалентности
21.2.2. Критерий сильной эквивалентности, основанный на понятии бимоделирования
21.2.3. Логический критерий сильной эквивалентности
21.2.4. Алгебраические свойства сильной эквивалентности
21.2.5. Ра спознавание сильной эквивалентности
21.2.6. Мини мизация процессов относительно сильной эквивалентности
21.3.Наблюдаемая эквивалентность
21.3.1.Определение наблюдаемой эквивалентности
21.3.2. Критерий наблюдаемой эквивалентности, основанный на понятии наблюдаемогобимоделирования
21.3.3. Логический критерий наблюдаемой эквивалентности процессов
21.3.4. Алгебраические свойства наблюдаемой эквивалентности
21.3.5. Ра спознавание наблюдаемой эквивалентности
21.4.Наблюдаемая конгруэнция
21.4.1. Мотивировка наблюдаемой конгруэнции
21.4.2. Определение наблюдаемой конгруэнции
21.4.3. Связь между наблюдаемой эквивалентностью и наблюдаемой конгруэнцией
21.5.Другие эквивалентности процессов
22. Примеры.доказательства свойств процессов
22.1.Мастерская
22.2.Планировщик
23. Процессы с передачей сообщений
23.1.Действия с передачей сообщений
23.2.Процессы с передачей сообщений
23.2.1.Операторы
23.2.2. Понятие процесса с передачей сообщений
23.2.3. Операции на процессах
23.2.4. Редукция процессов
23.3.Наблюдаемая эквивалентность процессов
23.3.1.Система переходов процесса
23.3.2. Метод доказательства наблюдаемой эквивалентности процессов
23.4.Примеры верификации процессов с передачей сообщений
23.4.1. Последовательная композиция буферов
23.4.2. Разделение мультимножеств
23.4.3. Вычисление квадрата
24. Процессы с асинхронным взаимодействием
24.1.Понятие асинхронного взаимодействия
24.2.Понятие процесса с асинхронным взаимодействием
24.3.Протоколы передачи данных
24.3.1.Однонаправленный протокол с чередующимися.битами
24.3.2. Двунаправленный протокол передачи сообщений с чередующимися битами
24.3.3. Протокол скользящего окна с возвратом
24.3.4. Протокол скользящего окна с заданным повтором
25. Задачии исследовательские проблемы