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

г

САНКТ-ПЕТЕРБУРГСКИЙ ГОСУДАРСТВЕННЫЙ УНИВЕРСИТЕТ

на правах рукописи

Прокофьева Евгения Юрьевна

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

05.13.17 - теоретические основы информатики

АВТОРЕФЕРАТ диссертации на соискание ученой степени кандидата физико-математических наук

Санкт-Петербург - 2004

Работа выполнена на кафедре информатики математико-механического факультета Санкт-Петербургского государственного университета и в лаборатории алгоритмизации, сложности и логики университета Париж XII - Валь де Марн

Научные руководители: доктор физико-математических наук,

профессор Косовский Николай Кириллович, доктор, профессор Бокье Даниэль Официальные оппоненты: доктор физико-математических наук,

профессор Братчиков Игорь Леонидович кандидат физико-математических наук Ярославский Владимир Валерьевич Ведущая организация: Санкт-Петербургский институт

информатики и автоматизации РАН

Защита состоится "¿3 " 200У г. в Н час. на заседании

диссертационного совета Д.212.232.51 по защите диссертаций на соискание ученой степени доктора наук при Санкт-Петербургском государственном университете по адресу: 198504, Санкт-Петербург, Старый Петергоф, Университетский просп., 28, Математико-механи-ческий факультет.

С диссертацией можно ознакомиться в Научной библиотеке им.М.Горького Санкт-Петербургского государственного университета по адресу: 199034, Санкт-Петербург, Университетская наб., 7/9.

Автореферат разослан " " НЛ&ф/ 200^ г.

Ученый секретарь диссерационного совета, доктор физ.-мат. наук,

профессор Мартыненко Б.К.

vmx

$£9/И

Общая характеристика работы

Актуальность темы. Процесс создания любого программного обеспечения включает в себя фазу спецификации требований к программному продукту, фазу спецификации системы (алгоритма), фазу разработки (получение из формальных спецификаций системы исполняемого кода) и фазу валидации (обоснование того, что полученный программный продукт удовлетворяет начальным требованиям). Существует два общеизвестных метода валидации программного обеспечения: тестирование и верификация. Первый, наиболее часто используемый, состоит в тестировании (запуске) программы на конечном, множестве входных данных и анализе того, удовлетворяет ли результат (выходные данные) требованиям. Второй метод состоит в построении докаг затсльства того, что спецификации алгоритма удовлетворяют спецификациям требований, т.е. для всех допустимых входных данных алгоритм заканчивает работу и результат удовлетворяет требованиям. С математической точки зрения только верификация является доказательным методом.

С ростом использования программных систем в повседневной жизни возрастает необходимость разработки эффективных методов автоматической верификации программного обеспечения.

Цели работы

1. Реализация прототипа системы компьютерной верификации параметрических алгоритмов реального времени, основанной на ГОТЬ-методе.

2. Апробация этой системы на верификации некоторых существующих систем и протоколов с временными ограниче-

3. Разработка модификаций FOTL-метода, расширяющих класс проблем, для которых компьютерная верисЬикация является успешной.

Методы исследования. В диссертации для верификации систем реального времени применяется метод, основанный на временной логике первого порядка (First Order Timed Logic,

ниями.

FOTL) и называемый в диссертации FOTL-методом. Основная идея метода заключается в сведении проблемы верификации алгоритма к проверке общезначимости формулы некоторой временной логики первого порядка. Если удается доказать принадлежность этой формулы к разрешимому подклассу, то общезнаг чимость исходной формулы эквивалентна общезначимости формулы смешанной теории вещественных и целых чисел с раздельными переменными. Для проверки последнего используются алгоритмы элиминации кванторов.

Автором составлен пакет программ, реализующий FOTL-метод, с использованием систем компьютерной алгебры Reduce и QepcadB. Проведены эксперименты с реализациями алгоритмов элиминации кванторов в различных системах компьютерной алгебры для использования в разрабатываемой системе. Экспериментально продемонстрирована необходимость улучшения метода, так как на длинных формулах элиминация кванторов не может быть завершена из-за недостатка памяти или времени. Разработаны и реализованы модификации основного алгоритма FOTL-метода, сводящие задачи верификации к формулам с меньшим числом связанных переменных. С применением разработанного пакета программ доказана корректность двух систем реального времени, считающихся стандартными для тестирования систем автоматической верификации.

Научная новизна. Разработан прототип системы компьютерной верификации алгоритмов, использующих линейное время. Эта система позволяет описывать задачи верификации для систем с параметрами, как вещественными, например, временными параметрами системы, так и целыми, например, количеством взаимодействующих процессов. Верификация в предложенной системе не зависит от конкретных значений этих параметров.

Разработанные модификации FOTL-метода значительно расширяют круг задач, для которых компьютерная верификация является успешной.

С помощью разработанного пакета программ реализована компьютерная верификация двух систем реального времени: обобщенной задачи о железнодорожном переезде и протокола выбора лидера из двух конфликтующих процессов стандарта IEEE 1394. Кроме того, что названные системы имеют конкретные практиче-

ские приложения, они считаются эталонами для сравнения различных систем автоматической верификации алгоритмов. Впервые рассматриваемые задачи проанализированы во всей полноте, т.е. доказательство учитывает все параметры. Для протокола выбора лидера стандарта IEEE 1394 получены необходимые и достаточные условия, которым должны удовлетворять его параг метры для обеспечения корректности. Данные условия синтезированы, а не проверены, как в предшествующих работах, системой компьютерной верификации.

