MODEL СHECKING. Верификация параллельных и распределенных программных систем

Description

В книге рассказывается о новых результатах в области верификации с помощью метода model checking и приводятся примеры приложений этого метода в самых разных областях. Рассматриваются проблема верификации, темпоральные логики, алгоритмы model checking для CTL и LTL, структуры Крипке как модели реагирующих систем, спецификация свойств реагирующих систем формулами темпоральной логики, бинарные решающие диаграммы, символьная верификация, количественный анализ систем и системы реального времени, а также применение фундаментальных идей алгоритма model checking в различных приложениях. На прилагаемом компакт-диске находятся: инструкция по установке системы верификации Spin, методическое пособие по этой системе и описание курсовой работы по верификации нетривиальной системы логического управления с несколькими вариантами заданий. Оглавление Предисловие Структура книги Сопровождающий компакт-диск Благодарности Глава 1. Проблема верификации 1.1. Ошибки в программах и их последствия 1.2. Примеры ошибочных программ 1.3. Общая схема верификации. Проверка моделей (model checking) 1.4. Тестирование и верификация 1.5. Примеры успешной верификации систем 1.6. Инструменты верификации 1.7. Заключение 1.8. Замечания 1.9. Задачи к главе 1 Глава 2. Темпоральные логики 2.1. Утверждения, истинность которых зависит от времени 2.2. Модальные и временные логики. Tense Logic 2.3. Темпоральная логика линейного времени (LTL) 2.4. Реагирующие системы (reactive systems) 2.5. Формальное определение LTL 2.6. Примеры использования формул LTL 2.7. Соотношения между операторами LTL 2.8. Структура Крипке 2.9. Расширенная темпоральная логика ветвящегося времени CTL* 2.10. Сравнение логик LTL и CTL 2.11. Темпоральные логики прошлого 2.12. Model checking 2.13. Заключение 2.14. Замечания 2.15. Задачи к главе 2 Глава 3. Алгоритм model checking для CTL 3.1. Темпоральная логика ветвящегося времени CTL 3.2. Семантика СTL на деревьях вычислений 3.3. Формальная семантика CTL 3.4. Проверка формул CTL на развертке структуры Крипке 3.5. Базисы CTL 3.6. Алгоритм model checking для CTL 3.7. Пример выполнения алгоритма model checking 3.8. Заключение 3.9. Замечания 3.10. Задачи к главе 3 Глава 4. Алгоритм model checking для LTL 4.1. Проверка выполнимости LTL-формул на вычислениях 4.2. Пересечение языков в теории конечных автоматов 4.3. Теоретико-автоматный метод проверки выполнимости LTL-формулы 4.4. Автоматы Бюхи — модели для задания щ-языков 4.5. Операции над автоматами Бюхи 4.6. Автоматы Бюхи и LTL-формулы 4.7. Структуры Крипке и автоматы Бюхи 4.8. Проверка модели для формул LTL 4.9. Построение автомата Бюхи по формуле LTL 4.10. Заключение 4.11. Замечания 4.12. Задачи к главе 4 Глава 5. Структуры Крипке как модели реагирующих систем 5.1. Состояния и переходы реагирующей системы. Гранулярность переходов 5.2. Реагирующие системы, специфицированные в виде систем переходов 5.3. Реагирующие системы, специфицированные в виде нескольких взаимодействующих систем переходов 5.4. Представление программы с конечным числом состояний структурой Крипке 5.5. Представление параллельных программ структурой Крипке 5.6. Пакеты верификации и структура Крипке. Пакет верификации Spin 5.7. Построение структуры Крипке для программ высокого уровня 5.8. Заключение 5.9. Замечания 5.10. Задачи к главе 5 Глава 6. Спецификация свойств реагирующих систем формулами темпоральной логики 6.1. Примеры спецификации свойств технических систем 6.2. Свойства достижимости (reachability) 6.3. Свойства безопасности (safety) 6.4. Свойства живости (liveness) 6.5. Свойства справедливости (fairness) 6.6. Спецификация справедливости в логике CTL 6.7. Справедливая CTL (fair CTL) 6.8. Заключение 6.9. Замечания 6.10. Задачи к главе 6 Глава 7. Примеры верификации 7.1. Протокол передачи данных W.C.Lynch 7.2. Протокол PAR 7.3. Протокол двухфазной фиксации 7.4. Заключение 7.5. Замечания 7.6. Задачи к главе 7 Глава 8. Применения алгоритма model checking 8.1. Анализ бизнес-процессов 8.2. Проблема планирования как model checking 8.3. Логические головоломки и model checking 8.4. Верификация криптографических протоколов 8.5. Заключение 8.6. Замечания 8.7. Задачи к главе 8 Глава 9. Бинарные решающие диаграммы 9.1. Проблемы с представлением булевых функций 9.2. Бинарные решающие диаграммы 9.3. Свойства бинарных решающих диаграмм 9.4. Операции над BDD 9.5. Проблема булевой выполнимости (SAT) и бинарные решающие диаграммы 9.6. Применения BDD к решению логических и комбинаторных задач 9.7. Использование BDD в анализе и синтезе логических схем 9.8. Конечные структуры данных и BDD 9.9. Символьные и неявные алгоритмы обработки данных 9.10. Бинарные решающие диаграммы с подавлением нулей 9.11. Заключение 9.12. Замечания 9.13. Задачи к главе 9 Глава 10. Символьная верификация 10.1. Необходимость символьных методов в верификации 10.2. Представление структуры Крипке булевыми функциями 10.3. Представление структуры Крипке реагирующих систем булевыми функциями без предварительного явного построения структуры Крип 10.4. Представление булевыми функциями структуры Крипке для программ 10.5. Символьный алгоритм model checking для CTL 10.6. Операторы на множествах и неподвижные точки 10.7. Теорема Тарского о неподвижной точке 10.8. Символьный алгоритм верификации для формулы EF. 10.9. Определение темпоральных формул CTL через неподвижные точки операторов 10.10. Заключение 10.11. Замечания 10.12. Задачи к главе 10 Глава 11. Количественный анализ систем 11.1. Вероятностный метод model checking 11.2. Вероятностная логика ветвящегося времени (Probabilistic CTL, PCTL) и верификация вероятностных моделей 11.3. Проверка свойств, зависящих от дискретного времени и вероятностного выбора 11.4. Примеры свойств, выражаемых в PCTL 11.5. Заключение 11.6. Замечания 11.7. Задачи к главе 11 Глава 12. Системы реального времени 12.1. Модель систем реального времени. Временнo„z „p„rтомат и его поведение 12.2. Сети временных автоматов: параллельная композиция 12.3. Операционная семантика модели времен„~oго автомата — система переходов 12.4. Нереалистичные поведения времен„~oго автомата 12.5. Проблема анализа системы переходов временного автомата 12.6. Временные регионы: один таймер 12.7. Граф регионов временного автомата 12.8. Временные регионы для нескольких локальных часов 12.9. Анализ временных автоматов: логика CTL 12.10. Временная темпоральная логика ветвящегося времени (Timed CTL) 12.11. Анализ временных автоматов: сведение проверки TCTL-формул к проверке CTL-формул 12.12. Сложность алгоритмов model checking для логики TCTL 12.13. Другие проблемы верификации временных автоматов 12.14. Временные зоны 12.15. Инструменты верификации систем реального времени 12.16. Заключение 12.17. Замечания 12.18. Задачи к главе 12 Заключение Список литературы Иностранные издания Литература на русском языке Материалы из Интернета Предметный указатель