Введение
1. Логический вывод и верификация параллельных алгоритмов 13
1.1. Подходы к верификации 13
1.2. Формальная верификация алгоритмов и программ 16
1.2.1. Техника дедуктивного анализа 17
1.2.2. Техника проверки эквивалентности 18
1.2.3. Техника проверки моделей 18
1.3. Классическая схема верификации с применением техники проверки моделей 21
1.4. Обзор инструментальных систем формальной верификации 24
1.5. Применение логического вывода для сопоставления реализации и спецификации 31
1.6. Классификация методов логического вывода 32
1.7. Сравнительный анализ методов логического вывода 33
1.8. Выводы 35
2. Формальная верификация параллельных алгоритмов с применением техники проверки моделей и методов логического вывода 37
2.1. Алгоритм формирования базы знаний на основе структуры Крипке и формулы темпоральной логики 37
2.2. Постановка логической задачи формальной верификации 41
2.3. Метод логического вывода для проверки эквивалентности моделей алгоритма и спецификации 41
2.3.1. Унификация литералов 42
2.3.2. Процедуры полного и ограниченного образования остатков 43
2.3.3. Процедура деления дизъюнктов 46
2.3.4. Метод логического вывода делением дизъюнктов на основе определяющего элемента
2.3.5. Схема процесса логического вывода 51
2.3.6. Оценка эффективности метода 55
2.3.7. Анализ особенностей структуры правил в базе знаний 56
2.4. Формирования модели алгоритма 61
2.5. Построение дерева грамматического разбора LTL-спецификации 62
2.5.1. Алгоритм построения дерева грамматического разбора формулы темпоральной логики линейного времени 62
2.5.2. Оптимизация дерева грамматического разбора формулы темпоральной логики линейного времени 67
2.5.3. Метод построения оптимизированного дерева грамматического разбора формулы темпоральной логики линейного времени 75
2.6. Выводы 76
3. Комплекс и машина логического вывода для верификации параллельных алгоритмов 77
3.1. Структура комплекса для формальной верификации параллельных алгоритмов 77
3.2. Модель логического вывода 81
3.2.1. Анализ степени параллелизма используемого метода логического
вывода 81
3.2.2. Древовидное представление модели логического вывода 82
3.2.3. Анализ особенностей модели логического вывода 87
3.2.4. Состояния процессов 91
3.2.5. Типы сообщений 92
3.2.6. Выбор модели вычислений 94
3.2.7. Характеристика модели логического вывода 94
3.3. Машина логического вывода 96
3.3.1. Структура машины 97
3.3.2. Формат фрейма процесса 102
3.3.3. Форматы служебных пакетов и сообщений 105
3.3.4. Форматы данных 108
3.3.5. Принципы организации работы процессора команд 113
3.3.6. Подпрограммы обработки процессов 119
3.3.7. Унификация литералов 122
3.3.8. Начальная инициализация и цикл работы машины 126
3.3.9. Формирование контрпримера 131
3.3.10. Особенности практической реализации машины 131
3.4. Выводы 134
4. Исследование аппаратно-программных реализаций машины логического вывода 136
4.1. Аналитические оценки основных характеристик машины 136
4.2. Программная реализация машины логического вывода 141
4.3. Реализация группы исполнительных процессоров на GPU 144
4.4. Реализация блока унификации на ПЛИС 145
4.5. Оценка производительности реализаций машины логического вывода на тестовых примерах ИС SPIN 148
4.6. Рекомендации по выбору архитектурно-структурных решений машины логического вывода 151
4.7. Выводы 154
Заключение 156
Список использованной литературы 158