Практическая ценность. Разработанная система может быть использована для компьютерной верификации ряда алгоритмов, например, в системах реального времени с параметрами.

Апробация работы. Основные результаты работы докладывались на городском семинаре по программированию в Институте Информатики и Автоматизации РАН (Санкт-Петербург, 2000), VI международной конференции по компьютерной алгебре и ее приложениям "International Conference On Application Of Computer Algebra, IMACS АСА 2000" (Санкт-Петербург, 2000), Vil международной конференции "Региональная информатика -2000" (Санкт-Петербург, 2000), IV молодежной научной школе по дискретной математике и ее приложениям (Москва, 2000), V молодежной научной школе по дискретной математике и ее приложениям (Пенза, 2001), УШ международной конференции по компьютерной алгебре и ее приложениям "International Conference On Application Of Computer Algebra, АСА 2002" (Volos, Greece,

2002), IX международной конференции "Региональная информатика 2002" (Санкт-Петербург, 2002), III "Workshop on Automated Verification of Critical Systems, AVoCS 2003" (Southampton, UK,

2003), на семинаре кафедры Информатики математико-механиче-ского факультета СПбГУ (Санкт-Петербург, 2003), Х-ой международной конференции "Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2004" (Barselona, Spain, 2004).

Публикации. По теме диссертации опубликовано 7 работ [17].

Структура и объем работы. Диссертация состоит из шести глав и списка литературы. Основной текст диссертации занимает 99 страниц машинописного текста. Библиография содержит 75 наименований.

Содержание работы

Во введении рассматриваются различные методологии компьютерной верификации программ, описываются основные этапы РОТЬ-метода, обосновываются его преимущества и дается краткий обзор содержания работы.

Логический подход к проблеме верификации систем реального времени, основанный на временной логике первого порядка с непрерывным временем (РОТЬ), был предложен Веагщшег и ЯНзвепко в [ВЭ02] . Идея логического подхода заключается в описании спецификаций алгоритма и требований в виде формул некоторой алгоритмически разрешимой теории, что позволяет свести проблему верификации к проверке общезначимости логической формулы выбранной теории. Логика ГОТЬ является неразрешимой, но содержит разрешимые классы формул, позволяющие описывать проблемы верификации для систем контроля, обладающих некоторыми "конечными" свойствами.

Во второй главе рассматриваются синтаксис и семантика логик ГОТЬ, один из разрешимых подклассов этих логик, подробно описывается РОТЬ-метод и связанные с ним теоретические понятия и результаты.

Логики РОТЬ являются расширением теории сложения вещественных чисел конечными абстрактными сортами и временными функциями. Сигнатура логик РОТЬ состоит из конечного множества сортов и функциональных символов. Для фиксированной сигнатуры понятие терма и формулы определяется классическим для предикатной логики первого порядка образом. Вводятся понятия копечной интерпретаций и ее сложности.

Рассматривается разрешимый класс формул, введенный в [В802], который моделирует некоторые "конечные" свойства систем контроля. Эти "конечные" свойства сформулированы в терминах интерпретаций формул и названы конечной выполнимостью и конечной опровержимостъю. Конечная выполнимость формулы F означает, что каждый "конечный кусок" произвольной модели формулы Р может быть расширен до конечной модели Р. Конечная опровержимость означает, что если формула

имеет контр-модель, противоречие, даваемое этой контр-моделыо, сосредоточено на конечном куске ограниченной сложности. Существование контр-модели для формул-импликаций, посылка которых конечно-выполнима, а заключение конечно-опровержимо, эквивалентно существованию конечной модели.

В [BS02] доказано, что существование конечной модели фиксированной сложности разрешимо для замкнутых FOTL-формул. Доказательство представляет собой алгоритм, который по данной формуле G логики FOTL, строит формулу G(k,n) смешанной линейной теории вещественных и целых чисел с раздельными переменными. Формула G(k,n) истинна тогда и только тогда, когда формула G имеет модель сложности (к, п). Общезначимость G(k,n) может быть проверена последовательным применением алгоритмов элиминации кванторов для теории сложения вещественных чисел [Таг51] и для теории сложения целых чисел [РгеЗО] последовательно для каждой связанной переменной. Оценки сложности таких алгоритмов для общего случая достаточно неэффективны для практического применения на длинных формулах, поэтому, учитывая, что полученная формула содержит только линейные полиномы, можно применять алгоритмы для частного случая. Эти алгоритмы имеют более эффективные оценки сложности.

Как язык формальных спецификаций временных алгоритмов в FOTL-методе выбран частный случай машин абстрактных состояний Гуревича (ASM), называемых простыми временными абстрактными машинами Гуревича (timed basic ASM), и достаг точных для спецификации большого ряда контроллеров реального времени.

Простой временной абстрактной машиной Гуревича называг ется тройка вида (W, Init, Prog), где W - сигнатура, Init -замкнутая формула, описывающая начальное состояние, Prog -блок-программа, содержащая инструкции вида "If guard Then set of assignments Endlf", исполняемые одновременно и мгновенно.

Определение семантики таких машин может быть сделано различными способами, эквивалентными с физической точки зрения, но формально различными. В данной работе приводиться краткий обзор результатов из [BS02, BCS00] и описывается набор схем аксиом, конъюнкция которых представляет собой FOTL-формулу, описывающую множество запусков конкретной временной ASM.

