Оглавление.

Глава 1. Проблема верификации
13
1.1. Ошибки в программах и их последствия 13
1.2. Примеры ошибочных программ 18
1.3. Общая схема верификации. Проверка моделей (model checking) 24
1.4. Тестирование и верификация 30
1.5. Примеры успешной верификации систем 33
1.6. Инструменты верификации 35
1.7. Заключение 36
1.8. Замечания 37
1.9. Задачи к главе 1 38
Глава 2. Темпоральные логики
41
2.1. Утверждения, истинность которых зависит от времени 41
2.2. Модальные и временные логики. Tense Logic 45
2.3. Темпоральная логика линейного времени (LTL) 51
2.4. Реагирующие системы (reactive systems) 58
2.5. Формальное определение LTL 62
2.6. Примеры использования формул LTL 64
2.7. Соотношения между операторами LTL 66
2.8. Структура Крипке 68
2.9. Расширенная темпоральная логика ветвящегося времени CTL* 73
2.10. Сравнение логик LTL и CTL 80
2.11. Темпоральные логики прошлого 82
2.12. Model checking 82
2.13. Заключение 83
2.14. Замечания 84
2.15. Задачи к главе 2 85
Глава 3. Алгоритм model checking для CTL
91
3.1. Темпоральная логика ветвящегося времени CTL 91
3.2. Семантика СTL на деревьях вычислений 92
3.3. Формальная семантика CTL 96
3.4. Проверка формул CTL на развертке структуры Крипке 98
3.5. Базисы CTL 99
3.6. Алгоритм model checking для CTL 103
3.7. Пример выполнения алгоритма model checking 111
3.8. Заключение 113
3.9. Замечания 113
3.10. Задачи к главе 3 114
Глава 4. Алгоритм model checking для LTL
117
4.1. Проверка выполнимости LTL-формул на вычислениях 118
Поиск контрпримеров 119
Контрольный автомат 120
4.2. Пересечение языков в теории конечных автоматов 123
Конечные автоматы и автоматные языки 123
Синхронная композиция автоматов и пересечение языков 125
4.3. Теоретико-автоматный метод проверки выполнимости LTL-формулы 128
4.4. Автоматы Бюхи — модели для задания w-языков 130
w-языки и поведение реагирующих систем 131
Автомат Бюхи как контрольный автомат для реагирующей системы 134
4.5. Операции над автоматами Бюхи 135
4.6. Автоматы Бюхи и LTL-формулы 141
4.7. Структуры Крипке и автоматы Бюхи 144
4.8. Проверка модели для формул LTL 146
4.9. Построение автомата Бюхи по формуле LTL 147
Разметка состояний вычисления формулами LTL 148
Атомы темпоральной формулы логики LTL 150
Переходы между состояниями искомого автомата Бюхи 155
Допускающие состояния искомого автомата Бюхи 157
Построение автомата Бюхи по формуле LTL 157
4.10. Заключение 164
4.11. Замечания 166
4.12. Задачи к главе 4 167
Глава 5. Структуры Крипке как модели реагирующих систем
171
5.1. Состояния и переходы реагирующей системы. Гранулярность переходов 171
5.2. Реагирующие системы, специфицированные в виде систем переходов 175
5.3. Реагирующие системы, специфицированные в виде нескольких взаимодействующих систем переходов 177
5.4. Представление программы с конечным числом состояний структурой Крипке 186
5.5. Представление параллельных программ структурой Крипке 189
5.6. Пакеты верификации и структура Крипке. Пакет верификации Spin 197
5.7. Построение структуры Крипке для программ высокого уровня 204
5.8. Заключение 206
5.9. Замечания 207
5.10. Задачи к главе 5 209
Глава 6. Спецификация свойств реагирующих систем формулами темпоральной логики
215
6.1. Примеры спецификации свойств технических систем 216
Причинно-следственная связь событий 216
Примеры спецификации свойств систем формулами LTL 218
Спецификация формулами LTL выполнения события на вычислениях 219
Спецификация формулами LTL отсутствия события на вычислениях 219
Примеры спецификации свойств систем формулами CTL 219
6.2. Свойства достижимости (reachability) 221
6.3. Свойства безопасности (safety) 222
6.4. Свойства живости (liveness) 227
6.5. Свойства справедливости (fairness) 229
6.6. Спецификация справедливости в логике CTL 233
6.7. Справедливая CTL (fair CTL) 237
6.8. Заключение 244
6.9. Замечания 244
6.10. Задачи к главе 6 245
Глава 7. Примеры верификации
247
7.1. Протокол передачи данных W.C.Lynch 247
7.2. Протокол PAR 250
7.3. Протокол двухфазной фиксации 253
7.4. Заключение 255
7.5. Замечания 256
7.6. Задачи к главе 7 257
Глава 8. Применения алгоритма model checking
259
8.1. Анализ бизнес-процессов 259
8.2. Проблема планирования как model checking 262
8.3. Логические головоломки и model checking 267
8.4. Верификация криптографических протоколов 279
8.5. Заключение 290
8.6. Замечания 291
8.7. Задачи к главе 8 292
Глава 9. Бинарные решающие диаграммы
295
9.1. Проблемы с представлением булевых функций 296
9.2. Бинарные решающие диаграммы 301
9.3. Свойства бинарных решающих диаграмм 308
9.4. Операции над BDD 312
9.5. Проблема булевой выполнимости (SAT) и бинарные решающие диаграммы 328
9.6. Применения BDD к решению логических и комбинаторных задач 330
9.7. Использование BDD в анализе и синтезе логических схем 340
9.8. Конечные структуры данных и BDD 345
Представление отношений c помощью характеристических булевых функций 347
Операции над отношениями 349
9.9. Символьные и неявные алгоритмы обработки данных 355
Пример символьного алгоритма: анализ достижимости на графе 356
9.10. Бинарные решающие диаграммы с подавлением нулей 358
9.11. Заключение 363
9.12. Замечания 364
9.13. Задачи к главе 9 366
Глава 10. Символьная верификация
367
10.1. Необходимость символьных методов в верификации 368
10.2. Представление структуры Крипке булевыми функциями 370
10.3. Представление структуры Крипке реагирующих систем булевыми функциями без предварительного явного построения структуры Крипке 372
10.4. Представление булевыми функциями структуры Крипке для программ 375
10.5. Символьный алгоритм model checking для CTL 380
10.6. Операторы на множествах и неподвижные точки 385
10.7. Теорема Тарского о неподвижной точке 390
Решетки 392
10.8. Символьный алгоритм верификации для формулы EF? 395
10.9. Определение темпоральных формул CTL через неподвижные точки операторов 403
10.10. Заключение 410
10.11. Замечания 411
10.12. Задачи к главе 10 411
Глава 11. Количественный анализ систем
415
11.1. Вероятностный метод model checking 416
11.2. Вероятностная логика ветвящегося времени (Probabilistic CTL, PCTL) и верификация вероятностных моделей 427
11.3. Проверка свойств, зависящих от дискретного времени и вероятностного выбора 432
11.4. Примеры свойств, выражаемых в PCTL 437
11.5. Заключение 440
11.6. Замечания 441
11.7. Задачи к главе 11 442
Глава 12. Системы реального времени
445
12.1. Модель систем реального времени. Временн?й автомат и его поведение 446
12.2. Сети временных автоматов: параллельная композиция 453
12.3. Операционная семантика модели временн?го автомата — система переходов 457
12.4. Нереалистичные поведения временн?го автомата 462
12.5. Проблема анализа системы переходов временного автомата 465
12.6. Временные регионы: один таймер 468
12.7. Граф регионов временного автомата 472
12.8. Временные регионы для нескольких локальных часов 476
12.9. Анализ временных автоматов: логика CTL 482
12.10. Временная темпоральная логика ветвящегося времени (Timed CTL) 489
Интерпретация формул TCTL 491
Формальная семантика TCTL 494
12.11. Анализ временных автоматов: сведение проверки TCTL-формул к проверке CTL-формул 496
12.12. Сложность алгоритмов model checking для логики TCTL 506
12.13. Другие проблемы верификации временных автоматов 507
Допускаемый язык 507
Бисимуляция 508
Достижимость 510
12.14. Временные зоны 511
Временные регионы и временные зоны 511
Операции над зонами 515
Пересечение зоны с ограничениями на показания часов 515
Приращение времени 515
Достижимость за один шаг 516
Структуры данных для представления временных зон 521
Матрица разностей границ (Difference Bound Matrix, DBM) 522
Разностная решающая диаграмма (Difference Decision Diagram, DDD) 524
12.15. Инструменты верификации систем реального времени 525
Uppaal 525
Kronos 526
12.16. Заключение 527
12.17. Замечания 529
12.18. Задачи к главе 12 530
Заключение 533
Список литературы 535
Иностранные издания 535
Литература на русском языке 544
Материалы из Интернета 545
Предметный указатель