Введение
1 Введение 3
1.1 Общая характеристика работы 3
1.2 Формальные методы верификации 4
1.3 Содержание диссертационной работы 7
2 Временная логика первого порядка FOTL 13
2.1 Синтаксис и семантика FOTL 13
2.2 Разрешимость конечно-определяемых свойств 16
2.3 FOTL-метод 22
3 Модификации FOTL-метода 31
3.1 Расширение языка рассматриваемых формул 31
3.2 Свойства внутренних и внешних функций 34
3.3 Строгие конечные интерпретации 41
3.4 Ступенчатые конечные интерпретации 45
3.5 Ступенчато-строгие интерпретации 48
3.6 Отсутствие равенства для абстрактных сортов 50
4 Реализация FOTL-метода 52
4.1 Автоматическая генерация FOTL-формулы, описывающей запуски ASM 52
4.2 Компьютерные реализации методов элиминации кванторов 53
4.3 Прототип системы компьютерной верификации систем реального времени 56
5 Обобщенная задача о железнодорожном переезде 63
5.1 Постановка задачи GRCP 63
5.2 Моделизация GRCP 65
5.3 Разрешимый класс FOTL для верификации GRCP 69
5.4 Компьютерная верификация GRCP 72
6 IEEE 1394 Root Contention Protocol 74
6.1 Неформальное описание IEEE 1394 RCP 74
6.2 Моделирование протокола при помощи ASM 79
6.3 Требования корректности на языке FOTL 85
6.4 Разрешимость верификации корректности RCP 88
6.5 Компьютерная верификация протокола 93
Литература 95