В FOTL-методе можно выделить четыре основных этапа. Первый состоит в формализации спецификаций алгоритма и требований к его функционированию, второй - в трансляции полученной машины Гуревича в FOTL-формулу и доказательстве принадлежности формулы, описывающей проблему верификации, разрешимому подклассу. Третий этап заключается в применении алгоритма элиминации функциональных символов к формуле -г {$Aig —Фде9), где ФА1д~ FOTL-спецификация алгоритма и Фдед -FOTL-спецификация требований. Преобразованная формула истинна тогда и только тогда, когда исходная формула имеет конечную контр-модель. На четвертом этапе к полученной формуле применяются алгоритмы элиминации кванторов для 1 решения вопроса о ее противоречивости.

Реализация данного метода и его тестирование на примерах, использующих ASM, содержащие не более двух правил, показало невозможность завершения последнего этапа при существующих реализациях методов элиминации кванторов1 за 10-12 часов. Для расширения границ практической применимости данного метода разработаны шесть модификаций алгоритма элиминации функциональных символов.

Третья глава посвящена описанию разработанных автором диссертации модификаций алгоритма элиминации функциональных символов. Приводятся различные способы получения формулы G(yt,n), содержащей меньшее число связанных переменных, что расширяет границы эффективной применимости алгоритмов элиминации кванторов.

Основной алгоритм элиминации функциональных символов, или преобразование FOTL-формулы G в формулу теории сложения вещественных и целых чисел G(k,n)> описан для языка формул, атомы которых имеют вид f(X) -< z, где / функцио- <

нальный символ (предопределенный или абстрактный), X-список переменных или констант, г - переменная или константа. Для приведения формул к формулам требуемого вида в [BS02] '

приводится эквивалентное преобразование, вводящее в формулу новые связанные переменные.

1. Эксперименты проводились на компьютерах с процессором UltraSparc II (6dbits) 440mgh с памятью IG и процессором UltraSparc III (64bits) (2x)900mgh с памятью 4G. Вычисления, превосходящие 12 часов, прерывались.

Первая модификация алгоритма, предлагаемая в диссертации, состоит в обосновании того, что указанное преобразование достаточно применять лишь для атомов вида Р(.../(...<?...)...), где f -абстрактный функциональный символ и в терм, не являющийся переменной или константой. Таким образом из рассматриваемого изначально языка исключаются все термы с вложенными функциями, когда внешняя функция является абстрактной. Приводятся формулы преобразования формулы G в формулу G[k,n) для расширенного языка. Данный вариант алгоритма, уменьшая число связанных переменных, в некоторых случаях увеличивает число атомарных формул, но из компьютерных экспериментов сделан вывод, что элиминация кванторов более эффективна для формул, получаемых при использовании данной модификации.

Вторая модификация FOTL-метода состоит в изменении описания искомой модели. Формула G(k,n) содержит для каждого абстрактного функционального символа / список переменных, описывающих разбиение Т на п промежутков для к классов разбиения абстрактных сортов. Изначально не накладывается никаких ограничений на вид этих промежутков, поэтому для кодирования разбиения вводится п — 1 переменная типа Т для обозначения границ промежутков и п — 1 переменная типа Bool для кодирования принадлежности границ промежутков. Например, формула ti < i,+i Л Ьг = О Л bi+i = 1 описывает открытый промежуток (ti, tl+1). В рассматриваемой семантике ASM доказаны следующие свойства о виде промежутков для моделей формулы, описывающих ее запуски. Внутренние функции (функции, вычисляемые машиной) имеют значения, постоянные на промежутках вида (£г, i,+ i]. Таким образом, отпадает необходимость введения булевских переменных для внутренних функций, уменьшая тем самым число связанных переменных на (тг — 1) • Мк ■ s, где (к, п) - сложность искомой модели, М - число абстрактных сортов в сигнатуре логики, s - число внутренних абстрактных функциональных символов в сигнатуре логики. Число атомарных формул также уменьшается.

Третья модификация FOTL-метода состоит в рассмотрении конечных свойств для строгих конечных интерпретаций. Идея строгой (А;, п) интерпретации состоит в рассмотрении разбиения каждого из М конечных сортов на к подклассов, и для каждого из Мк подкласса разбиения Т на п промежутков одинакового для всех абстрактных символов. Тогда число переменных, описыва-

ющих разбиение, равно (п - 1) • Мк . Но эта модификация FOTL-метода не всегда уменьшает число связанных переменных. Пусть формула принадлежит разрешимому классу VERIF(k, п), тогда существует строгий разрешимый класс VERIFatrong{k'п'), которому принадлежит эта формула и к' ^ к An' ^ п. Таким образом, для первого класса и описания разбиения Т и значений функций вводится ((fc - 1) • М + (п - 1) • Мк + п • Мк) ■ а переменных, а для второго класса число переменных равно (к' — 1) • М + (п' — 1) • Мк' + п' ■ Мк' • 8. Какой из двух классов целесообразнее использовать зависит от значений этих двух выражений (какое из них меньше, тот класс и следует применять).

Четвертая модификация FOTL-метода состоит в рассмотрении конечных свойств для ступенчатых конечных интерпретаций. Исходя из алгоритма построения всюду определенного запуска ASM, возможно сделать выводы о максимальной сложности интерпретаций внутренних функций. Пусть рассматриваемая проблема принадлежит разрешимому классу VERIF{k, п). Если будет доказано, что для любой модели М интерпретация внутренней функции / является конечной и ее сложность не превосходит (к/, rij), где kf ^ к, nf ^ п, то в формуле G(k,n) можно использовать для / интерпретацию сложности (kf,n/).

