Модификации и реализации FOTL-метода компьютерной верификации алгоритмов, использующих линейное время

• Автор: Прокофьева, Евгения Юрьевна
• Шифр специальности: 05.13.17
• Научная степень: Кандидатская
• Год защиты: 2004
• Место защиты: Санкт-Петербург
• Количество страниц: 99 с.

Оглавление

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 Компьютерная верификация протокола
Литература


В тех случаях, когда результат слишком длинный для восприятия человеком, в заключение могут быть применены алгоритмы символьных преобразований для приведения формулы к более простому виду. Реализация данного метода и его тестирование даже на маленьких примерах показало невозможность успешного завершения четвертого этапа при существующих реализациях методов элиминации кванторов в ночное время1. Это объясняется тем, что большинство алгоритмов, лежащих в основе FOTL-метода, имеют экспоненциальные и супер-экспоненциальные нижние оценки сложности. Для больших исходных данных такие оценки не позволяют получить эффективно работающие алгоритмы. Для повышения эффективности FOTL-метода разработаны шесть модификаций алгоритма элиминации функциональных символов. Применение модифицированного FOTL-метода дало успешные результаты при компьютерной верификации обобщенной проблемы железнодорожного перекрестка и протокола выбора лидера из двух конкурирующих процессов стандарта IEEE . Эксперименты проводились на компьютерах с процессором иИгаврагс II (Ь»1з) 0п^Ь с памятью Ю и процессором ЩгаБрагс III (Ы) (2х)0ш§Ь с памятью 4С. Все вычисления, превосходящие 0-0 минут, прерывались. В главе 2 рассматриваются временные логики первого порядка ЕОТЬ, предложенные О. Веаисрпег и А. Иьэепко [, ]. ЕОТЬ являются расширением теории сложения вещественных чисел конечными абстрактными сортами и временными функциями. Для фиксированной сигнатуры логик РОТЬ понятие терма и формулы определяется классическим для предикатной логики первого порядка образом. Понятия интерпретации, модели, выполнимости, общезначимости и опровержимости аналогичны соответствующим понятиям предикатной логики первого порядка. Логики РОТЬ позволяют выражать спецификации требований, которые обычно даются на естественном языке. Если они выражены не достаточно полно и четко, попытка формализации позволяет выявить слабые места, которые требуют доработки. В 3, ] авторы изучают разрешимые классы РОТЬ-логик. Разрешимый класс проблем верификации, исследуемый в этой работе, описан в [| и моделирует некоторые “конечные” свойства систем контроля. Эти “конечные” свойства сформулированы в терминах интерпретаций формул и названы конечной выполнимостью и конечной опровержимостъю. Конечная выполнимость формулы Е означает, что каждый “конечный кусок” произвольной модели формулы Е может быть расширен до “конечноопределимой” модели Г. Конечная опровержимость означает, что если формула имеет контр-модель, противоречие, даваемое этой контр-моделью, сосредоточено на конечном куске ограниченной сложности. Класс формул-импликаций в этой логике, для которых посылка конечно выполнима, а заключение конечно опровержимо с фиксированной сложностью, является разрешимым классом, если существование соответствующей конечно-определимой модели разрешимо. В [] доказано, что существование модели фиксированной сложности разрешимо для замкнутых ЕОТЬ-формул. Доказательство теоремы о разрешимости существования модели ограниченной сложности для ЕОТЬ-формул представляет собой алгоритм, который по данной формуле С логики ЕОТЬ, строит формулу а{к,п) смешанной линейной теории вещественных и целых чисел. Формула (*(*,„) истинна тогда и только тогда, когда формула й имеет модель сложности (к,п). Смешанная теория сложения вещественных и целых чисел является разрешимой теорией [|, таким образом, общезначимость формулы С(*,п) разрешима. Так же можно заметить, что вещественные и целые переменные этой формулы не входят в одну и ту же атомарную формулу, а значит можно применить алгоритмы элиминации кванторов для теории Тарского [] и арифметики Пресбургера [] последовательно дня каждой связанной переменной. В работе приводится краткий обзор разрешающих процедур дня данных теорий. Оценки сложности таких алгоритмов для общего случая не достаточно эффективны для практического применения на длинных формулах, поэтому, учитывая, что полученная формула содержит только линейные полиномы, можно применять алгоритмы дня этого частного случая. Эти алгоритмы оказываются более успешными.