Оглавление
1 Введение .
1.1 Общая характеристика работы
1.2 Формальные методы верификации
1.3 Содержание диссертационной работы
2 Временная логика первого порядка .
2.1 Синтаксис и семантика
2.2 Разрешимость конечноопределяемых свойств .
2.3 метод.
3 Модификации метода .
3.1 Расширение языка рассматриваемых формул
32 Свойства внутренних и внешних функций .
3.3 Строгие конечные интерпретации.
3.4 Ступенчатые конечные интерпретации
3.5 Ступенчатострогие интерпретации.
3.6 Отсутствие равенства для абстрактных сортов
4 Реализация метода
4.1 Автоматическая генерация формулы, описывающей запуски
4.2 Компьютерные реализации методов элиминации кванторов
4.3 Прототип системы компьютерной верификации систем реального времени .
5 Обобщенная задача о железнодорожном переезде
5.1 Постановка задачи
5.2 Моделизация
5.3 Разрешимый класс для верификации .
5.4 Компьютерная верификация .
6 I i .
6.1 Неформальное описание I .
6.2 Моделирование протокола при помощи .
6.3 Требования корректности на языке .
6.4 Разрешимость верификации корректности
6.5 Компьютерная верификация протокола
Литература
- Київ+380960830922