Две последние модификации FOTL-метода можно обобщить следующим образом. Пусть для любой модели М формулы, описывающей запуски, можно разделить множество внутренних функций на р классов таких, что сужение М. на г-й класс является строгой конечной интерпретацией сложности (fa, пг). В этом случае анализ ASM позволяет выделить строгие подклассы и описывать формулу G(k,n) с меньшим числом переменных.

Последняя модификация касается частных случаев логик FOTL, в которых в сигнатуре отсутствует равенство для <

абстрактных сортов. В этом случае при построении формулы G(k,n) можно ограничиться только вещественными переменными. Можно предположить, что каждый из к классов эквивалентности содержит ровно один элемент, а, значит, мощность интерпретации каждого абстрактного сорта равна А:, и в процедуре построения формулы G(fc,n) кванторы всеобщности заменяются конъюнкцией по всем значениям абстрактной переменной от 1 до к, а кванторы существования - дизъюнкцией. Такое преобразование, несомненно, увеличивает число атомарных формул, но позволяет

ограничиться только вещественными переменными. Такой подход оказывается более результативным, так как существующие реализации алгоритма элиминации кванторов для целых чисел требуют приведения формулы к дизъюнктивно-нормальной форме (ДНФ). На больших формулах существующие реализации алгоритма приведения к ДНФ или не заканчивают работу из-за недостатка памяти, или время, затраченное на вычисления ДНФ для элиминации только одного квантора по целой переменной, в десятки раз превосходит время вычисления задачи в целом.

Четвертая глава посвящена описанию прототипа реализуемой системы верификации алгоритмов. В данной системе используется транслятор ASM2F0TL, реализованный T.Crolard [BCS00] для генерации аксиом, описывающих множество запусков ASM. Для элиминации кванторов и символьных преобразований формул в систему интегрированы различные средства символьных вычислений. Проводится анализ реализаций метода элиминации кванторов в пакетах компьютерной алгебры Qepcad, QepcadB, Mathematica и Redlog (один из пакетов системы Reduce) и выполненных автором реализаций [3, 6] для линейного случая теории Тарского и арифметики Пресбургера. Целесообразность использования пакета Redlog в разрабатываемой системе обосновывается тем, что алгоритм элиминации кванторов, лежащий в основе функций пакета Redlog, разработан для формул, содержащих полиномы степени не выше второй, тогда как остальные пакеты основываются на алгоритме, использующем алгебраическую цилиндрическую декомпозицию и применимом к произвольным формулам. Верхняя оценка сложности первого алгоритма оказывается лучше такой же оценки общего алгоритма в случае, когда формула содержит большое число свободных переменных. В системе, разработанной автором, все рассматриваемые формулы имеют степень не выше первой, поэтому применение для элиминации вещественных кванторов пакета Redlog является обоснованным.

Однако при использовании Redlog результатом элиминации кванторов являются громоздкие формулы, очевидно упрощаемые. Алгоритмы упрощения формул, реализованные в Redlog, не дают успешных результатов. Для приведения результата к виду, достаточно легко воспринимаемому человеком, используются функции упрощения бескванторных формул системы QepcadB.

Так как формулы, содержащие целые переменные, имеют специальный вид, то для элиминации кванторов реализован алгоритм для данного частного случая [2].

Алгоритм элиминации функциональных символов [1], функции ввода/вывода, функции лексического и синтаксического анализа входных данных, обмена данных между основным приложением и используемой системой компьютерной алгебры, функции генерации исполняемых скриптов для систем Reduce и QepcadB, библиотека функций, позволяющая запускать отдельные части вычислений на удаленной платформе, входят в состав модуля F0TL2REDUCE и реализованы на языке программирования С++.

Пятая и шестая главы содержат описания апробации разработанной системы на верификации двух систем контроля реального времени [4, 5, 7]. Выбор этих систем обоснован тем, что каждая из них является своеобразным эталоном (benchmark) для систем автоматической верификации программ. Предложенные модификации FOTL-метода позволяет описывать и анализировать указанные проблемы во всей их общности, учитывая параметризацию этих систем. Описанные модификации, разработанные при анализе этих задач, приводят к формулам, для которых компьютерная элиминация кванторов оказалась успешной.

В пятой главе демонстрируется эффективность описанного метода на примере обобщенной проблемы железнодорожного переезда (Generalized Railroad Crossing Problem, GECP) [НМ96]. Проблема GRCP рассматривается во всей ее общности. Во-первых. количество путей и все временные значения являются параметрами, во-вторых, требования записываются на языке FOTL-формул фактически без изменений и упрощений.

В начале 1лавы приводится неформальное описание контроллера, управляющего шлагбаумом на железнодорожном переезде, условий на функционирование окружения и требований, определяющих корректность функционирования контроллера. Спецификации требований ч окружения записываются в виде FOTL-формул Фде, и Ф tmv соответственно. Спецификация контроллера - это машина Гурсвича, которая транслируется в FOTL-формулу, описывающую множество всех ее возможные запусков (Фдип8).

Для доказательства того, что формула (Фяиш) Л Фв„„) Фде9 принадлежит разрешимому классу логики FOTL, доказана строгая конечная опровержимость Фяед и строгая конечная выполнимость Ф Rune Л Ф.

Заключительная часть пятой главы приводит результаты компьютерной верификации описанной модели.

