Содержание к диссертации
Введение
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
- Формальные методы верификации
- Разрешимость конечно-определяемых свойств
- Свойства внутренних и внешних функций
- Компьютерные реализации методов элиминации кванторов
Введение к работе
1.1 Общая характеристика работы
Актуальность темы. Процесс создания любого программного обеспечения как привило включает в себя фазу спецификации требований к программному продукту, фазу спецификации системы (алгоритма), фазу разработки (получение из формальных спецификаций системы исполняемого кода) и фазу валидации (обоснование того, что полученный программный продукт удовлетворяет начальным требованиям). Существует два общеизвестных метода валидации программного обеспечения: тестирование и верификация. Первый, наиболее часто используемый, состоит в тестировании (запуске) программы на конечном множестве входных данных и анализе того, удовлетворяет ли результат (выходные данные) требованиям. Второй метод состоит в построении доказательства того, что спецификации алгоритма удовлетворяют спецификациям требований, т.е. для всех допустимых входных данных алгоритм заканчивает работу, и результат удовлетворяет требованиям. С математической точки зрения только верификация является доказательным методом.
С ростом использования программных систем в повседневной жизни возрастает необходимость разработки эффективных методов автоматической верификации программного обеспечения.
Цели работы
1. Реализация прототипа системы компьютерной верификации параметрических алгоритмов реального времени, основанной на FOTL-методе.
2. Апробация этой системы на верификации некоторых существующих систем и протоколов с временными ограничениями.
3. Разработка модификаций FOTL-метода, расширяющих класс проблем, для которых компьютерная верификация является успешной.
Методы исследования. В диссертации для верификации систем реального времени применяется метод, основанный на временной логике первого порядка (First Order Timed Logic, FOTL) и называемый в диссертации FOTL-методом. Основная идея метода заключается в сведении проблемы верификации алгоритма к проверке общезначимости формулы некоторой вре менной логики первого порядка. Если удается доказать принадлежность этой формулы к разрешимому подклассу, то общезначимость исходной формулы эквивалентна общезначимости формулы смешанной теории сложения вещественных и целых чисел с раздельными переменными. Для проверки последнего используются алгоритмы элиминации кванторов.
Автором разработан пакет программ, реализующий FOTL-метод, с использованием систем компьютерной алгебры Reduce [59] и QepcadB [58]. Проведены эксперименты с различными реализациями алгоритмов элиминации кванторов для использования в разрабатываемой системе. Экспериментально показана необходимость улучшения метода, так как на длинных формулах он не может быть завершен из-за недостатка памяти или времени при применении методов элиминации кванторов. Разработаны и реализованы модификации основного алгоритма FOTL-метода, сводящие задачи верификации к формулам с меньшим числом связанных переменных. С применением разработанного пакета программ доказана корректность двух систем реального времени.
Научная новизна. Разработан прототип системы компьютерной верификации алгоритмов, использующих линейное время. Эта система позволяет описывать задачи верификации для систем с параметрами, как вещественными, например, временными параметрами системы, так и целыми, например, количеством взаимодействующих процессов. Верификация в предложенной системе не зависит от конкретных значений этих параметров.
Разработанные модификации значительно расширяют круг задач, для которых компьютерная верификация является успешной.
С помощью разработанного пакета программ реализована компьютерная верификация двух систем реального времени: обобщенной задачи о железнодорожном переезде и протокола выбора лидера из двух конфликтующих процессов стандарта IEEE 1394. Кроме того, что названные системы имеют конкретные практические приложения, они так же являются примерами для сравнения различных систем автоматической верификации алгоритмов. Впервые рассматриваемые задачи проанализированы во всей полноте, т.е. доказательство учитывает все параметры. Получены необходимые и достаточные условия, которым должны удовлетворять параметры этих систем для обеспечения их корректности.
Практическая ценность. Разработанная система может быть использована для компьютерной верификации ряда алгоритмов, например, в системах реального времени с параметрами.
1.2 Формальные методы верификации
Можно выделить два основных подхода к верификации систем, использующих время: модельный (model-based) и доказательный(ргоо/-Леогегса/ reasonig).
При модельно-теоретическом подходе, система, называемая verifier, проверяет удовлетворяют ли спецификации алгоритма, в виде какой-либо машины конечных состояний, требуемому свойству. В последнее время разработано большое число алгоритмов для такой верификации. Наиболее известный, называемый model chekers, использует машину конечных состояний, как спецификацию системы, и формулу некоторой временной логики, как спецификацию свойств, и проверяет выполнена ли формула в данной модели. Строится граф вычислений для представления всех возможных состояний, в которые может войти система, и в каждом из состояний проверяется указанной свойство.
Такие системы как SMV, TReX, HYTECH, LPMC, Uppaal и другие реализуют принципы model-cheking и параметрического model-cheking. Изначально model-cheking был разработан для машин с конечным множеством состояний. При введении времени и параметров в рассматриваемые алгоритмы, множество состояний становиться бесконечным. Для сложных и параметризованных моделей граф вычислений становится слишком большим, что накладывает ограничение на практическое применение данных методов. Для расширения их применимости разрабатываются различные походы для отсечения недостижимых состояний как в конечном, так и в бесконечном случае.
При доказательно-теоретическом, или логическом, подходе, строится теория о разрабатываемой системе в некоторой логике. Свойства системы описываются формулами этой теории и строится доказательство о выполнимости рассматриваемых свойств. Для автоматизации процесса доказательства используются такие средства автоматического доказательства теорем как HOL, PVS, LarchProver(LP), Coq и другие. Очень часто используемые теории являются неразрешимыми, поэтому указанные системы используют различные стратегии поиска доказательств, которые, к сожалению, не всегда являются успешными. Данные средства было бы точнее называть не системами автоматического доказательства, а "помощниками построения доказательств", так как часто от пользователя требуется "руководство" системой, когда не удается доказать поставленную цель. Поэтому процесс верификации при таком подходе не является полностью автоматическим.
Обзор конкретных реализаций указанных подходов может быть найден в [41].
В работе [14] Beauquier и Slissenko был предложен логический подход к проблеме верификации систем реального времени, основанный на временной логике первого порядка с непрерывным временем. В качестве языка формальных спецификаций алгоритмов выбран формализм простых временных абстрактных машин Гуревича (timed basic ASM), являющийся частным случаем абстрактных машин Гуревича, специально адаптированный для спецификаций систем реального времени с мгновенными действиями.
Идея логического подхода заключается в описании спецификаций алгоритма и требований в виде формул некоторой алгоритмически разрешимой теории, сводящих тем самым проблему верификации к проверке общезначимости логической формулы выбранной теории.
В [14] введена временная логика первого порядка (First Order Timed Logic, FOTL), позволяющая описать, с одной стороны, множество запусков простых временных ASM, с другой стороны, выражать требования к системе. Таким образом, верификация сводится к проверке общезначимости формулы в логике FOTL. Логика FOTL является неразрешимой, но содержит разрешимые классы формул, позволяющие описывать проблемы верификации для систем контроля, обладающих некоторыми "конечными" свойствами. Одним из таких классов является класс формул, для которых существование контрмодели формулы эквивалентно существованию "конечной" контр-модели, т.е. модели, определенной конечным набором значений заданной сложности.
В описанном методе верификации, называемом автором FOTL-методом, можно выделить четыре основных этапа. Первый состоит в формализации спецификаций алгоритма и требований к его функционированию и доказательстве принадлежности формулы, описывающей проблему верификации, одному из разрешимых классов. Второй этап заключается в трансляции полученной машины Гуревича в FOTL-формулу, описывающую множество всех возможных запусков машины. Третий этап представляет собой применение алгоритма элиминации функциональных символов к формуле - {Флід - - Req), где Флід- FOTL-спецификация алгоритма и ФЛе9 - FOTL-специфи-кация требований. Преобразованная формула истинна тогда и только тогда, когда исходная формула имеет конечную контр-модель. На четвертом этапе к полученной формуле применяются алгоритмы элиминации кванторов для решения вопроса о ее противоречивости. В тех случаях, когда рассматриваемая проблема верификации содержит параметры, соответствующая ей FOTL-формула содержит свободные переменные. Результатом применения алгоритмов элиминации кванторов на четвертом этапе является бескванторная формула от данных переменных, являющаяся необходимым и достаточным условием корректности алгоритма. В тех случаях, когда результат слишком длинный для восприятия человеком, в заключение могут быть применены алгоритмы символьных преобразований для приведения формулы к более простому виду.
Реализация данного метода и его тестирование даже на маленьких примерах показало невозможность успешного завершения четвертого этапа при существующих реализациях методов элиминации кванторов в ночное время1. Это объясняется тем, что большинство алгоритмов, лежащих в основе FOTL-метода, имеют экспоненциальные и супер-экспоненциальные нижние оценки сложности. Для больших исходных данных такие оценки не позволяют получить эффективно работающие алгоритмы. Для повышения эффективности FOTL-метода разработаны шесть модификаций алгоритма элиминации функциональных символов. Применение модифицированного FOTL-метода дало успешные результаты при компьютерной верификации обобщенной проблемы железнодорожного перекрестка и протокола выбора лидера из двух конкурирующих процессов стандарта IEEE 1394.
1. Эксперименты проводились на компьютерах с процессором UltraSparc II (64bits) 440mgh с памятью 1G и процессором UltraSparc III (64bits) (2x)900mgh с памятью 4G. Все вычисления, превосходящие 600-700 минут, прерывались.
1.3 Содержание диссертационной работы
В главе 2 рассматриваются временные логики первого порядка FOTL, предложенные D.Beauquier и A.Slissenko [13, 14].
FOTL являются расширением теории сложения вещественных чисел конечными абстрактными сортами и временными функциями. Для фиксированной сигнатуры логик FOTL понятие терма и формулы определяется классическим для предикатной логики первого порядка образом. Понятия интерпретации, модели, выполнимости, общезначимости и опровержимости аналогичны соответствующим понятиям предикатной логики первого порядка.
Логики FOTL позволяют выражать спецификации требований, которые обычно даются на естественном языке. Если они выражены не достаточно полно и четко, попытка формализации позволяет выявить слабые места, которые требуют доработки.
В [13, 14] авторы изучают разрешимые классы FOTL-логик. Разрешимый класс проблем верификации, исследуемый в этой работе, описан в [14] и моделирует некоторые "конечные" свойства систем контроля. Эти "конечные" свойства сформулированы в терминах интерпретаций формул и названы конечной выполнимостью и конечной опровержимостъю. Конечная выполнимость формулы F означает, что каждый "конечный кусок" произвольной модели формулы F может быть расширен до "конечно-определимой" модели F. Конечная опровержимость означает, что если формула имеет контр-модель, противоречие, даваемое этой контр-моделью, сосредоточено на конечном куске ограниченной сложности. Класс формул-импликаций в этой логике, для которых посылка конечно выполнима, а заключение конечно опровержимо с фиксированной сложностью, является разрешимым классом, если существование соответствующей конечно-определимой модели разрешимо. В [14] доказано, что существование модели фиксированной сложности разрешимо для замкнутых FOTL-формул. Доказательство теоремы о разрешимости существования модели ограниченной сложности для FOTL-формул представляет собой алгоритм, который по данной формуле G логики FOTL, строит формулу G(k,n) смешанной линейной теории вещественных и целых чисел. Формула G(k,n) истинна тогда и только тогда, когда формула G имеет модель сложности (к, п). Смешанная теория сложения вещественных и целых чисел является разрешимой теорией [75], таким образом, общезначимость формулы G(k,n) разрешима. Так же можно заметить, что вещественные и целые переменные этой формулы не входят в одну и ту же атомарную формулу, а значит можно применить алгоритмы элиминации кванторов для теории Тарского [71] и арифметики Пресбургера [52] последовательно для каждой связанной переменной. В работе приводится краткий обзор разрешающих процедур для данных теорий. Оценки сложности таких алгоритмов для общего случая не достаточно эффективны для практического применения на длинных формулах, поэтому, учитывая, что полученная формула содержит только линейные полиномы, можно применять алгоритмы для этого частного случая. Эти алгоритмы оказываются более успешными.
Данная глава так же содержит описание выбранного языка формальных спецификаций временных алгоритмов. В тех случаях, когда анализ алгоритма явно затрагивает время, становятся актуальными такие вопросы, как длительность действий и синхронизация различных действий. Мы ограничиваемся конструкциями вида "If guard Then set of assigments Endlf ", которые могут быть организованы в блоки. В одном блоке все Ifhen опера-горы выполняются одновременно и мгновенно. Как язык описания такого рода алгоритмов выбран частный случай машин абстрактных состояний Гуревича (ASM), называемые простыми временными абстрактными машинами Гуревича (timed basic ASM), и достаточными для спецификации большого ряда контроллеров реального времени.
Простой временной абстрактной машиной Гуревича (timed basic ASM) является тройка вида (W, Init, Prog), где W является сигнатурой, Init -замкнутая формула, описывающая начальное состояние, Prog - блок-программа, содержащая инструкции вида "If guard Then set of assigments Endlf ", исполняемые одновременно и мгновенно.
Сорта, переменные и функции определяются подобно этим понятиям в FOTL, отличие состоит в том, что время (Т) не может быть аргументом функции. Функции классифицируются как статические и динамические, абстрактные и предопределенные.
Динамические функции классифицируются как внешние и внутренние. Внешние функции не изменяются машиной, внутренние же, напротив, вычисляются машиной и являются абстрактными. Предопределенные статические функции имеют одну фиксированную интерпретацию для всех t Т. Интерпретации динамических предопределенных функций зависят от времени, но не зависят от функционирования машины.
Определение семантики таких машин может быть сделано различными способами, эквивалентными с физической точки зрения, но формально различными. В [14, 9] рассматривается алгоритм построения интерпретации внутренних функций на основе заданных интерпретаций внешних функций и начальных данных, и описывается набор схем аксиом, конъюнкция которых представляет собой FOTL-формулу, описывающую множество запусков конкретной временной ASM. В данной работе приводиться краткий обзор этих результатов и алгоритмов, которые используются в дальнейшем для доказательств модификаций FOTL-метода.
Глава 3 посвящена описанию разработанных автором диссертации модификаций алгоритма элиминации функциональных символов. Приводятся различные способы получения формулы G(k,n), содержащей меньшее число связанных переменных, что расширяет границы эффективной применимости алгоритмов элиминации кванторов.
Основной алгоритм элиминации функциональных символов, или преобразование FOTL-формулы G в формулу теории сложения вещественных и целых чисел G(k,n), описан для языка формул, атомы которых имеют вид f(X) - z, где /- функциональный символ (предопределенный или абстрактный), Х- список переменных или констант, z - переменная или константа. Для приведения формул к формулам требуемого вида в [14] приво дится эквивалентное преобразование, вводящее в формулу новые связанные переменные.
В диссертации предлагается первая модификация алгоритма, которая состоит в обосновании того, что указанное преобразование достаточно применять лишь для атомов вида Р(.../(...в.)), где / - абстрактный функциональный символ и в - терм, не являющийся переменной или константой. Таким образом из рассматриваемого изначально языка исключаются все термы с вложенными функциями, когда внешняя функция является абстрактной. Приводятся формулы преобразования формулы G в формулу G(jfc,„) для расширенного языка. Отметим, что данный вариант алгоритма, уменьшая число связанных переменных, в некоторых случаях увеличивает число атомарных формул, но из компьютерных экспериментов сделан вывод, что элиминация кванторов более эффективна для формул, получаемых при использовании данной модификации.
Вторая модификация FOTL-метода состоит в изменении описания искомой модели. Формула G(k,n) содержит для каждого абстрактного функционального символа / список переменных, описывающих разбиение Т на п промежутков для к классов разбиения абстрактных сортов. Изначально не накладывается никаких ограничений на вид этих промежутков, поэтому для кодирования разбиения вводится п — \ переменных типа Т, обозначающих границы промежутков и п — 1 переменных типа Bool, кодирующих принадлежность границ промежутков. Например, формула U U+i Л Ь{ — О Л frj+i = 1 описывает открытый промежуток (;, j+i). В рассматриваемой семантике timed basic ASM доказаны следующие свойства о виде промежутков для моделей формулы, описывающих ее запуски. Внутренние функции (функции, вычисляемые машиной) имеют значения, постоянные на промежутках вида (ti, U+i]. Таким образом, отпадает необходимость введения булевских переменных для внутренних функций, уменьшая тем самым число связанных переменных на (п — 1) • Мк s, где (к, п) - сложность искомой модели, М -число абстрактных сортов в сигнатуре логики, s - число внутренних абстрактных функциональных символов в сигнатуре логики. Число атомарных формул также уменьшается.
Третья модификация FOTL-метода состоит в рассмотрении конечных свойств для строгих конечных интерпретаций. Идея строгой (к, п) интерпретации состоит в рассмотрении разбиения каждого из М конечных сортов на к подклассов, и для каждого из Мк подкласса разбиения Т на п промежутков одинакового для всех абстрактных символов. Тогда число переменных, описывающих разбиение, равно (п — 1) • Мк . Но эта модификация FOTL-метода не всегда эффективна. Пусть формула принадлежит разрешимому классу VERIF(k, п), тогда существует строгий разрешимый класс VERIFstrong{k , п ), которому принадлежит эта формула и к к Л п п. Таким образом, для первого класса и описания разбиения Т и значений функций вводится ((к — 1) • М + (п — 1) • Мк + п Мк) s переменных, а для второго класса число переменных равно (к - 1) • М + (п - 1) Мк + п Мк s. Какой из двух классов целесообразнее использовать зависит от значений этих двух выражений (какое из них меньше, тот класс и применять).
Четвертая модификация FOTL-метода состоит в рассмотрении конечных свойств для ступенчатых конечных интерпретаций. Исходя из алгоритма построения всюду определенного запуска ASM, возможно сделать выводы о максимальной сложности интерпретаций внутренних функций. Пусть рассматриваемая проблема принадлежит разрешимому классу VERIF(k, п). Если мы докажем, что для любой модели Лі интерпретация внутренней функции / является конечной и ее сложность не превосходит (kf, Uf), где kf к, rij п, то в формуле G(k,n) можно использовать для / интерпретацию сложности (kf,nj).
Две последние модификации FOTL-метода можно обобщить следующим образом. Пусть для любой модели Л4 формулы, описывающей запуски, можно разделить множество внутренних функций на р классов, таких, что сужение АІ на г-й класс является строгой конечной интерпретацией сложности (кі, ПІ). В этом случае анализ ASM позволяет выделить строгие подклассы и описывать формулу G(k,n) с меньшим числом переменных.
Последняя модификация касается частных случаев логик FOTL, в которых в сигнатуре отсутствует равенство для абстрактных сортов. В этом случае при построении формулы G(k,n) можно ограничиться только вещественными переменными. Можно предположить, что каждый из к классов эквивалентности содержит ровно один элемент, а, значит, мощность интерпретации каждого абстрактного сорта равна к, и в процедуре построения формулы G(k,n) кванторы всеобщности заменяются конъюнкцией по всем значениям абстрактной переменной от 1 до к, а кванторы существования - дизъюнкцией. Такое преобразование, несомненно, увеличивает число атомарных формул, но позволяет ограничиться только вещественными переменными. Такой подход оказывается более эффективным, так как существующие реализации алгоритма элиминации кванторов для целых чисел требуют приведения формулы к дизъюнктивной нормальной форме. А на больших формулах существующие реализации алгоритма приведения к ДНФ или не заканчивают работу из-за недостатка памяти, или время, затраченное на вычисления ДНФ для элиминации только одного квантора по целой переменной, в десятки раз превосходит время вычисления задачи в целом.
Глава 3 посвящена описанию прототипа реализуемой системы верификации алгоритмов. Вначале приводится краткое описание транслятора ASM2F0TL, реализованного Т. Crolard для генерации аксиом, описывающих множество запусков ASM. Далее проводится анализ реализаций метода элиминации кванторов в таких пакетах компьютерной алгебры как Qepcad, QepcadB, Mathematica и Redlog (один из пакетов системы Reduce) и выполненных автором реализаций для линейного случая теории Тарского и арифметики Пресбургера, опубликованных в [3, 55]. Он показал целесообразность использования пакета Redlog в разрабатываемой системе. Это обосновывается тем, что алгоритм элиминации кванторов, лежащий в основе функций пакета Redlog, разработан для формул, содержащих полиномы степени не выше второй, тогда как остальные пакеты основываются на алгоритме, использующем алгебраическую цилиндрическую декомпозицию (CAD), применимом к произвольным формулам. Как плата за общность этого алгоритма является его меньшая эффективность в линейном случае. В нашей системе все рассматриваемые формулы имеют степень не выше первой, поэтому применение для элиминации вещественных кванторов Redlog является обоснованным.
Однако при использовании Redlog результатом элиминации кванторов являются громоздкие формулы, очевидно упрощаемые. Алгоритмы упрощения формул, реализованные в Redlog, не дают успешных результатов. Для приведения результата к виду, достаточно легко воспринимаемому человеком, используются функции упрощения бескванторных формул системы QepcadB.
Так как формулы, содержащие целые переменные, имеют специальный вид, то для элиминации кванторов в этом случае предлагается специальный алгоритм и его реализация, которая является одной из функций системы [2].
Входными данными для системы верификации являются спецификация алгоритма как ASM, требований в виде FOTL-формул и параметр разрешимого класса - сложность (к, п). Результат - бескванторная формула от параметров системы, если таковые были, являющаяся необходимым и достаточным условием правильности алгоритма, в противном случае, результат -тождественно истинная или тождественно ложная формула.
Основные функции, такие как алгоритм элиминации функциональных символов (см. [1]), функции ввода-вывода, функции лексического и синтаксического анализа входных данных, обмен данных между основным приложением и используемой системой компьютерной алгебры, генерация скриптов для выполнения элиминации кванторов, реализованы на языке программирования C++ и являются частью модуля F0TL2REDUCE. Разработаны классы, позволяющие запускать отдельные части вычислений на удаленной платформе.
Главы 5 и б содержат описания апробации разработанной системы на верификации двух систем контроля реального времени [10, 7, 8]. Выбор этих систем обоснован тем, что каждая из них является своеобразным эталоном для сравнения систем автоматической верификации программ. Результаты верификации являются успешными. Предложенные модификации FOTL-метода позволяют описывать и анализировать указанные проблемы во всей их общности, учитывая параметризацию этих систем. Описанные модификации, фактически разработанные при анализе этих задач, приводят к формулам, компьютерная элиминация кванторов для которых оказалась успешной.
В главе 5 демонстрируется эффективность описанного метода на примере обобщенной проблемы железнодорожного перекрестка {Generalized Railroad Crossing Problem, GRCP). Проблема GRCP рассматривается во всей ее общности. Во-первых, количество путей и все временные условия являются параметрами, во-вторых, требования записываются на языке FOTL-формул фактически без изменений.
В начале главы приводится неформальное описание контроллера, условий на функционирование окружения и требований, определяющих корректность функционирования контроллера. Спецификации требований и окружения записываются в виде FOTL-формул (Фде? и Фя„„ соответственно). Специфи кация контроллера - это ASM, которая транслируется в FOTL-формулу, описывающую множество всех ее возможных запусков (Фдиги).
Для применения описанного метода необходимо доказать, что формула (Фяиги Л ФЕПЬ) — Req принадлежит разрешимому классу логики FOTL, и найти параметры этого класса. Поэтому доказывается строгая конечная ОПрОВержиМОСТЬ Фдед И конечная ВЫПОЛНИМОСТЬ Фд„п« Л Фягіи Заключительная часть главы приводит результаты компьютерной верификации описанной модели.
Глава 6 содержит спецификацию и верификацию протокола выбора лидера из двух конфликтующих процессов (Root Contention Protocol, RCP). Рассматриваемый протокол является частью стандарта IEEE 1394, который специфицирует высокоскоростную шину для передачи данных между мультимедиа устройствами. Корректность работы протокола критическим образом зависит от выбора значений временных параметров и использования механизма случайного выбора.
Протокол моделируется посредством ASM, требования - в виде FOTL-формул. Все запуски ASM, моделирующей один цикл протокола, имеют сложность не более 3, поэтому всякая контр-модель формулы Фдиг18 — ФReq, является интерпретацией сложности не более 3.
Формула Фдипз - Фде?, содержит свободные переменные, являющиеся параметрами протокола. Цель верификации - получить ограничение на эти параметры, являющееся необходимым и достаточным условием для выполнения утверждения "один из процессов будет выбран лидером и только один". В результате верификации были получены формулы, подтверждающие требования стандарта.
Формальные методы верификации
Можно выделить два основных подхода к верификации систем, использующих время: модельный (model-based) и доказательный(ргоо/-Леогегса/ reasonig). При модельно-теоретическом подходе, система, называемая verifier, проверяет удовлетворяют ли спецификации алгоритма, в виде какой-либо машины конечных состояний, требуемому свойству. В последнее время разработано большое число алгоритмов для такой верификации. Наиболее известный, называемый model chekers, использует машину конечных состояний, как спецификацию системы, и формулу некоторой временной логики, как спецификацию свойств, и проверяет выполнена ли формула в данной модели. Строится граф вычислений для представления всех возможных состояний, в которые может войти система, и в каждом из состояний проверяется указанной свойство.
Такие системы как SMV, TReX, HYTECH, LPMC, Uppaal и другие реализуют принципы model-cheking и параметрического model-cheking. Изначально model-cheking был разработан для машин с конечным множеством состояний. При введении времени и параметров в рассматриваемые алгоритмы, множество состояний становиться бесконечным. Для сложных и параметризованных моделей граф вычислений становится слишком большим, что накладывает ограничение на практическое применение данных методов. Для расширения их применимости разрабатываются различные походы для отсечения недостижимых состояний как в конечном, так и в бесконечном случае.
При доказательно-теоретическом, или логическом, подходе, строится теория о разрабатываемой системе в некоторой логике. Свойства системы описываются формулами этой теории и строится доказательство о выполнимости рассматриваемых свойств. Для автоматизации процесса доказательства используются такие средства автоматического доказательства теорем как HOL, PVS, LarchProver(LP), Coq и другие. Очень часто используемые теории являются неразрешимыми, поэтому указанные системы используют различные стратегии поиска доказательств, которые, к сожалению, не всегда являются успешными. Данные средства было бы точнее называть не системами автоматического доказательства, а "помощниками построения доказательств", так как часто от пользователя требуется "руководство" системой, когда не удается доказать поставленную цель. Поэтому процесс верификации при таком подходе не является полностью автоматическим. Обзор конкретных реализаций указанных подходов может быть найден в [41].
В работе [14] Beauquier и Slissenko был предложен логический подход к проблеме верификации систем реального времени, основанный на временной логике первого порядка с непрерывным временем. В качестве языка формальных спецификаций алгоритмов выбран формализм простых временных абстрактных машин Гуревича (timed basic ASM), являющийся частным случаем абстрактных машин Гуревича, специально адаптированный для спецификаций систем реального времени с мгновенными действиями.
Идея логического подхода заключается в описании спецификаций алгоритма и требований в виде формул некоторой алгоритмически разрешимой теории, сводящих тем самым проблему верификации к проверке общезначимости логической формулы выбранной теории.
В [14] введена временная логика первого порядка (First Order Timed Logic, FOTL), позволяющая описать, с одной стороны, множество запусков простых временных ASM, с другой стороны, выражать требования к системе. Таким образом, верификация сводится к проверке общезначимости формулы в логике FOTL. Логика FOTL является неразрешимой, но содержит разрешимые классы формул, позволяющие описывать проблемы верификации для систем контроля, обладающих некоторыми "конечными" свойствами. Одним из таких классов является класс формул, для которых существование контрмодели формулы эквивалентно существованию "конечной" контр-модели, т.е. модели, определенной конечным набором значений заданной сложности.
В описанном методе верификации, называемом автором FOTL-методом, можно выделить четыре основных этапа. Первый состоит в формализации спецификаций алгоритма и требований к его функционированию и доказательстве принадлежности формулы, описывающей проблему верификации, одному из разрешимых классов. Второй этап заключается в трансляции полученной машины Гуревича в FOTL-формулу, описывающую множество всех возможных запусков машины. Третий этап представляет собой применение алгоритма элиминации функциональных символов к формуле - {Флід - - Req), где Флід- FOTL-спецификация алгоритма и ФЛе9 - FOTL-специфи-кация требований. Преобразованная формула истинна тогда и только тогда, когда исходная формула имеет конечную контр-модель. На четвертом этапе к полученной формуле применяются алгоритмы элиминации кванторов для решения вопроса о ее противоречивости. В тех случаях, когда рассматриваемая проблема верификации содержит параметры, соответствующая ей FOTL-формула содержит свободные переменные. Результатом применения алгоритмов элиминации кванторов на четвертом этапе является бескванторная формула от данных переменных, являющаяся необходимым и достаточным условием корректности алгоритма. В тех случаях, когда результат слишком длинный для восприятия человеком, в заключение могут быть применены алгоритмы символьных преобразований для приведения формулы к более простому виду.
Реализация данного метода и его тестирование даже на маленьких примерах показало невозможность успешного завершения четвертого этапа при существующих реализациях методов элиминации кванторов в ночное время1. Это объясняется тем, что большинство алгоритмов, лежащих в основе FOTL-метода, имеют экспоненциальные и супер-экспоненциальные нижние оценки сложности. Для больших исходных данных такие оценки не позволяют получить эффективно работающие алгоритмы. Для повышения эффективности FOTL-метода разработаны шесть модификаций алгоритма элиминации функциональных символов. Применение модифицированного FOTL-метода дало успешные результаты при компьютерной верификации обобщенной проблемы железнодорожного перекрестка и протокола выбора лидера из двух конкурирующих процессов стандарта IEEE 1394.
Разрешимость конечно-определяемых свойств
Тот факт, что теория, расширением которой является логика FOTL, является разрешимой теорией, позволяет выделить разрешимые классы проблем верификации, представляющие практический интерес. FOTL-метод основан на одном из таких классов. Основное "физическое" свойство этого класса состоит в возможности описания систем контроля в терминах некоторого конечного множества значений, размерность которого ограничена некоторой фиксированной константой. Сужение языка рассматриваемых формул
Для упрощения описания алгоритмов и доказательств теорем в [14] приводится список эквивалентных преобразований формул, сужающих язык, используемый для построения формул в логиках первого порядка. В новом языке атомарными формулами являются выражения вида:
Так же приводится преобразование сигнатуры логики, результатом которой является сигнатура, не содержащая сортов, являющихся объединением других сортов и содержащая абстрактные функциональные символы вида /: Т х Х\ х ... х Xs— Z, где ХІ абстрактный сорт неизвестной мощности. Конечные интерпретации
Так как рассматриваемые интерпретации абстрактных сортов являются конечными множествами, не теряя общности, можно полагать, что абстрактные сорта интерпретируются начальными отрезками натурального ряда. Введем следующие обозначения.
Для каждого абстрактного функционального символа /: Т х X — Z посредством Uf обозначим множество термов Щх„ которые будут использоваться для описания значения функции fx- на некотором интервале Т- Возможные типы термов зависят от сорта Z. Если Z является абстрактным сортом, то Щх, является константой z интерпретации Z . Если Z = Bool, то U}x, является булевской константой, и если Z = R или Z — Т, то U)xt это терм вида t + у, где некоторая константа из множества Ну С Q (фиксированного для данной интерпретации), t - временная переменная и у - вещественная константа.
В примерах, рассматриваемых в главах 5 и 6, Е/ является одно-элементным множеством, содержащим 1 или 0.
В приведенных ниже определениях в записях вида /: Т х X - Z под X понимается прямое произведение атомических абстрактных сортов Х\ х ... х Xs, при s 1 (аналогично для X и х ).
Рассмотрим / и / интерпретации функционального символа /: Т х X — Z. Пусть множества У и У , интерпретирующие X, совпадают и для каждого элемента из У подмножества Т, на которых определены / и / , так же совпадают и для одинаковых значений аргументов tux значения / и / равны. С формальной точки зрения такие интерпретации считаются различными, если они имеют различные Т-поддержки для интерпретации некоторой одной и той же абстрактной переменной х . Такие интерпретации будем называть эквивалентными.
Сложность конечной интерпретации.
Идея сложности, определенная ниже, основана на следующем свойстве интерпретаций: интерпретация функционального символа для данной интерпретации сортов, как бы велика ни была ее размерность, может быть факторизо-вана на малое число классов эквивалентности. Разрешимость существования конечной (к, п) — модели
Доказательство теоремы о разрешимости существования модели заданной сложности представляет собой алгоритм, который по данной FOTL-формуле G и сложности (к, п) искомой модели строит формулу G(k,n), не содержащую абстрактных функциональных символов, которая истинна тогда и только тогда, когда формула G имеет модель сложности (к,п). Получаемая формула является формулой разрешимой теории (таким образом строилась FOTL), и для определения ее общезначимости или противоречивости могут быть применены алгоритмы элиминации кванторов[71, 75].
Если исходная формула G является замкнутой, то формула G ,n) Т&К же является замкнутой, и в результате процедуры элиминации кванторов получается тождественно истинная либо тождественно ложная формула. Если формула G содержала свободные переменные, то формула G(k,n) содержит те же свободные переменные, и результатом элиминации кванторов является бескванторная формула, зависящая от этих свободных переменных. Истинность этой формулы является необходимым и достаточным условием существования модели сложности (к,п) исходной формулы G.
Приведенная ниже теорема доказана Beauquier и Slissenko в [14]. Ниже процесс построения формулы G(fc,n) приводится во всех деталях (порой опущенных в [14]). Такая подробность, может быть и не необходимая для доказательства, потребовалась для компьютерной реализации алгоритма. Так же при доказательстве модификаций FOTL-метода в дальнейшем мы будем ссылаться на эту теорему и использовать введенные ниже обозначения.
Конечная интерпретация сложности (к, п) представляет собой интерпретацию абстрактных сортов и (всюдуопределенную) интерпретацию абстрактных функциональных символов для этих сортов. Абстрактные сорта интерпретируются начальными отрезками натурального ряда, и, следовательно, их интерпретация характеризуется натуральным числом. Интерпретация каждого функционального символа /: Т х X — Z характеризуется разбиением X на ks классов эквивалентности, как описано в определении 2.12, и для каждого класса эквивалентности / определяется в терминах разбиения Тна п интервалов и параметров, определяющих значения / на каждом интервале разбиения.
Пусть X = Х\ х ... х Xs. Разбиение X описывается fc-интервальными разбиениями множеств Х. Интерпретацией сорта ХІ является множество X = {1, 2, ...МІ), и -интервальное разбиение этого множества представляется натуральными переменными тп\, тп12,..., тпгк_1, где 1 тп\ тг2 ... т\-\ Mj.
Для каждого из к3 классов эквивалентности, для описания модели необходимо п — 1 временных t\, ..., tn_i и п — 1 булевских Ь\, ..., Ьп-і переменных, представляющих разбиение Т на п непустых интервалов. Булевские переменные определяют принадлежность границ интервала следующим образом, если Ь{ = 0, то U принадлежит левому интервалу, т.е. Ii = (tj-i ti] и Jj+i = (U, ti+i), где ( Є {(, [} и ) Є {), ]}, если Ьг = 1, то ti принадлежит правому интервалу, т.е. h — (U-i, U) и /j+i = [U, tj+i). Следующие неравенства определяют ограничения на их значения
Свойства внутренних и внешних функций
Использование вместе различных специализированных средств компьютерных аналитических вычислений, позволяет расширить границы практической применимости и решать задачи, которые не под силу только одной системе.
Теоретические результаты не дают больших надежд на существование эффективной практической разрешающей процедуры для арифметики Пресбургера в общем случае. В [34] приводиться обзор существующих реализаций двух типов разрешающих процедур, основанных на автоматном подходе и на линейном программировании для целых чисел. Указанные средства работают лишь на бескванторном фрагменте арифметики Пресбургера, но могут быть расширены до теории в целом. Авторы данной работы утверждают, что процедура элиминации кванторов Купера является слишком неэффективной, что бы соперничать с двумя другими подходами. Напротив, результаты представленные в [23] показывают, что использование метода Купера в тандеме с некоторой эвристикой, быстро отсекающей тождественно ложные формулы, дает лучшую практическую эффективность, чем частичный метод Хода [42].
В отличии от теории Тарского, несмотря на большое число работ и экспериментов по реализации и использованию разрешающей процедуры для арифметики Пресбургера, ни в одном из широкоизвестных пакетов компьютерной алгебры (например Mathematica, Redlog, MatCad и др.) эта процедура не реализована.
Существует система OMEGA [56], специально направленная на решение задач в целых числах. В данной системе реализовано расширение алгоритма линейного программирования Фурье-Моцкина до целых чисел. Использование данного алгоритма для элиминации кванторов на произвольных формулах требует начального приведения формулы к дизъюнктивно-нормальной форме, что может привести (и обычно приводит) к экспоненциальному росту числа атомарных формул.
В FOTL-методе формулы арифметики Пресбургера являются линейными неравенствами вида х - у, где - { , = }. Для этого частного случая автором был реализован алгоритм элиминации кванторов. С использованием функций системы Redlog, реализация данного алгоритма не потребовала больших усилий, так как такие трудоемкие алгоритмы как приведение формул к дизъюнктивно нормальной форме, приведение формул к антипре-фексной нормальной форме и др. уже реализованы в Redlog. Был так же использован интерфейс с системой, написанный для вещественной элиминации кванторов.
Проблема в использовании данного алгоритма возникает при вычислении дизъюнктивно нормальной формы. В некоторых случаях время, затраченное на вычисление ДНФ для элиминации одного лишь квантора, превосходило время, затраченное на вычисление задачи в целом. В таком случае, если в сигнатуре логики отсутствует равенство для абстрактных сортов, может быть применена последняя модификация FOTL-метода, в которой получаемая формула содержит только вещественные переменные. Однако "хорошая" практическая реализация метода элиминации кванторов для арифметики Пресбургера остается важным элементом для FOTL-метода. Например, при рассмотрении классов периодических интерпретаций невозможно обойтись без такой процедуры [15].
Прототип системы компьютерной верификации, основанной на FOTL-методе, разрабатывался средствами языка программирования C++ [50] для Windows-платформ с использованием систем компьютерной алгебры Reduce [59], точнее ее пакета Redlog, и QepcadB [58]. Основной алгоритм FOTL-метода и его модификаций, реализован в модуле F0TL2REDUCE, кторый содержит примерно 10000 строк исполняемого кода.
Архитектура разработанного прототипа системы автоматической верификации соответствует этапам 1-4 FOTL-метода. Общая схема системы приведена на рис. 4.1.
Модуль F0TM2REDUCE начинает свою работу с лексического и синтаксического анализа данных (файлы .sng H.ftl). Лексический и синтаксический анализаторы были разработаны с использованием средств автоматической генерации лексических и синтаксических анализаторов Lex и Yacc.
Если лексический и синтаксический анализ прошел успешно, то к формуле, описывающей проблему верификации, может быть применен алгоритм элиминации функциональных символов.
Результатом элиминации функциональных символов является файл с расширением .ird (сокращение "input reduce"), содержащий скрипт, написанный на входном языке системы Redlog, представляющий собой запуск функций элиминации кванторов. Запуск системы Redlog производится автоматически из модуля F0TL2REDUCE. В зависимости от настроек системы, Redlog может быть запущен на удаленной платформе.
Если полученные результаты требуют упрощения, рекомендуется использовать систему Qepcad В (доступную только на платформах Unix), так как алгоритмы символьных преобразований системы Redlog не достаточно эффективны. Используя скрипт Reduce2Qepcad, результаты, полученные в Redlog, преобразовываются в набор команд, выполняющих упрощение формул в Qepcad В.
Основная часть реализации FOTL-метода и его модификаций содержится в классах модуля F0TL2REDUCE. Далее перечисляются основные классы (но далеко не все), реализующие этапы 1-4 FOTL-метода.
Пусть входными данными системы являются файлы ex.sgn, ex.ftl, ex_to_add.ftl и ex_to_prove.ftl. Первый файл содержит определения абстрактных сортов, переменных и функций и параметры разрешимого класса. Файл может содержать комментарии. Комментариями считаются все строки, начинающиеся с символа "//" Файл состоит из двух частей: описание сортов и определений функций. Каждая из этих частей начинается строкой "/Definition of Sorts:" и "/Definition of Functions:" соответственно. Внутри каждой части все непустые строки кроме комментариев понимаются как определение сорта или функции. Для сортов первый идентификатор понимается именем сорта, последующие именами переменных данного сорта. Полагается, что первые три сорта - это предопределенные сорта R, Т и Bool. Строки, содержащие описания функций, должны начинаться с идентификатора функции, далее идет номер сорта результата функции и затем список номеров соответствующих сортов параметров. На рисунке 4.2 представлен пример такого файла.
Компьютерные реализации методов элиминации кванторов
В данной главе речь идет о компьютерной реализации FOTL-метода и используемых в нем средствах, таких как трансляция абстрактных машины Гуревича в FOTL-формулы и разрешающие процедуры для теорий сложения вещественных и целых чисел. Приводится описание прототипа системы компьютерной верификации систем, основанной на FOTL-методе и его модификациях. Данная система реализована на языке программирования C++. Она содержит модули, осуществляющие интерфейс с системами компьютерной алгебры, средства которых используются для реализации различных частей алгоритма верификации.
Процесс построения FOTL-формулы, описывающей множество всюдуопреде-ленных запусков, впервые реализован в трансляторе, называемом ASM2PVC[9]. Он позволяет по входной ASM генерировать список аксиом, согласно теореме 2.3, в синтаксисе системы PVS[28]. В [9] приведено доказательство общезначимости формулы, описывающей верификацию свойства безопасности задачи о железнодорожном переезде, выполнено с помощью данной системы автоматического построения доказательств.
В реализации FOTL-метода используется новая версия транслятора ASM2F0TL[7], генерирующая аксиомы в синтаксисе логик первого порядка.
Транслятор состоит из парсера, модуля осуществляющего проверку типов, библиотеки функций, которые, собственно, и осуществляют трансляцию, и генератора, который создает выходной файл в соответствии с определенным абстрактным синтаксисом. Благодаря модульному проектированию транслятора, предусмотрена возможность расширения и изменения синтаксиса ASM, генерации дополнительных лемм и использования в дальнейшем других систем аналитических вычислений (отличных Reduce и PVS).
— Входной файл. Формальная грамматика входного файла, содержащего описание ASM, состоит из трех частей. Первая часть - сигнатура и, возможно, список статических и внутренних функций. Вторая часть представляет собой описание некоторых функций, предикатов и сигнатуру логических переменных. Третья честь содержит блок условных правил ASM.
— Абстрактный синтаксис. Абстрактный синтаксис соответствует конкретному синтаксису, определенному формальной грамматикой ASM. Заметим, что термы и формулы не различаются (т.е. формулы - это булевские термы) и, что ASM может быть параметризована.
— Проверка типов. На этом этапе осуществляется проверка того, что ни одна функция не объявлена как внутренняя и статическая одновременно, что правила ASM не изменяют значения внешних функций, и, наконец, проверяется типизация условий и присваиваний.
— Трансляция. Реализация транслятора близка к математическом определению, данному в теореме 2.3: набор аксиом генерируется для каждой схемы Ф ().
Многие авторы отмечают применимость разрешающих процедур арифметики Пресбургера и теории Тарского для автоматизации решения задач из различных областей информатики, математики, физики, механики, таких как автоматическое доказательство теорем, верификация программ и символьные математические вычисления. Данная работа является одним из таких примеров - последний шаг FOTL-метода состоит в применении разрешающих процедур к формулам указанных теорий для решения вопроса о выполнимости логической формулы, описывающей проблему верификации. Для обоих теорий существуют методы элиминации кванторов, являющиеся одним из типов разрешающих алгоритмов. При реализации прототипа системы компьютерной верификации по FOTL-методу был возможен выбор: самостоятельно реализовать алгоритмы элиминации кванторов как функции системы или использовать существующие реализации данных процедур в системах компьютерной алгебры.
Количество переменных и атомарных формул в формулах, получаемых на последнем этапе верификации, зависит от сложности верифицируемой системы, количества параметров и функций, и применимость FOTL-метода критически зависит от эффективности алгоритмов элиминации кванторов. Но все же целью данной работы являлась не реализация практически эффективных методов элиминации кванторов, а реализация практически эффективной системы верификации алгоритмов, поэтому работу, связанную с реализацией алгоритмов элиминации кванторов, хотелось минимизировать, по крайней мере, на начальном этапе, и, при возможности, использовать максимум существующего програмного кода.
Разработка систем компьютерной алгебры и символьных вычислений получила большое развитие в последние десятилетия. Это связано с быстро растущей мощностью вычислительных машин - алгоритмы, которые недавно казались абсолютно неприменимыми на практике из-за громоздких вычислений, в настоящее время исполняются за миллисекунды на обычном компьютере. Разработка и реализация разрешающих процедур, эффективно применимых на практике для теории Тарского и арифметики Пресбургера, является отдельной областью компьютерной алгебры, исследование которой проводится в десятке лабораторий и университетов мира. Казалось ответ очевиден: надо использовать существующие реализации, ведь автор, вряд ли сможет претендовать на то, что реализованный им алгоритм будет эффективнее, чем алгоритмы найденные, реализованные и постоянно оптимизируемые многими учеными и разработчиками. С другой стороны, формулы, получаемые в FOTL-методе, имеют особенную структуру и, возможно, для таких частных случаев существуют алгоритмы более эффективные, чем общие алгоритмы. В каждом из двух случаев, был сделан соответствующий выбор, казавшийся наименее трудоемкими и наиболее эффективный для поставленной цели на момент проведения компьютерных экспериментов.
Первой компьютерной реализацией метода элиминации кванторов для теории Тарского была реализация метода Коллинза Денисом Арноном в 1980. Результатом работы Хонга стала система Qepcad , первые версии которой стали доступны в начале 1990х [25, 57]. В 2002 году Кристофером Брауном [18, 20, 58] была представлена система QepcadB, расширяющая и улучшающая возможности системы Qepcad.
Другой широко известной реализацией метода элиминации кванторов является пакет Reglog, распространяемый как часть системы Reduce[37, 59]. В доступной сейчас версии Reglog[30] реализован первый метод Вейпсфе-нинга для линейных полиномов и ряд функций, позволяющих в некоторых случаях уменьшить степень формул.
В последнее время ведутся работы по интеграции метода элиминации кванторов, основанного на CAD, в системы компьютерной алгебры Methematica[67, 49] и Redlog[60]. В версии 4.0 пакета Mathematica элиминация кванторов была экспериментальной возможностью и доступна в полном объеме в последней, пятой версии. Реализация данного метода в Redlog пока еще недоступна.
В начале работы над диссертацией, автором был реализован метод элиминации кванторов для формул, содержащих полиномы первой степени [3, 55]. В основе реализованного алгоритма лежало доказательство обобщенной теоремы Штурма, приведенное в [4, 31]. Данное доказательство, используя свойства непрерывности полиномов и их производных, для формул вида Зх(а х b Л А(х)) и \/хА(х) строит бескванторные формулы, не содержащие переменную х. Используя стандартные преобразования, алгоритм расширен для произвольных формул. Реализация данного алгоритма выполнена как библиотека функций в системе Mathematica3.0 (в этой версии еще не существовало реализации алгоритма элиминации кванторов для алгебры Тарского). Системы компьютерных символьных вычислений оказываются очень удобными для реализации таких математических алгоритмов. Понятие полинома, производной, логической формулы первого порядка, вычисление различных нормальных форм уже интегрированы в среду программирования и остается реализовать непосредственно алгоритм, не отвлекаясь на технические детали. К сожалению, общность рассматриваемого алгоритма элиминации кванторов не лучшим образом сказывается на его эффективности, и компьютерные тесты проходят лишь на формулах, содержащих не более трех связанных переменных. Это связанно с тем, что алгоритм применяется рекурсивно для каждого квантора и происходит экспоненциальный рост числа атомарных формул.
