- Артикул:00-01091992
- Автор: Е.М. Кларк, О. Грамберг, Д. Пелед
- ISBN: 5-94057-054-2
- Тираж: 1000 экз.
- Обложка: Твердая обложка
- Издательство: МЦМНО (все книги издательства)
- Город: Москва
- Страниц: 416
- Формат: 60х90 1/16
- Год: 2002
- Вес: 653 г
Развернуть ▼
В монографии всемирно известных специалистов в области математической логики и теории вычислений представлено полное и подробное изложение нового подхода к решению задачи проверки правильности функционирования сложных программных систем.
Содержание
От редактора перевода
Вступительное слово
Предисловие
1. Введение
1.1. Необходимость использования формальных методов
1.2. Верификация аппаратуры и программного обеспечения
1.3. Процесс верификации моделей программ
1.4. Темпоральная логика и проверка на модели
1.5. Символьные алгоритмы
1.6. Редукция частичных порядков
1.7. Другие подходы к проблеме «комбинаторного взрыва»
2. Моделирование систем
2.1. Моделирование параллельных систем
2.1.1. Представления первого порядка
2.1.2. Степень детализации переходов
2.2. Параллельные системы
2.2.1. Цифровые схемы
2.2.2. Программы
2.2.3. Параллельные программы
2.3. Пример трансляции программы
3. Темпоральные логики
3.1. Логика деревьев вычислений CTL*
3.2. CTL и LTL
3.3. Справедливость
4. Верификация моделей
4.1. Верификация моделей для CTL
4.1.1. Ограничения справедливости
4.2. Табличная верификация моделей для LTL
4.3. Верификация моделей для CTL*
5. Двоичные разрешающие диаграммы
5.1. Представление булевых функций
5.2. Представление моделей Крипке
6. Символьная верификация моделей
6.1. Представления неподвижной точки
6.2. Символьная верификация моделей для CTL
6.2.1. Квантифицированные булевы формулы
6.2.2. Символьный алгоритм верификации моделей
6.3. Как учитывать справедливость при верификации
6.4. Контрпримеры и свидетельства
6.5. Пример АЛУ
6.6. Вычисление реляционных произведений
6.6.1. Расщепленные отношения переходов
6.6.2. Рекомбинация разбиений
6.6.3. Еще раз о примере АЛУ
6.7. Символьная верификация моделей для LTL
7. Верификация моделей для ?-исчисления
7.1. Введение
7.2. Пропозициональное ?-исчисление
7.3. Вычисление значений формул неподвижной точки
7.4. Представление формул ?-исчисления
7.5. Трансляция CTL в ?-исчисление
7.6. Вопросы сложности
8. Верификация моделей на практике
8.1. Программа SMV верификации моделей
8.2. Пример из практики
9. Верификация моделей и теория автоматов
9.1. Автоматы на конечных и бесконечных словах
9.2. Верификация моделей при помощи автоматов
9.2.1. Недетерминированные автоматы Бюхи
9.2.2. Обобщенные автоматы Бюхи
9.3. Проверка пустоты
9.4. Трансляция LTL в автоматы
9.5. Верификация моделей на лету
9.6. Символьная проверка вложенности языков
10. Редукция частичных порядков
10.1. Параллельность в асинхронных системах
10.2. Независимость и невидимость
10.3. Редукция частичных порядков для LTL-х
10.4. Пример
10.5. Вычисление достаточных множеств
10.5.1. Сложность проверки условий
10.5.2. Эвристики для достаточных множеств
10.5.3. Редукция на лету
10.6. Корректность алгоритма
10.7. Редукция частичных порядков в системе SPIN
11. Эквивалентности и квазипорядки на моделях
11.1. Алгоритмы эквивалентности и квазипорядка
11.2. Табличная конструкция
12. Композиционные доказательства
12.1. Композиция моделей
12.2. Обоснование по схеме «допущение-подтверждение»
12.3. Верификация устройства управления
13. Абстракция
13.1. Редукция по конусу влияния
13.2. Абстракция данных
13.2.1. Вычисление аппроксимаций
13.2.2. Точные аппроксимации
13.2.3. Простой язык
13.2.4. Пример абстракций
13.2.5. Конгруенция по модулю натурального числа
13.2.6. Представление по логарифму
13.2.7. Абстракции одиночного бита и декартова произведения
13.2.8. Символьные абстракции
14. Симметрия
14.1. Группы и симметрия
14.2. Фактормодели
14.3. Верификация моделей с использованием симметрии
14.4. Вопросы сложности
14.4.1. Задача вычисления орбит и изоморфизм графов
14.4.2. Отношение орбит и OBDD
14.5. Практические результаты
15. Бесконечные семейства конечных систем
15.1. Темпоральные логики для бесконечных семейств
15.2. Инварианты
15.3. Пересмотренный пример Futurebus+
15.4. Графовые и сетевые грамматики
15.5. Неразрешимость семейства колец с маркерами
16. Дискретное время и количественный анализ
16.1. Системы реального времени
16.2. О верификации систем реального времени
16.2.1. Родственные методы верификации систем реального времени
16.3. Проверка выполнимости на модели для RTCTL
16.4. Количественный временной анализ
16.4.1. Алгоритм вычисления минимальной задержки
16.4.2. Алгоритм вычисления максимальной задержки
16.5. Пример: бортовая система управления
16.5.1. Описание системы
16.5.2. Модель бортовой системы управления
16.5.3. Результаты верификации
17. Непрерывное реальное время
17.1. Временные автоматы
17.2. Параллельная композиция
17.3. Моделирование временными автоматами
17.4. Часовые области
17.5. Часовые пояса
17.6. Матрицы разностных границ
17.6.1. Вопросы сложности
18. Заключение
19. Литература
Предметный указатель
Рекомендуем