Шестая глава содержит спецификацию и верификацию протокола выбора лидера из двух конфликтующих процессов (Root Contention Protocol, RCP). Рассматриваемый протокол является частью стандарта IEEE 1394 |[InsOO], который специфицирует высокоскоростную шину для передачи данных между мультимедиа устройствами. Корректность работы протокола критическим образом зависит от выбора значений временных параметров.

Протокол моделируется посредством ASM, требования - в виде FOTL-формул. Все запуски ASM, моделирующей один цикл протокола, имеют сложность не более 3, поэтому всякая контрмодель формулы Флип$ —¥ Фяе?, является интерпретацией сложности не более 3.

Формула Фдыпв —> Ф Fteq содержит свободные переменные, являющиеся параметрами протокола. Цель верификации - получение ограничений на эти параметры, являющиеся необходимым и достаточным условием для выполнения утверждения "один из процессов будет выбран лидером и только один". В результате верификации были получены формулы, подтверждающие требования стандарта. Данная работа является первой, в которой формулы были полностью синтезированы системой.

Результаты экспериментов доступны на web-сайте лаборатории LACL http://www.univ-parisl2.fr/lacl/ на личной страничке автора диссертации.

Основные результаты

• Разработан прототип системы компьютерной верификации временных алгоритмов основанной на FOTL-методе.

• Разработаны и реализованы шесть модификаций FOTL-метода.

• Выполнена верификация обобщенной задачи о железнодорожном переезде.

• Выполнена верификация протокола выбора лидера из двух конкурирующих процессов стандарта IEEE 1394.

Литература

[BCSOO] D. Beauquier, Т. Crolard, and A. Slissenko. A predicate logic framework for mechanical verification of real-time Gurevich Abstract State Machines: A case study with PVS. Technical Report 00-25, University Paris 12, Department of Informatics, 2000. Available at http://www.imiv-parisl2.fr/lacl/.

[bs02] D. Beauquier and A. Slissenko. A first order logic for specification of timed algorithms: Basic properties and a decidable class. Annals of Pure and Applied Logic, 113:13-52, 2002.

[hm96] C. Heitmeyer and D. Mandrioli, editors. Formal Methods ¡or RealTime Computing, volume б of Trends in Software. John Wiley & Sons, 1996. Series Editor: B. Krishnamurthy.

[InsOO] Institute of electrical and electronic engineers. IEEE Standart for a High Performace Sertal Bits - Amenedement 1. Std lS94a-2000, June 2000.

[РгеЗО] M. Presburger. Uber de Vollständigkeit eines gewissen systems der arithmetik ganzer zahlen, in welchen, die addition als einzige operation hervortritt. In Sprawozdanie z I Kongresu metematykow slowinskich, Warszawa 1929, pages 92-101, Warsaw, 1930.

|Tar61] A. Tarski. A decision method of elementary algebra and geometry. Berkely: University of California Press, 1951.

Публикации автора по теме диссертации

[1] Д. Бокье, Е. Прокофьева Реализация основного этапа алгоритма проверки существования модели заданной сложности для формул некоторой временной логики. Труды V-й молодежной научной школе по дискретной математике и ее приложениям, Пенза, Россия, 2001.

[2] Д. Бокье, Е. Прокофьева Применение метода элиминации кванторов в задачах анализа алгоритмов. Региональная Информатика (РИ-2002), Санкт-Петербург, Россия, 2002.

[3] Н.К. Косовский, Е.Ю. Прокофьева Реализация алюритма разрешимости теории вещественного сложения. Региональная Информатика (РИ-2000), Санкт-Петербург, Россия, 2000.

[4] D. Beauquier, Т. Crolard and Е. Prokofieva. Automatic verification of real time systems: A case study. In Third Workshop on Automated Verification of Critical Systems (AVoCS'2003), Technical Report of the University of Southampton, pages 98-108, Southampton, UK, April 2003.

[5] D. Beauquier and E. Prokofieva. A logical framework for an automatic verification of ieee 1394a root contention protocol In 8th International Conference on Applications of Computer Algebra (АСА 2002), pages 2223, Volos, Greece, June 2002.

[6] E. Prokofleva. A program of solvability of linear equality and inequality systems with parameters. In 6th IMACS International Conference on Applications of Computer Algebra (IMACS ACA 2000), page 62, Saint-Petersburg, Russia, June 2000.

[7] D. Beauquier, T. Crolard and E. Prokofleva. Automatic parametric verification of a root contention protocol based on abstract state machines and first order timed logic. In Kurt Jensen and Andreas Podelski, editors, Tools and Algorithms for the Construction and Analysis of Systems, 10th International Conference, TACAS 2004, volume 2988 of Lecture Notes in Computer Science, pages 372-387. Springer, 2004.

Подписано к печати 1 2004 г. Формат бумаги 60X84 1/16. Бумага офсетная. Печать ризографическая. Объем 1 усл. п. л. Тираж 100 экз Заказ 3401. Отпечатано в отделе оперативной полиграфии НИИХ СПбГУ с оригинал-макета заказчика. 198504, Санкт-Петербург, Старый Петергоф, Университетский пр , 26.

№-1624

РНБ Русский фонд

2005-4 48638

1 Введение

1.1 Общая характеристика работы

1.2 Формальные методы верификации

1.3 Содержание диссертационной работы

2 Временная логика первого порядка FOTL

2.1 Синтаксис и семантика FOTL

2.2 Разрешимость конечно-определяемых свойств

2.3 FOTL-метод.

3 Модификации FOTL-метода

3.1 Расширение языка рассматриваемых формул.

3.2 Свойства внутренних и внешних функций

3.3 Строгие конечные интерпретации.

3.4 Ступенчатые конечные интерпретации

3.5 Ступенчато-строгие интерпретации.

3.6 Отсутствие равенства для абстрактных сортов.

4 Реализация FOTL-метода

4.1 Автоматическая генерация FOTL-формулы, описывающей запуски

4.2 Компьютерные реализации методов элиминации кванторов

4.3 Прототип системы компьютерной верификации систем реального времени

5 Обобщенная задача о железнодорожном переезде

5.1 Постановка задачи GRCP

5.2 Моделизация GRCP.

5.3 Разрешимый класс FOTL для верификации GRCP

5.4 Компьютерная верификация GRCP.

6 IEEE 1394 Root Contention Protocol.

6.1 Неформальное описание IEEE 1394 RCP.

6.2 Моделирование протокола при помощи ASM

6.3 Требования корректности на языке FOTL

6.4 Разрешимость верификации корректности RCP

6.5 Компьютерная верификация протокола.

Актуальность темы. Процесс создания любого программного обеспечения как привило включает в себя фазу спецификации требований к программному продукту, фазу спецификации системы (алгоритма), фазу разработки (получение из формальных спецификаций системы исполняемого кода) и фазу валидации (обоснование того, что полученный программный продукт удовлетворяет начальным требованиям). Существует два общеизвестных метода валидации программного обеспечения: тестирование и верификация. Первый, наиболее часто используемый, состоит в тестировании (запуске) программы на конечном множестве входных данных и анализе того, удовлетворяет ли результат (выходные данные) требованиям. Второй метод состоит в построении доказательства того, что спецификации алгоритма удовлетворяют спецификациям требований, т.е. для всех допустимых входных данных алгоритм заканчивает работу, и результат удовлетворяет требованиям. С математической точки зрения только верификация является доказательным методом.

С ростом использования программных систем в повседневной жизни возрастает необходимость разработки эффективных методов автоматической верификации программного обеспечения.

Цели работы

1. Реализация прототипа системы компьютерной верификации параметрических алгоритмов реального времени, основанной на FOTL-методе.

2. Апробация этой системы на верификации некоторых существующих систем и протоколов с временными ограничениями.

3. Разработка модификаций FOTL-метода, расширяющих класс проблем, для которых компьютерная верификация является успешной.

Методы исследования. В диссертации для верификации систем реального времени применяется метод, основанный на временной логике первого порядка (First Order Timed Logic, FOTL) и называемый в диссертации FOTL-методом. Основная идея метода заключается в сведении проблемы верификации алгоритма к проверке общезначимости формулы некоторой временной логики первого порядка. Если удается доказать принадлежность этой формулы к разрешимому подклассу, то общезначимость исходной формулы эквивалентна общезначимости формулы смешанной теории сложения вещественных и целых чисел с раздельными переменными. Для проверки последнего используются алгоритмы элиминации кванторов.

Автором разработан пакет программ, реализующий FOTL-метод, с использованием систем компьютерной алгебры Reduce [59] и QepcadB [58]. Проведены эксперименты с различными реализациями алгоритмов элиминации кванторов для использования в разрабатываемой системе. Экспериментально показана необходимость улучшения метода, так как на длинных формулах он не может быть завершен из-за недостатка памяти или времени при применении методов элиминации кванторов. Разработаны и реализованы модификации основного алгоритма FOTL-метода, сводящие задачи верификации к формулам с меньшим числом связанных переменных. С применением разработанного пакета программ доказана корректность двух систем реального времени.

Научная новизна. Разработан прототип системы компьютерной верификации алгоритмов, использующих линейное время. Эта система позволяет описывать задачи верификации для систем с параметрами, как вещественными, например, временными параметрами системы, так и целыми, например, количеством взаимодействующих процессов. Верификация в предложенной системе не зависит от конкретных значений этих параметров.

Разработанные модификации значительно расширяют круг задач, для которых компьютерная верификация является успешной.

С помощью разработанного пакета программ реализована компьютерная верификация двух систем реального времени: обобщенной задачи о железнодорожном переезде и протокола выбора лидера из двух конфликтующих процессов стандарта IEEE 1394. Кроме того, что названные системы имеют конкретные практические приложения, они так же являются примерами для сравнения различных систем автоматической верификации алгоритмов. Впервые рассматриваемые задачи проанализированы во всей полноте, т.е. доказательство учитывает все параметры. Получены необходимые и достаточные условия, которым должны удовлетворять параметры этих систем для обеспечения их корректности.

Практическая ценность. Разработанная система может быть использована для компьютерной верификации ряда алгоритмов, например, в системах реального времени с параметрами.

1. Д. Бокье, Е. Прокофьева. Реализация основного этапа алгоритма проверки существования модели заданной сложности для формул некоторой временной логики. 1. Труды V-й молодежной научной школе по дискретной математике и её приложениям, Пенза, Россия, 2001.

2. Д. Бокье, Е. Прокофьева. Применение метода элиминации кванторов в задачах анализа алгоритмов. In Региональная Информатика (РИ-2002), Санкт-Петербург, Россия, 2002.

3. Н.К. Косовский, Е.Ю. Прокофьева. Реализация алгоритма разрешимости теории вещественного сложения. In Региональная Информатика (РИ-2000), Санкт-Петербург, Россия, 2000.

4. Э. Энгелер. Метаматематика элементарной математики. Москва "Мир", 1987. перевод с немецкого 31] Г.Е. Минца под редакцией А.О. Слисенко.

5. М. Archer and С. Heitmeyer. Mechanical verification of timed automata: A case study. Technical Report 5546-98-8180, University Paris-12, Department of Informatics, Naval Reserach Laboratory, Washington, 1998. NRL Memorandum Report.

6. G. Bandini, R. L. Spelberg, R. С. H. de Rooij, and H. Toetenel. Application of parametric model checking the root contention protocol. In Sixth Annual Conference of the Advanced School for Computing and Imaging(ASCI 2000), Lommel, Belgium, June 2000.

7. D. Beauquier and E. Prokofieva. A logical framework for an automatic verification of ieee 1394a root contention protocol. In 8th International Conference on Applications of Computer Algebra (АСА 2002), pages 22-23, Volos, Greece, June 2002.

8. D. Beauquier and A. Slissenko. Decidable classes of the verification problem in a timed predicate logic. Fundamentals (or Foundations) of Computation Theory, 12, 1999.

9. D. Beauquier and A. Slissenko. A first order logic for specification of timed algorithms: Basic properties and a decidable class. Annals of Pure and Applied Logic, 113:13-52, 2002.

10. D. Beauquier and A. Slissenko. Periodicity based decidable classes in a first order timed logic. Technical Report 2004-04, University Paris 12, Department of Informatics, 2004. Available at http://www.univ-parisl2.fr/lacl/.

11. L. Berman. The complexity of logical theories. Theoretical Computer Science, 11:71— 77, 1991.

12. N. Bjorner, Z. Manna, H. Sipma, and T. Uribe. Deductive verification of real-time systems using STeP. Technical Report STAN-CS-TR-98-1616, Computer Sci. Dept., Stanford Univ., December 1998. Submitted to Elsevier Science.

13. C. Brown. Implementing Q.E. by CAD to be compleye, correct, fast and "good". In 8th International Conference on Applications of Computer Algebra (АСА 2002), page 23, Volos,Greece, June 2002. University of Thessaly.

14. Christopher W. Brown. An overview of QEPCAD B: a tool for real quantifier elimination and formula simplification. Journal of Japan Society for Symbolic and Algebraic Computation, 10(l):13-22, 2003.

15. Christopher W. Brown. QEPCAD B: a program for computing with semi-algebraic sets using cads. SIGSAM Bull., 37(4):97-108, 2003.

16. J. Buchi. Weak second-order arithmetic and finite automata. Z.Math. Logik Grundlagen Math., 6:66-92, 1960.

17. F. Budan de Boislaurent. Nouvelle methode pour la resolution des equation numeriques d'un degre quelconque,1807. Paris, 1822. 2nd edition.

18. A. Bundy and I. Green. A comparison of decision procedures in presburger arithmetic, November 1999. The Pennsylvania State University CiteSeer Archives.

19. G. Collins. Quantifier elimination for the elementary theory of real closed fields by cylindrical algebraic decomposition. Lecture Notes in Computer Science, 33:134-183, 1975.

20. G. Collins and H. Hong. Partial cylindrical algebraic decomposition for quantifier elimination. Journal of Symbolic Computation, 12(3), Septembre 1991.

21. A. Collomb-Annichini and M. Sighireanu. Parametrized reachability analysis of the IEEE 1394 Root Contention Protocol using TReX. In Proceedings of the Workshop on Real-Time Tools (RT-TOOLS'2001), 2001.

22. D. Cooper. Theorem proving in arithmetic without multiplication. Machine Intelligence, 7:91-99, 1972.

23. R. Descartes. La geometrie livre iii. OEuvres des Descartes, 6:442-485, 1973.

24. A. Dolzmann and T. Sturm. Redlog user manual. Technical Report MIP-9905, Universitat Passau, April 1999.

25. E. Engeler. Metamathematik der Elementarmathematik. Hochschultext. Springer-Verlag, Berlin Heidelberg New York, 1983.

26. M. Fischer and M. Rabin. Super-exponential complexity of presburger arithmetic. In Symp. on appl. Math., volume 7 of SIAM-AMS Proc., pages 27-41, 1974.

27. J.-B. Fourier. Analyse des equation determinees. F. Didot, Paris, 1831.

28. V Ganesh, S. Berezin, and D. Dill. Deciding presburger arithmetic by model checking and comparisons with other methods. In FMCAD'02, 2002.

29. Y. Gurevich. Evolving algebra 1993: Lipari guide. In E. Borger, editor, Specification and Validation Methods, pages 9-93. Oxford University Press, 1995.

30. A. Hearn. REDUCE user's and contributed packages manual, version 3.7. Available from Konrad-Zuse-Zentrum Berlin, Germany, February 1999.

31. C. Heitmeyer, R. Jeffords, and B. Labaw. A benchmark for comparing different approaches for specifying and verifying real-time systems. In Proc. of the 10th IEEE Workshop on Real-Time Operating Systems and Software, New York. IEEE, 1993.

32. C. Heitmeyer and N. Lynch. The generalized railroad crossing: a case study in formal verification of real-time systems. In Proc. of Real-Time Systems Symp., San Juan, Puerto Rico. IEEE, 1994.

33. C. Heitmeyer and D. Mandrioli, editors. Formal Methods for Real-Time Computing, volume 5 of Trends in Software. John Wiley & Sons, 1996. Series Editor: B. Krishnamurthy.

34. L. Hodes. Solving problems by formula manipulation in logic and linear inequalities. In Proceedings of the 2nd International Joint Conference on Artificial Intelligence, pages 553-559, London, England, 1971. Imperial College.

35. T. Hune, J. Romijn, M. Stoelinga, and F. Vaandrager. Linear parametric model checking of timed automata. Journal of Logic and Algebraic Programming, 2002.

36. Institute of electrical and electronic engineers. IEEE Standart for a High Performace Serial Bus. Std 1394-1995, August 1995.

37. Institute of electrical and electronic engineers. IEEE Standart for a High Performace Serial Bus Amenedement 1. Std 1394a-2000, June 2000.

38. F. Klaedtke. On the automata size for presburger arithmetic. In 19th Annual IEEE Symposium on Logic in Computer Science (LICS'04), pages 110-119, Turku, Finland, July 2004. IEEE Computer Society Press.

39. Mathematica. Web-site: http://www.wolfram.com/products/mathematica/.

40. Microsoft Visual С++ 6.0 Introductory Edition. Wrox Press et Editions Eyrolles, 1999.2 p*n

41. D. Oppen. A 2 upper bound on the complexity of presburger arithmetic. Journal of Logic and Algebraic Programming, 1978.

42. M. Presburger. Uber de vollstandigkeit eines gewissen systems der arithmetik ganzer zahlen, in welchen, die addition als einzige operation hervortritt. In Sprawozdanie z I Kongresu metematykow slowinskich, Warszawa 1929, pages 92-101, Warsaw, 1930.

43. M. Presburger. On the completeness of a certain system of arithmetic of whole numbers in which addition occurs as the only operation. History and Philosophy of Logic, 12:225-233, 1991. (Translation of 52] by D. Jacquette).

44. E. Prokofieva. Expiriments with automatic verification of GRCP and IEEE 1394 RCP. Available at http://www.univ-parisl2.fr/lacl/prokofieva.

45. E. Prokofieva. A program of solvability of linear equality and inequality systems with parameters. In 6th IMACS International Conference on Applications of Computer Algebra (IMACS АСА 2000), page 62, Saint-Petersburg, Russia, June 2000.

46. W. Pugh. The omega test: a fast and practical integer programming algorithm for dependence analysis. Technical report, 1991.

47. Qepcad. Web-site: http://www.cs.usna.edu/ qepcad.

48. QepcadB. Web-site: http://www.cs.usna.edu/ qepcad/b/qepcad.html.

49. Reduce. Web-site: http://www.reduce-algebra.com/ and http://www.uni-koeln.de/reduce/.

50. A. Seidl. Cylindrical algebraic decomposition for real quantifier elimination within redlog. In 8th International Conference on Applications of Computer Algebra (АСА 2002), page 35, Volos,Greece, June 2002. University of Thessaly.

51. N. Shankar. Verification of real-time systems using PVS. In Proc. 5th International Computer Aided Verification Conference, pages 280-291, 1993.

52. D. Simons and M. Stoelinga. Mechanical verification of the IEEE 1394a root contention protocol using UppaaJ2k. Springer International Journal of Software Tools for Technology Transfer, pages 469-485, 2001.

53. T. Skolem. Uber einige stazfunktionen in der arithmetik. In Shifter utgitt av Det Norske Videnskaps-Akademi i Oslo, I. Matematiks naturvidenskapeling klasse, volume 7, pages 1-28, Oslo, 1931.

54. T. Skolem. Uber einige stazfunktionen in der arithmetik. In J. Fenstad, editor, Selected Works in Logic, pages 281-206. Universitetsforlaget, Oslo, 1970. Reprint of the article 63].

55. M. Stoelinga. Fun with FireWire: Experiments with verifying the IEEE 1394 Root Contention Protocol. In J.M.T. Romijn S. Maharaj, C. Shankland, editor, Formal Aspects of Computing, volume 14, page 9, 2002.

56. M. Stoelinga and F. Vaandrager. Root contention in IEEE 1394. In J.-P. Katoen, editor, Proceedings of the 5th AM AST Workshop on Real-Time and Probabilistic Systems (ARTS'99), pages 53-75, Bamberg, Germany, May 1999.

57. A. Strzebonski. Solving systems of strict polynomial inequalities. Journal of Symbolic Computation, 29:471-480, 2000.

58. J. Sturm. Memoire sur la resolution des equation numeriques. In Memoires presentes par divers Savant etrangers a I'Academie royale des sciences, section Sc. math, phys., pages 273-318, 1835.

59. A. Tarski. A decision method of elementary algebra and geometry. Technical report, RAND, Santa Monica, С A, 1948.

60. A. Tarski. A decision method of elementary algebra and geometry. Berkely: University of California Press, 1951.

61. H. Toetenel, R.L. Spelberg, and G. Bandini. Parametric verification of the IEEE 1394a root contention protocol using LPMC. In Seventh International Conference on Real-Time Systems and Applications (RTCSA'OO), Cheju Island, South Korea, December 2000.

62. V. Weispfenning. The complexity of linear problems in fields. Journal of Symbolic Computation, 5(l-2):3-27, February-April 1988.

63. V. Weispfenning. Quantifier elimination for real algebra the quadratic case and beyond. Applicable Algebra in Engineering Communication and Computing, 8(2):85-101, February 1997.

64. V. Weispfenning. Mixed real-integer linear quantifier elimination. In Proc. of the 1999 Int. Symp. on Symbolic and Algebraic Computations (ISSAC'99), pages 129-136. ACM Press, 1999