автореферат диссертации по информатике, вычислительной технике и управлению, 05.13.11, диссертация на тему:Верификация параметризованных моделей распределенных систем

Московский государственный университет имени М.В. Ломоносова Факультет вычислительной математики и кибернетики

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

Коннов Игорь Владимирович

ВЕРИФИКАЦИЯ ПАРАМЕТРИЗОВАННЫХ МОДЕЛЕЙ РАСПРЕДЕЛЁННЫХ СИСТЕМ

Специальность 05.13.11 — математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей

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

МОСКВА 2008

003450599

003450599

Работа выполнена на кафедре автоматизации систем вычислительных комплексов факультета вычислительной математики и кибернетики Московского государственного университета имени М.В. Ломоносова.

Защита состоится «28» ноября 2008 г. в 11:00 на заседании диссертационного совета Д 501.001.44 при Московском государственном университете имени М.В. Ломоносова по адресу: 119991, ГСП-1, Москва, Ленинские горы, МГУ, 2-ой учебный корпус, факультет вычислительной математики и кибернетики, аудитория 685.

С диссертацией можно ознакомиться в библиотеке факультета ВМиК МГУ имени М.В. Ломоносова, с текстом автореферата — на официальном сайте ВМиК МГУ имени М.В.Ломоносова: http://wre.ca .msu.su в разделе «Наука» — «Работа диссертационных советов» — «Д 501.001.44».

9 2

Автореферат разослан ' ^ » октября 2008 г. Ученый секретарь

диссертационного совета Д 501.001.44

Научные руководители:

доктор физико-математических наук, профессор, академик РАЕН Смелянский Руслан Леонидович; кандидат физико-математических наук, доцент Захаров Владимир Анатольевич.

Официальные оппоненты:

доктор физико-математических наук, профессор

Соколов Валерий Анатольевич; кандидат физико-математических наук, старший научный сотрудник Кулямин Виктор Вячеславович. Вычислительный центр имени A.A. Дородницына Российской академии наук.

Ведущая организация:

профессор

Н.П. Трифонов

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ

Актуальность работы. Одним из наиболее распространенных подходов к проверке правильности программ является метод верификации моделей программ (Model Checking, МС). Суть метода такова. Дли заданной программы строится её логическая модель, множество трасс которой покрывает множество вычислений программы. Спецификация программы, описывающая правильное поведение программы, задаётся в виде логических формул. Доказательство того, что программа удовлетворяет спецификации, заключается в проверке выполнимости указанных логических формул на модели программы. Чаще всего в качестве моделей программ выбираются размеченные системы переходов с конечным множеством состояний, а спецификации программ задаются в виде формул одной из темпоральных логик. Задача проверки выполнимости темпоральной формулы на модели с конечным множеством состояний алгоритмически разрешима. Более того, для многих темпоральных логик построены эффективные алгоритмы проверки выполнимости спецификации за время, линейное относительно размера модели1. Благодаря этому метод МС получил широкое распространение как практически пригодный автоматический метод верификации программ со сложным поведением.

В настоящее время существует несколько десятков систем верификации программ, разработанных на основе метода МС. В этих системах используются различные модели программ, темпоральные логики и алгоритмы проверки выполнимости логических формул. Наиболее известными из них являются системы верификации Spin, SMV, RuleBase, Java Pathfinder, SLAM, BLAST, которые успешно эксплуатируются во многих крупнейших компаниях, занимающихся разработкой вычислительной техники и программного обеспече-

1 Кларк Э., Грамберг О , Пелед Д. Верификация моделей программ: Model Checking. — М.: Издательство Московского центра непрерывного математического образования, 2002.

ния (Microsoft, Intel, NASA, IBM и др.). При помощи этих инструментальных средств удается проводить проверку правильности логических описаний микроэлектронных схем, драйверов операционных систем, сетевых протоколов, распределенных алгоритмов. Известно немало примеров обнаружения при помощи этих средств изощренных и трудноуловимых программных ошибок.

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

Модели распределённых систем такого вида состоят из однотипных взаимодействующих процессов; число процессов является параметром, зависящим от начальной конфигурации, и может быть сколь угодно большим. Вследствие этого, обычные алгоритмы решения задачи МС для конечных моделей программ не могут гарантировать корректной проверки параметризованных моделей программ. Таким образом, возникает задача верификации параметризованных моделей распределенных систем (Parameterized Model Checking, PMC), для решения которой нужны специальные алгоритмы.

Настоящая диссертация посвящена исследованию и решению задачи РМС для одного класса параметризованных моделей распределенных программ.

Цель работы. Цель диссертационной работы — разработка и анализ алгоритмов верификации параметризованных моделей распределённых программ с произвольным числом однотипных асинхронно-взаимодействующих процессов. При этом новые разработанные алгоритмы решения задачи РМС должны быть совместимы с теми способами представления конечных моделей программ и алгоритмами решения задачи МС для конечных моделей, которые используются в современных инструментальных системах верификации программ. Благодаря этому указанные системы верификации конечных моделей программ могут быть легко адаптированы для проверки правильности гораздо более широких классов распределенных программ.

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

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

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

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

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

пределенных алгоритмов и сетевых протоколов, применяющихся на практике.

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

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

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

тематических методой проверки правильности программ и построенных на их основе систем автоматической верификации программ.

Апробация работы. Результаты, представленные в работе, докладывались на объединённом научно-исследовательском семинаре кафедр автоматизации систем вычислительных комплексов, системного программирования и алгоритмических языков факультета ВМиК МГУ имени М.В. Ломоносова под руководством профессора М.Р. Шура-Бура, на научных семинарах лаборатории вычислительных комплексов кафедры автоматизации систем вычислительных комплексов факультета ВМиК МГУ имени М.В. Ломоносова под руководством профессора Р.Л. Смелянского, рабочих совещаниях группы проекта INTAS 05-1000008-8144 «Practical Formal Verification Using Automated Reasoning and Model Checking», а также на следующих конференциях:

• Всероссийские конференции «Методы и средства обработки информации» (Москва, октябрь 2003 и 2005 гг.);

• Научная конференция «Тихоновские чтения» (Москва, октябрь 2005 г.);

• Седьмая международная конференция «Дискретные модели в теории управляющих систем» (Москва, март 2006 г.);

• Научная конференция «Ломоносовские чтения» (Москва, апрель 2007);

• Научный семинар «Методы порождения инвариантов программ» (Workshop on Invariant Generation) (Австрия, Хагенберг, июнь 2007 г.);

• Пятая Всероссийская научная конференция студентов, аспирантов и молодых учёных «Технологии Microsoft в теории и практике программирования», секция «Теоретическое программирование» (Москва, апрель 2008 г.).

Работа была выполнена при поддержке грантов INTAS и РФФИ.

Публикации. По теме диссертации имеется 7 публикаций, список которых приводится в конце автореферата.

Структура и объем диссертации. Диссертация состоит из введения, шести глав, списка литературы и двух приложений. Объём работы — 142 страницы, с приложениями — 198 страниц. Список литературы содержит 110 наименований.

ОСНОВНОЕ СОДЕРЖАНИЕ РАБОТЫ

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

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

В первой главе проводится и обосновывается выбор математической модели распределенных программных систем, а также формулируется общая задачи верификации параметризованных моделей систем взаимодействующих процессов (Parameterized Model Checking, PMC).

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

• отсутствие глобальных часов,

• дискретное изменение состояний процессов,

• асинхронное выполнение процессов системы,

• взаимодействие процессов посредством синхронного обмена сообщениями,

• абсолютная надежность процессов и каналов связи.

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

В качестве моделей распределённых программ используются размеченные системы, переходов (ЬТв), состоящие из конечного множества размеченных состояний, множества начальных состояний и отношения размеченных переходов между состояниями. На множестве систем переходов определяется операция параллельной композиции. Отдельные процессы распределенной системы моделируются при помощи ЬТЯ, которые описываются в явном виде; модель всей распределенной системы образуется в результате параллельной композиции ЬТБ процессов: М = Р\ || • • • || Рп.

В качестве языка спецификаций поведения распределённых систем выбираются темпоральные логики: линейного времени 1_Т1_, ветвящегося времени СТ1_ и обобщение обеих логик — логика СТ1_*.

Задача верификации параметризованных моделей распределённых систем (РМСР1), рассматриваемая в данной работе, формулируется следующим образом. Пусть заданы

1. бесконечное семейство конечных моделей Т = {Мп}<£=1, параметризованное по параметру » £ К; каждая модель Мп = <3 || Р\ || • • • || Рп состоит из ЬТЭ фиксированного процесса (5 и п экземпляров процесса-прототипа Р — ЬТБ процессов Р^,

2. конечное множество Рг, г 6 I, / С М, наблюдаемых процессов, каждый из которых является некоторым вариантом процесса-прототипа Р\

3. спецификация, представленная формулой темпоральной логики зависящей от переменных выделенных процессов Рг, г £ /, и переменных процесса <3.

Требуется проверить выполнимость формулы на всех моделях семейства JF, т. е. убедиться в том, что соотношение Мп |= <р соблюдается для всех тг, п > 1.

В конце главы проводится обсуждение некоторых других вариантов задачи РМС.

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

Известно, что в общем случае задача РМС алгоритмически неразрешима?. Однако существуют классы параметризованных моделей, для которых задача РМСР может быть решена. Обзор методов верификации параметризованных моделей проводится относительно следующих критериев:

• область применимости метода (топология параметризованных моделей, виды параллелизма, способы взаимодействия процессов, ограничения на структуру LTS процессов),

• виды проверяемых спецификаций,

• возможность полной алгоритмизации.

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

2Apt К., Kozen D. Limits for automatic verification of finite-state concurrcnt systems. Information Processing Letter, vol. 15, Pp. 307- 309, 1986.

Методы поиска инвариантен осуществляют сведение задачи РМС к задаче МС для конечных моделей за счет конструирования для заданной параметризованной модели Т — {AijJ^Lj такой конечной модели Inv (инвариант), которая обладает следующими двумя свойствами:

1. модель Inv подобна некоторой модели Мk семейства Т,

2. параллельная композиция Inv || Р подобна модели Inv.

Если отношение подобия моделей обладает определенным набором свойств (монотонность параллельной композиции, консервативность отношения выполнимости для темпоральных формул), то верификация параметризованной модели Т сводится к решению задачи МС для конечных моделей Mi, М2, ■ • •, Affc-i, Inv. Отношения подобия на множестве моделей, а также способы конструирования модели-инварианта Inv могут быть разнообразны, и этим обеспечивается возможность широкого применения метода поиска инвариантов для решения задачи РМС. Отношение подобия консервативно для класса спецификаций Ф, если для любых подобных моделей М\ и Мг и любой спецификации tp £ Ф из выполнимости М2 |= tp следует выполнимость Mi |= tp. Отношение монотонно для операции параллельной композиции, если из подобия пар Mi и М2, Мз и М4 следует подобие Mi || Л/3 и Mi || М4.

В разделе 2.5 обосновывается выбор метода поиска инвариантов в качестве основного подхода к решению того варианта задачи РМС, который рассматривается в диссертационной работе. Предпочтение этому методу отдается по следующим причинам:

• возможность полной и эффективной алгоритмизации,

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

• сочетаемость метода с алгоритмами и инструментальными средствами верификации конечных моделей.

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

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

Модели распределённой системы описываются в виде LTS. В разделе 3.1 LTS определяется в виде шестерки (5,S°, A, R, Е, L), в которой S — конечное множество состояний, 5° — подмножество S начальных состояний системы, А — конечное множество действий, RCSxAxS — отношение размеченных переходов, Е — конечное множество булевых переменных системы, L — функция разметки состояний L : S —> 2Е. Конечная или бесконечная после-

а I Q2 an-1 ап т то

довательность Si —> ,?2 —+ ... —> sn —> ... переходов Lib называется путем в LTS, если (sj, at, si+1) Е R для всех г, г > 1. Путь в модели — это абстрактный образ вычисления моделируемой распределённой системы.

В разделе 3.2 определяется операция асинхронной параллельной композиции Mi ||r Мч для LTS Мг = (Si, Sf, Ai, Я,, Е„ ¿¿), i = 1,2. Одна из особен-

3Clarke Е., Grumberg О., Jha S. Verifying parameterized networks using abstraction and regular languages. In Proc. of 6-th International Conference on Concurrency Theory, Pp. 395-407, 1995.

ностей этой операции состоит I! том, что она требует янного указания правил синхронного взаимодействия моделей М\ и Мг- Правила взаимодействия задаёт синхронизатор Г = (Д,~), в котором множество Д С А[ описывает множество синхроиизируемых действий модели М\, а функция — : Д —+ Л2 описывает соответствующие действия модели М2, синхронно выполняющиеся с действиями из множества Д.

Раздел 3.3 посвящен сетевым грамматикам, с помощью которых задается описание топологии и порождаются модели параметризованного семейства. Контекстно-свободной сетевой грамматикой называется такая четвёрка С? = (Т,ЛГ, Р, 5), представленная конечным множеством терминалов Т (в роли терминалов вступают ЬТБ), конечным множеством нетерминалов Л^, стартовым нетерминалом Б и конечным множеством V правил вывода, имеющих вид X —* ^[7^1] ||р1 ••• ||гп_1 Уп[7?.п]. В каждом таком правиле участвуют нетерминал X 6 М, терминалы или нетерминалы ..., Уп € N и Т, синхронизаторы действий процессов Г,, 1 < г < п — 1, а также функции переименования действий С помощью сетевой грамматики порождаются ЬТБ, которые и образуют бесконечные параметризованные семейства конечных моделей программ. Аналогично выводу в контекстно-свободных грамматиках для каждого символа X из множества N и Т можно построить множество деревьев вывода Тгеез(А). На множестве деревьев вывода У Тгеез(Х)

хел/ит

определяется функция Ив^), сопоставляющая каждому дереву вывода соответствующую ЬТБ.

В разделе 3.4 приводится краткое описание темпоральной логики СТ1_* и сё подмножеств СТЦ 1_Т1_, АСТ1_*-Х, 1_Т1_-Х, используемых для описания свойств проверяемых моделей программ. В диссертационной работе для описания свойств моделей параметризованного семейства используются преимущественно логики АСТ1_*-Х и ПТ-Х, в формулах которых отсутствуют оператор X и квантор существования пути.

В разделе 3.5 вводится специальная классификация путей в моделях, которая используется в дальнейшем для определения новых разновидностей отношения симуляции между моделями. Если задана спецификация программы, то индивидуальные особенности определённых переходов ЬТБ могут быть важны для выполнимости спецификации, в то время как особенности других переходов не важны. Переходы последнего вида считаются ненаблюдаемыми, и в моделях распределённых систем для их обозначения часто используется специальный символ т. В общем случае для любой ЬТБ с отношением переходов Я можно выбрать некоторое множество наблюдаемых переходов Е, Е С /?. Конечным блоком называется такой конечный путь в2 • • ■ ——> 5„+ь в котором (в,, г, £¿+1) £ Е для всех 1 < г < п

и (зп,а, йп+О £ Е. Бесконечным блоком называется такой бесконечный путь —у ■ ■ ■ вь —■ ■ ■, в котором т. вг+1) ^ Е для всех г > 1. В том случае, когда в модели выделено некоторое множество наблюдаемых переменных Ео, то в качестве наблюдаемых переходов обычно выбираются все переходы из множества ОЬвегу^М, Е0) = {(я, а, | (я, а, £) 6 Я и (а ф т V ¿(й) П Е0 ф ¿(¿)ПЕо)}, а для обозначения всех остальных переходов используется запись

В четвёртой главе вводятся новые отношения симуляции: квазиблочная, блочная и полублочная. Исследованы основные свойства этих отношений. Показано, что введённые отношения обладают необходимым набором свойств для решения задачи верификации параметризованных моделей распределённых систем при помощи метода поиска инвариантов.

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

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

Среди различных отношений эквивалентности на моделях важную роль играют отношения бисимуляции. Для решения задачи РМС ранее использовалось отношение строгой бисимуляции (strong bisirnulation), а также некоторые ослабленные варианты этого отношения: ветвящаяся бисимуляции (branching bisirnulation), бисимуляция по прореживанию (stuttering bisirnulation). Одним из ослабленных отношений эквивалентности является отношение блочной бисимуляции (block bisirnulation4). Это отношение строже отношений ветвящейся и прореженной бисимуляции, но при этом, в отличие от ветвящейся бисимуляции, отношение блочной бисимуляции учитывает дивергенцию, т.е. бесконечные последовательности ненаблюдаемых переходов. Поэтому блочная бисимуляция обладает хорошими перспективами использования ее в качестве отношения подобия в методе поиска инвариантов.

В разделе 4-1 вводится отношение блочной симуляции, отличающееся от отношения блочной бисимуляции отсутствием свойства симметричности.

Определение 4.1 (Блочная симуляция, bks). Пусть заданы LTS М, = (5,, S®, А{, Rt, Е;, L,), г = 1,2, с выделенным множеством наблюдаемых переменных Ео Q Si П Ег- Отношение Н С Si х S2 называется блочной симуляцией на моделях Mi и М2 относительно Ео тогда и только тогда, когда для любой пары состояний (si,ij) 6 Н выполняются следующие условия:

1. Li(si) П Е0 = L2(ti) П Ео-

4Emerson Е, Namjoshi К. Reasoning about rings. In Proceedings of 22th ACM Conf on Principles of Programming Languages, Pp. 85-94, 1995.

2. Для любого конечного блока сг = йх 52 —> ■ ■ ■ 5т+1 из состояния в! найдётся такой конечный блок <5 = ^ Д ¿2 • ■ ■ — £„ ¿„+1 из состояния ¿1, что (вт-ц, ¿п+0 £ Я и (я^ £ Н верно для всех г,), 1 < г < т, 1 < ] < п.

3. Для любого бесконечного блока <х = йх —• • • —9—* зт • • • из состояния найдётся такой бесконечный блок 5 — ¿х ——> ■ ■ ■ —> —у • • ■ из состояния £1; что (я„ £_,) € Н верно для всех г,1 < г, 1 <

Для отношений эквивалентности вида и ЬТЭ М\ и используется запись М\ М2, если найдётся такое отношение Н вида $¡01, что для

каждого начального состояния во 6 5® найдётся такое начальное состояние ¿о € ¿2> чт0 (в<ь^о) € Н. Если зафиксировано множество переменных Е, то используется запись М\ Л/2.

Отношение блочной симуляции обладает свойством консервативности относительно формул логики АСТ1_*-Х, необходимым для применения метода инвариантов:

Теорема 4.3. Пусть даны ЬТБ М{ = (5„ 5,°, А„ Л,, Еь Ьг), г = 1,2, находящиеся в отношении блочной симуляции Н С х 52 относительно множества наблюдаемых переменных Ео С Ех П Ег- Для любой пары состояний (в, £) £ Н и любой формулы 1р логики АСТ1_*-Х с переменными из множества Ео верно: t\= <р => в |= <р.

Однако отношение блочной симуляции в общем случае не монотонно относительно операции параллельной композиции. Поэтому в разделе 4-2 вводится более слабое отношение квазиблочной симуляции.

Определение 4.3 (Квазиблочная симуляция, дЬз). Пусть заданы ЬТБ М, = (5г, Лг, /?;, Ег, Ьг = 1,2, с выделенным множеством наблюдаемых переменных Ео С Е1ПЕ2. Пусть также заданы множества наблюдаемых переходов

и Е2 моделей М\ и М2 соответственно. Отношение Я С ^ х52 называется квазиблочной симуляцией на моделях М\ и М2 относительно множеств Ео, Е\, если для любой пары состояний , ¿1) € Н выполняются следующие условия:

1. Ь1(51)ПЕо = Ь2(^)ПЕ0.

2. Для любого конечного блока а = —* ■ ■ ■ —* зт 5т+1 из состояния 51 модели М\ найдётся такой соответствующий блок (5 =

¿2 —» • • • —* Ьп+1 из состояния ¿1 модели Л/г, что (вт+ь^-и) 6

Н и (в;, £ Н верно для всех 1 < г < т., 1 < ] < п.

3. Для любого бесконечного блока а = й! ——> ■ ■ ■ -—> 8т —• ■ - из состояния модели М\ найдётся такой соответствующий бесконечный блок 5 = ¿1 • • • —> £„ • • ■ из состояния модели М2, что (si,tj) € Н верно для всех г,^, 1 < г, 1 < ].

В разделе 4-2-1 приводятся основные свойства квазиблочной симуляции. Из утверждения 4.4 следует, что отношение блочной симуляции является частным случаем отношения квазиблочной симуляции.

Утверждение 4.4. Пусть заданы ЬТБ =

с множеством наблюдаемых переменных Но С П Е2. Если Н С х 52 — отношение блочной симуляции для множества переменных Ео, то Н — отношение квазиблочной симуляции для множеств наблюдаемых переходов Е\ = ОЬзегу(М\, Ео) и ¿?2 = ОЬвегу(М2,'Ео) и множества наблюдаемых переменных Ео-

Одним из важнейших свойств квазиблочной симуляции, необходимым для применения метода инвариантов, является монотонность этого отношения относительно операции параллельной композиции:

Теорема 4.6. Пусть заданы:

• такие ЬТБ М, = (5„ 5,°, Л„ Д,, Е„ ¿¡), г = 1,2,3,4, '«то (Е1 и Е2) П (Е3 и Е4) = 0, Ах = А2 = А', Л3 = А4 = А" и А' Л А" = 0;

• такие непересекающиеся множества переменных Е' и Е", что Е' С (Е1 и Е3) и Е" С (Е2иЕ4);

• синхронизатор Г = (А,-), причём Д С А' и ~ : Д —> Л".

Тогда из Мх ^ М2 и А/3 ^ М4 следует М1 ||Г М3 м* Иг М^.

Как показано в разделе 4.2.2 отношение квазиблочной симуляции является также отношением прореженной симуляции, но не наоборот.

Теорема 4.7. Если МЛ М2, то М1 г<|Р М2.

Поскольку прореженная симуляция обладает свойством консервативности для формул логики АСТ1_*-Х, отсюда следует

Теорема 4.8. Пусть для ЬТБ М\ и М2 существует отношение квазиблочной симуляции, согласованное относительно формулы (р логики АСТ1_*-Х, т.е. М1 М2. Если М2 |= <р, то Мх \= (р.

Из указанных свойств следует, что отношение квазиблочной симуляции обладает всеми необход и мы ми свойствами для применения метода сетевых инвариантов к моделям асинхронных распределённых систем.

Главный недостаток квазиблочной симуляции — трудность вычисления этого отношения: требуется проводить тройной переборный поиск (по наблюдаемым действиям, по путям из соответствующих состояний и по всем парам состояний соответствующих путей). С точки зрения сложности поиска такого отношения выгоднее использовать отношений блочной симуляции. Для эффективного построения отношения блочной симуляции в разделе 4-3 определяется отношение полублочной симуляции.

Определение 4.5 (Полублочная симуляция, бЬб). Отношение Я С х называется отношением полублочной сильуляции на моделях — (¿>г, 5,°, Л,, Н,, Ег, ¿г), г — 1,2, относительно множества наблюдаемых неременных Ео С Е; П Е2, тогда и только тогда, когда для любой пары состояний , ¿1) € Я выполняются следующие условия:

1. ^1(а1)ПЕ0 = ^2(41)ПЕо.

2. Для каждого конечного блока а = й! йг • • • 5т вт+1

„ ^ , 9 в в

из состояния найдется такой конечный блок о = 1\ —> ¿2 —> ■ ■ ■ —>

¿п из СОСТОЯНИЯ в2, что

а. если п > 1, то (ях, <„) £ Н и (.5т+ь £„+1) С Я;

б. если п = 1, то («ш+ь^п+О € Я;

9 6

3. (дивергенция) Для каждого бесконечного блока а = ^ —> • ■ • —►

—• • • из состояния найдётся такой бесконечный блок 5 — 1 \ в в

■ ■ ■ —> —> • • • из состояния ¿1 и число к > 1, что (й!, е Я.

Теорема 4.9. Пусть даны ЬТБ М{ = 5,°, Д. Я,. Е„ ¿,), г = 1,2, ы лшо-жество наблюдаемых переменных Ео С Ех П Ег- В этом случае М\ ^^ Мг тогда и только тогда, когда М\ ^^ Мг-

Определение полублочной симуляции опирается па такие особенности устройства моделей, которые позволяют существенно ускорить переборный поиск — вместо тройного перебора, необходимого для вычисления квазиблочной симуляции, достаточно проводить лишь переборный поиск соответствующих блоков, исходящих из соответствующих состояний. Для осуществления этой возможности в разделе 4-3-1 установлен эффективно проверяемый критерий существования полублочной симуляции для ЬТБ, свободных от внутренних тупиков (НуеЬскв).

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

Идея предложенного метода такова. Деревья вывода сетевых грамматик, при помощи которых описывается параметризованная модель распределенной системы, позволяют порождать последовательно все LTSMjt, представляющие отдельные конечные модели этой системы. Поиск подходящей модели-инварианта проводится среди LTS Мь порождаемых деревьями вывода. Для проверки характеристических свойств инварианта в качестве отношения подобия используется отношение квазиблочной симуляции, удовлетворяющее требованиям монотонности и консервативности. Ранее доказанные теоремы гарантируют, что существование полублочной симуляции между моделями является достаточным условием существования квазиблочной симуляции между этими же моделями. Поэтому в целях повышения эффективности проверки соотношений инвариантности модели в нем вместо квазиблочной симуляции используется отношение полублочной симуляции. Если указанное соотношение выполнено и подходящая модель-инвариант М^ обнаружена, то решение задачи РМС для параметризованного семейства {М;}^ сводится к решению задачи МС для конечных моделей М\,М2, ■ ■ •, М^. Последняя задача решается при помощи известных алгоритмов верификации конечных моделей программ.

Более формально соотношения инвариантности модели относительно параметризованного семейства конечных моделей определяются следующим образом. Пусть задана сетевая грамматика G = (T,Af,V,S). Пусть для каж-

дого нетерминала А £ Л/" выбрано дерево вывода (представитель) Агерг 6

Тгеез(А). Определим функцию герг : N и Т —> и Тгеез(Х), которая

ХеМиТ

каждому нетерминалу А ставит в соответствие дерево вывода Лгерп а каждому терминалу р С Т — дерево, состоящее из самого терминала р.

Размеченные системы переходов из множества {/^(герг(Л)) | А £ Л/"} называются инвариантами соответствующих нетерминалов, если для каждого правила вывода грамматики А —> ВхЩ]\ ||р1 • • • ||г„_, Вп[Т^п] из предпосылок

• высота дерева вывода герг(А) равна Л;

• и 4 £ Тгеез(А) — произвольное дерево вывода из А высоты Н + 1, в котором из каждого нетерминала Д ф А выводится дерево герг(Д);

следует соотношение

Справедлива теорема о корректности метода инвариантов

Теорема 4.10 (Корректность метода инвариантов). Предположим, что для всякого нетерминала грамматики найден инвариант герг (А). Пусть А £ М — нетерминал грамматики, а £ — произвольное дерево из множества ТУеев(Л), в котором наибольшая высота деревьев для каждого нетерминала В грамматики больше или равна высоте инварианта герг (В). В этом случае верно соотношение

^(£) ^чЬ5 Из(герг(А)).

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

выводятся лишь терминалы или сам нетерминал А. После того, как инварианты для таких нетерминалов найдены, осуществляется поиск инвариантов для нетерминалов, использующих в правилах вывода другие нетерминалы.

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

В разделе 5.2 приводится краткое описание алгоритма построения полублочной симуляции с помощью итеративного вычисления неподвижной точки. Строящееся множество Н делится на два непересекающихся подмножества: опровергнутые пары (negatives) и неподтверждённые пары (positives). В начале работы алгоритма пары начальных состояний первой и второй модели заносятся в множество неподтверждённых пар. На каждой итерации алгоритма проверяется гипотеза о том, что все неподтверждённые пары удовлетворяют определению полублочной симуляции. Если в ходе проверки обнаруживается, что некоторая пара не удовлетворяет этому определению, она заносится в множество опровергнутых пар. Проверка прекращается, как только множества неподтверждённых и опровергнутых пар перестаёт расширяться.

В разделе 5.3 установлены верхние оценки сложности алгоритма. Получена следующая оценка сложности по времени алгоритма построения отношения полублочной симуляции для LTS Мг = {S1;, Sf, Аг, Ri, £„ ¿ = 1,2:

Сыне. <п\-п\-пА- 0(п] +п\ + пА-п\ ■ п\) < 0(п\ ■ п\ ■ п2А),

где щ = |Si| — число состояний LTS Mi, п2 = |5г| — число состояний LTS М2, па ~~ число наблюдаемых действий каждой LTS. Предполагается, что па<П2< щ.

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

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

В разделе 6.1 описана архитектура экспериментальной системы верификации параметризованных моделей распределённых систем CheAPS (Checker of Asynchronous Parameterized Systems). На вход системе подаются описания прототипов процессов и сетевой грамматики. По сетевой грамматике строятся модели, порождаемые нетерминальными символами грамматики. Для каждого нетерминала грамматики проводится поиск модели-инварианта среди моделей, выводимых из данного нетерминала. Проверка того, что модель является инвариантом, осуществляется с помощью построения полублочной симуляции. Когда для каждого нетерминала найдена модель-инвариант, может быть построен инвариант проверяемого семейства моделей. Далее с помощью инструментального средства верификации конечных моделей spin проводится проверка выполнимости спецификаций, заданных в виде формул логики LTL-X, на построенной модели-инварианте.

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

В разделе 6.2 описывается протокол резервирования ресурсов (RSVP),

который предоставляет механизм резервирования сетевых ресурсов для соблюдения заданного качества сервиса (QoS). Протокол реализован на транспортном уровне стека протоколов TCP/IP. Данный протокол используется для обеспечения определённой скорости передачи аудио- и видеотрафика от сервера к потребителю.

В разделе 6.3 проведен обозр и краткий анализ работ, посвящённых верификации протокола RSVP. В разделе 6-4 указаны основные абстракции, используемые при построении параметризованной модели протокола: процессы используют групповую рассылку сообщений, логическая топология системы соответствует бинарному дереву, механизмы контроля соединения и контроля доступа всегда разрешают соединение, сбои отсутствуют.

В разделе 6.5 описаны инварианты нетерминалов сетевой грамматики параметризованной модели RSVP и выделены те LTS, для которых проводилось построение полублочной симуляции с целью вычисления этих инвариантов. Приведены численные показатели экспериментов по построению полублочной симуляции для указанных LTS, а также данные времени построения отношений симуляции и потребления оперативной памяти для различных оптимизированных вариантов алгоритма построения полублочной симуляции.

В экспериментах построение полублочной симуляции для большинства моделей требовало не более 10 сек. процессорного времени и 20 МБ памяти. Для самых больших моделей с 1,8 млн. состояний и 25 тыс. состояний блочная симуляция была построена за 11,7 ч с использованием 300 МБ памяти. В экспериментах использовался сервер Лаборатории вычислительных комплексов (процессор AMD Opteron с тактовой частотой 2.4 ГГц).

Успешно подтверждена выполнимость следующих свойств на построенной модели-инварианте протокола RSVP: производитель не получает подтверждение о закрытии сессии, если он сам не отправил сообщение о закрытии сессии; маршрутизатор не отправляет запрос на резервирование, если

для сессии уже зарезервированы ресурсы; маршрутизатор получаст запрос на резервирование только после того, как был установлен маршрут; через маршрутизатор посылаются данные только в том случае, если соединение установлено.

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

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

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

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

ПУБЛИКАЦИИ ПО ТЕМЕ ДИССЕРТАЦИИ

1. Коннов И.В., Захаров В.А. Об одном подходе к верификации параметризованных симметричных распределённых программ // Труды Первой Всероссийской Научной Конференции «Методы и Средства Обработки Информации». —М.: Издательский отдел факультета ВМиК МГУ, 2003. - С. 395-400.

2. Захаров В.А., Коннов И.В. Об одном подходе к верификации асинхронных параметризованных распределённых программ // Труды Второй Всероссийской Научной Конференции «Методы и Средства Обработки Информации». —М.: Издательский отдел факультета ВМиК МГУ, 2005.

- С. 367-372.

3. И.В. Коннов, В.А. Захаров. Об одном подходе к верификации симметричных параметризованных распределенных систем // Программирование. - 2005. - №5. - С. 3-17.

4. Vladimir Zakharov and Igor Korrnov. An Invariant-based Approach to the Verification of Asynchronous Parameterized Networks. In International Workshop on Invariant Generation (WING'07), RISC, Hagenberg, Austria, June 25-27. RISC-Linz Report Series No. 07-07. Pp. 41-63.

5. I. V. Konnov, V. A. Zakharov. On the Verification of Asynchronous Parameterized Networks of Communicating Processes by Model Checking. // Сборник «Математические методы и алгоритмы», ИСПРАН. — 2007.

- т. 12. - С. 37-58.

6. Коннов И.В. Система верификации параметризованных моделей асинхронных распределённых систем (CHEAPS) // Труды пятой Всероссийской научно-технической конференции «Технологии Microsoft в теории и практике программирования» для студентов, аспирантов и молодых ученых Российской Федерации (Центральный федеральный округ). — 2008. - С. 225-226.

7. Коннов И.В. Применение ослабленных отношений симуляции в методе сетевых инвариантов для верификации параметризованных асинхронных моделей // Моделирование и анализ информационных систем. — 2008. - т. 15, № 3. - С. 3-13.

Подписано в печать 20.10.2008 Формат 60x88 1/16. Объем 1.75 п.л. Тираж 75 экз. Заказ № 755 Отпечатано в ООО «Соцветие красок» 119991 г.Москва, Ленинские горы, д.1 Главное здание МГУ, к. А-102

Введение

Проверка корректности программ.

Цель диссертационной работы.

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

Структура работы.16

Глава 1. Постановка задачи.19

1.1. Модели распределённых систем .19

1.2. Задача верификации моделей распределённых систем .22

1.3. Задача верификации параметризованных моделей распределённых систем .22

Глава 2. Обзор литературы .25

2.1. Аналитические методы редукции^ . . • ---------------29 -2.2. Методы абстракции.31

2.3. Символьные методы.35

2.4. Методы, основанные на поиске инварианта.38

2.5. Выводы, выбор метода и декомпозиция задачи .43

Глава 3. Основные определения .45

3.1. Размеченные системы переходов.45

3.2. Асинхронная параллельная композиция .49

3.3. Описание топологии распределённых систем с помощью сетевых грамматик.50

3.4. Темпоральные логики.53

3.5. Конечные и бесконечные блоки .56

3.6. Выводы.58

Глава 4. Новые отношения симуляции .59

4.1. Блочная симуляция .60

4.2. Квазиблочная симуляция.66

4.3. Полублочная симуляция .75

4.4. Выводы.95

Глава 5. Метод сетевых инвариантов для случая асинхронных параметризованных систем .96

5.1. Метод сетевых инвариантов с использованием квазиблочной и блочной симуляций .97

5.2. Алгоритм построения полублочной симуляции.100

5.3. Оценки сложности.106

5.4. Выводы.110

- Глава-6— Практическая-реализация и проверка протокола резервирования ресурсов .111

6.1. Архитектура системы CheAPS.Ill

6.2. Протокол резервирования ресурсов .114

6.3. Предыдущие работы по верификации протокола .117

6.4. Параметризованная модель.117

6.5. Верификация параметризованной модели.120

6.6. Проверка свойств модели протокола .125

6.7. Выводы.126

Заключение .127

Литература

129

Приложение А. Некоторые существующие отношения на LTS 143

А.1. Трассовая эквивалентность.143

А.2. Бисимуляционная эквивалентность (бисимуляция) .145

А.З. Прореженная бисимуляция.147

А.4. Ветвящаяся бисимуляция.^.148

А.5. Блочная бисимуляция.150

А.6. Симуляция .151

А.7. Прореженная симуляция .155

А.8. Выводы.156

Приложение Б. Детали реализации экспериментальной системы CheAPS .157

Б.1. Описание алгоритма построения полублочной симуляции . . . 157

Б.2. Язык TinyPromela .180

Б.З. Подсистема порождения моделей по сетевой грамматике . 181

--------------Б:4г Подсистема построения полублочной симуляции.184

Б.5. Подсистема поиска контрпримеров .197

Б.6. Выводы.198

Список иллюстраций

3.1 Диграммы LTS процессов типа Root, Inner, Leaf.48

4.1 Пример LTS, находящихся в отношении блочной симуляции . . 62

4.2 Полублочная симуляция.76

4.3 Взаимосвязь между путями в Similar Siblings . .77

4.4 Диаграмма путей пункта (2а).84

4.5 Диаграмма путей пункта (26) .85

4.6 Критерий полублочной симуляции.87

6.1 Архитектура системы проверки параметризованных систем . . . 113

6.2 Время построения полублочной симуляции с различными оптимизациями .123

6.3 Потребление памяти при построении полублочной симуляции с различными оптимизациями .124

А.1 Модели Mi и М2 находятся в отношении бисимуляции.146

-------------А-.2- LTS Mf и М.2 находятся в отношении симуляции.152

А.З Отсутствие симуляции для LTS, отличающихся уровнем абстракции .153

А.4 Процессы р и q и два экземпляра параметризованного семейства 154

Б.1 Сгенерированный граф модели из пяти процессов.183

Б.2 Архитектура подсистемы проверки симуляции.185

Б.З Признаки нестабильности пар состояний .196

Введение

Лев Николаевич (Королёв) оказался прав. Программ без ошибок не бывает.

Замечание С.А. Лебедева об ошибке в программе.

Проверка корректности программ

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

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

Как заметил Дейкстра [100]: «Тестирование программ может использоваться для демонстрации наличия ошибок, но оно никогда не покажет их отсутствие». Методы верификации направлены на доказательство утверждений о свойствах поведения программы или результатов её работы. Этот подход к проверке правильности программ был впервые предложен в работах А.А. Ляпунова [103, 104], Т. Хоара [40], Э. Дейкстры [100], Пратта [81] и Флойда [25].

Наиболее грандиозная задача верификации программ, известная как «Grand challenge», сформулирована в работе Хоара [41]. В этой работе описывается задача создания верифицирующего компилятора, т.е. такого компилятора, который проверяет корректность программы при трансляции. Там же приводится список достижений, благодаря которым Хоар считает, что технология разработки и верификации программ является достаточно зрелой для проведения исследований по созданию верифицирующего компилятора. В работе приводятся требования к решению задачи. Формулировка задачи используется в качестве общей цели для исследовательских групп, работающих в области валидации и верификации программ.

Методы верификации программ, использующие теоретико-доказательный подход, основываются на средствах автоматического доказательства теорем (САДТ, theorem prover, «прувер») [72, 73, 83, 90]. Описание программы представляется в виде множества логических утверждений. Спецификация программы также представляется в виде утверждения. САДТ строит доказательство выполнимости спецификации, исходя из утверждений, описывающих проверяемую программу.

К сожалению, при использовании САДТ в процессе построения доказательства может потребоваться участие эксперта. Одной из наиболее трудных задач, возникающих при верификации программ с помощью САДТ, является задача порождения инварианта цикла [40]. Инвариант цикла требуется при проверке выводимости постусловия функции из предусловия. Несмотря на значительный прогресс в этой области [51, 53], верификация большинства программ всё ещё требует привлечения эксперта.

Верификация программы с использованием логических утверждений, построенных непосредственно на основании исходных кодов программы, увеличивает сложность процесса доказательства. В тоже время некоторые фрагменты кода могут быть несущественными для проверки выделенных свойств программы. Свойства программы могут быть проверены на модели программы, более простой, чем исходная программа. Группа методов, основанных на верификации моделей (Model Checking, МС) [102], использует компромиссный подход между полноценной верификацией программы и тестированием, использующим формальную проверку свойств.

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

Первые примеры успешного применения МС относятся к проверке моделей аппаратных схем. В дальнейшем методы МС успешно применялись для проверки моделей сетевых протоколов, распределённых алгоритмов. В последние годы методы МС стали применяться и для верификации последовательных программ. В 2007 году за изобретение первых алгоритмов МС основоположники группы методов МС Э. Кларк, А. Эмерсон и Ж. Сифакис получили премию Тьюринга.

Применение методов МС ограничивает целый ряд недостатков, присущих этой группе методов:

• сложность построения адекватной модели,

• эффект «комбинаторного взрыва»,

• требование конечности модели.

Применение группы методов МС связано с нетривиальным вопросом построения корректной и адекватной модели. Модель строится для проверки соответствия исходной программы заданному набору спецификаций, поэтому модель должна быть адекватной, т.е. отражать все свойства исходной программы, необходимые для проверки спецификаций. Также модель должна быть корректной для выбранного набора свойств, т.е. поведение модели должно соответствовать поведению исходной программы с учётом выбранных свойств. От выбора свойств исходной программы, переносимых на модель, зависит адекватность модели^ проверяемому набору спецификаций и— -практическая применимость группы методов МС.

Если корректность модели можно гарантировать с помощью ограничений на методы построения модели по программе, то адекватность может быть проверена только после того, как проведена верификация модели. Для построения корректной модели могут использоваться методы автоматического порождения моделей (Model Extraction [45]) по заданной программе, а автоматическое построение адекватной модели достигается за счёт комбинирования методов булевой абстракции с итеративной верификацией моделей [12,14, 87]. Такой подход к построению моделей получил название Counter Example Guided Abstraction Refinement. В случае неудачной проверки построенной модели проводится уточнение модели с помощью САДТ. Стоит заметить, что в данном случае комбинируются средства МС и САДТ. Соответственно, гарантия полностью автоматической проверки моделей, вообще говоря, исчезает, так как не во всех случаях САДТ способны выдать доказательство запрашиваемого утверждения.

Эффект «комбинаторного взрыва» связан с экспоненциальным ростом пространства состояний при линейном росте числа взаимодействующих процессов. Последствиями экспоненциального роста пространства состояний становятся высокие требования к объему памяти, используемой верификатором моделей, и долгое время проверки модели. Для сжатия проверяемого множества состояний используются символьные способы представления моделей, например, двоичные разрешающие диаграммы (Binary Decision Diagrams, BDD) [19]. В символьном представлении модели выражаются с помощью BDD, которые реализуют функции алгебры логики. При поиске в пространстве состояний вместо перебора состояний используются операции над функциями. Алгоритмы верификации моделей с помощью BDD могут быть значительно эффективнее явного перебора состояний в том случае, когда BDD системы переходов модели и промежуточных результатов остаются компактными [65]. Для моделей аппаратных схем представление модели в виде BDD даёт хороший коэффициент сжатия по отношению к явному представлению множеств. Модели распределённых программ сжимаются несколько хуже, так как в распределённых программах используется асинхронное взаимодействие.

Для борьбы с «комбинаторным взрывом» при верификации моделей программ используются методы редукции частичных порядков [43, 76, 77]. В этих методах проверяется достаточное подмножество множества всех трасс. Такое подмножество вычисляется на основании зависимостей между переходами процессов модели. Типы проверяемых зависимостей выявляются эмпирически. Удачный выбор правил редукции может существенно ускорить алгоритм верификации модели [43].

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

При верификации моделей с бесконечным числом состояний (Infinite State-Space Model Checking) в описании модели могут присутствовать переменные с неограниченными типами данных, а порождаемая по описанию система переходов обладает бесконечным множеством состояний. Для решения этой задачи используются комбинации символьных методов верификации моделей и методов доказательства теорем [4, 18, 24, 30, 32, 36, 48, 63, 66, 69, 80, 85, 89].

Задача верификации параметризованных моделей (Parameterized Model Checking, PMC) возникает при рассмотрении моделей распределённых систем, в которых число однотипных взаимодействующих процессов зависит от начальной конфигурации системы и может быть сколь угодно большим. Как известно, увеличение числа вычислителей не всегда приводит к линейному росту производительности распределённой системы. Аналогично, выводы о выполнимости спецификации, полученные для конфигурации с одним числом процессов, нельзя переносить на конфигурации с другим числом процессов, не приводя дополнительной аргументации. Решение задачи РМС позволяет убедиться в выполнимости проверяемых спецификаций при масштабировании распределённой программы, т.е. при росте числа взаимодействующих процессов.

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

В задаче РМС рассматриваются распределённые системы взаимодействующих процессов. В этих системах присутствует фиксированное число статических процессов и неограниченное число однотипных процессов. Так как число однотипных процессов не ограничено, то по распределённой системе может быть построено бесконечное семейство моделей. Каждая модель соответствует конфигурации системы с фиксированным числом процессов. Для проверки свойств распределённой системы необходимо проверить спецификацию на всех моделях бесконечного семейства. Способы решения задачи для некоторых случаев параметризованных моделей приведены в работах [2, 711, 15, 17, 20-23, 28, 47, 49, 54-59, 61, 62, 64, 68, 71, 85, 86, 88, 89, 92, 93, 95, 97]. В последующих разделах будет проведён краткий анализ этих методов. Именно задаче верификации параметризованных моделей распределённых систем посвящена настоящая диссертационная работа.

Цель диссертационной работы

Цель диссертационной работы — разработка и анализ алгоритмов верификации параметризованных моделей распределённых программ для проверки свойств распределённых программ с произвольным числом однотипных асинхронно-взаимодействующих процессов.

При этом предъявляются следующие требования к решению:

• разрабатываемые алгоритмы должны опираться на существующие алгоритмы верификации моделей с конечным числом состояний;

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

Актуальность работы

В области вычислительной техники исследуются классы систем, параметризованных по числу взаимодействующих компонентов. К числу таких систем относятся:

• распределённые алгоритмы [60, 91]: волновые алгоритмы, распределения ресурсов, взаимного исключения доступа к критической секции, избрания лидера (leader election), обнаружения завершения (termination detection), согласованного принятия транзакции (distributed commit);

• сетевые протоколы [109]: кольцо с маркером, протоколы маршрутизации, протоколы обеспечения качества сервиса, широковещательные протоколы;

• аппаратные схемы: аппаратные схемы управления доступом к шине при различном числе клиентских устройств, протоколы обеспечения когерентности кэшей [38].

В дальнейшем под словами «распределённый алгоритм» мы будем понимать как системы из первого, так и из второго пункта.

Довольно часто при построении модели распределённой системы, которая может потенциально содержать любое количество однотипных процессов, ограничиваются моделью с небольшим, фиксированным числом процессов. При этом предполагается, что свойства, проверенные на модели с фиксированным числом процессов, автоматически масштабируются для моделей с большим числом процессов. Однако этот приём не является вполне корректным: известны примеры, когда спецификация была верна на модели с одним числом процессов и нарушалась при изменении числа процессов [102, с- 161], [7].

Это означает, что для верификации параметризованных моделей программ недостаточно проверить спецификацию на нескольких моделях с фиксированным числом процессов: необходимо обоснование масштабируемости проверенной спецификации на остальные модели. Так как число процессов в моделях не ограничено, то спецификация должна быть проверена на бес конечном семействе моделей с конечным числом состояний. В работе [1] показано, что в общем случае задача РМС сводится к задаче останова машины Тьюринга и, следовательно, алгоритмически неразрешима.

Тем не менее, для некоторых практически интересных классов параметризованных моделей задача РМС может быть решена. Так, показана разрешимость задачи для однонаправленных колец с маркером одного типа [20], колец с произвольным типом маркера и дополнительными ограничениями на LTS процесса [23, 93], симметричных систем с глобальными предусловиями переходов [21, 24], широковещательных систем [21, 22, 61], систем с произвольной топологией и одним маркером [95]. Предложены различные полуразрешающие процедуры: подходы, основанные на поиске инвариантов [911, 52, 55, 64, 86, 97]; подходы, основанные на проверке достижимых состояний регулярных моделей [2, 30, 59, 88]; символьные методы верификации [4, 80, 85]. Указаны способы абстракции [2, 36, 47, 50, 57, 61, 95] для определённых классов систем.

Как будет показано в обзоре, наиболее перспективными методами, настраиваемыми на различные виды топологии параметризованных систем, являются методы, основанные на поиске инвариантов, и символьные методы. Символьные методы верификации параметризованных систем могут потребовать участия эксперта для переработки модели и указания дополнительных подсказок. Примечательно, что примеры успешного применения метода, основанного на поиске инвариантов, относятся к классам распределённых систем синхронно-взаимодействующих процессов [9-11, 52, 55, 97], хотя метод инвариантов использовался и для систем асинхронно-взаимодействующих процессов в работах [11, 64, 86].

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

Таким образом, задача верификации параметризованных моделей распределённых систем актуальна. Однако при разработке таких методов и средств желательно сохранить основное преимущество метода МС — свойство автоматической верификации модели. Необходимо, чтобы для верификации параметризованной модели не требовалась существенная перестройка модели, использованной при верификации средствами МС, или участие эксперта.

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

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

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

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

Структура работы

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

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

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

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

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

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

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

В заключении формулируются основные результаты работы и возможные направления развития.

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

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

6.7. Выводы

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

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

Заключение

В диссертационной работе получены следующие основные результаты:

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

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

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

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

Методы инвариантов, за исключением [7] и [102, стр. 307], проверялись на простых примерах: взаимного исключения процессов в критической секции в кольце и звёздообразной топологии, распространении сообщения в дереве и т.д. В настоящей работе с помощью предлагаемого метода проверяется параметризованная модель протокола резервирования ресурсов (RSVP). Число состояний проверяемых моделей параметризованного семейства варьируется от нескольких десятков тысяч до нескольких миллионов.

Предложенные в данной работе ослабленные отношения симуляции могут быть применены не только для решения задачи верификации параметризованных моделей распределённых систем, но и для обоснования модульного подхода к верификации моделей [35], редукции частичных порядков [43, 76, 77], т.е. там, где используется отношение симуляции.

Направления дальнейших исследований. Построение полублочной симуляции, используемой при поиске инварианта, может быть ускорено за счёт вычисления эквивалентных состояний на модели, а также за счёт применения техник символьных подходов и статического анализа. Интересна задача комбинирования автоматических методов абстракции с автоматическими методами инвариантов для проверки моделей, в описаниях которых присутствуют целочисленные счётчики.

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

1. Apt К., Kozen D. Limits for automatic verification of finite-state concurrent systems // 1.formation Processing Letter. — 1986. — Vol. 15. — Pp. 307309.

2. Browne M. C., Clarke E. M., Grilmberg O. Characterizing finite kripke structures in propositional temporal logic // Theor. Comput. Sci. — 1988. — Vol. 59, no. 1-2,- Pp. 115-131.

3. Bultan Т., Gerber R., Pugh W. Symbolic model checking of infinite state systems using presburger arithmetic // CAV '97: Proceedings of the 9th International Conference on Computer Aided Verification. — London, UK: Springer-Verlag, 1997.- Pp. 400-411.

4. Bulychev P., Konnov I., Zakharov V. Computing (bi)simulation relations preserving ctlx logic for ordinary and fair kripke structures // Труды Института системного программирования РАН. — Vol. 12. — 2007. — Pp. 59-76.

5. Calder M., Miller A. Five ways to use induction and symmetry in the verification of networks of processes by model-checking // Automated Verification of Critical Systems (AvoCS 2002). — 2002. — Pp. 29-42.

6. Calder M., Miller A. Using spin to analyse the tree identification phase of the ieee 1394 high performance serial bus (firewire) protocol // Formal Aspects of Computing. 2003. - Pp. 247-266.

7. Calder M., Miller A. Detecting feature interactions: how many components do we need? // Objects, Agents and Features. — 2004. — Vol. 2975. — Pp. 4566.

8. Clarke E., Grumberg 0., Browne M. Reasoning about networks with many identical finite-state processes // PODC '86: Proceedings of the fifth annual ACM symposium on Principles of distributed computing. — New York, NY, USA: ACM, 1986. Pp. 240-248.

9. Clarke E., Grumberg O., Jha S. Verifying parameterized networks using abstraction and regular languages // 6-th International Conference on Concurrency Theory. — 1995. — Pp. 395-407.

10. Clarke E., Grumberg O., Jha S. Verifying parameterized networks // ACM Transactions on Programming Languages and Systems. — 1997. — Vol. 19, no. 5. Pp. 726-750.

11. Cleaveland R., Sokolsky O. Equivalence and preorder checking for finite-state systems // Handbook of Process Algebra / Ed. by J. Bergstra, A. Ponse, S. Smolka. North-Holland, 2001. — Pp. 391-424.

12. Counterexample-guided abstraction refinement / Б. Clarke, O. Grumberg, S. Jha et al. // Computer Aided Verification. 2000. - Pp. 154-169.

13. Creese S., Reed J. Verifying end-to-end protocols using induction with csp/f-dr // IPPS/SPDP Workshop. 1999.- Pp. 1243-1257.

14. De Nicola R., Vaandrager F. Three logics for branching bisimulation // ,7. ACM. 1995. - Vol. 42, no. 2. - Pp. 458-487.

15. Delzanno G. Constraint-based verification of parameterized cache coherence protocols // Form. Methods Syst. Des. — 2003. — Vol. 23, no. 3. — Pp. 257301.

16. Drechsler R., Becker B. Binary Decision Diagrams — Theory andlmple-mentation. — Kluwer Academic Publishers, 1998.

17. Emerson E., Namjoshi K. Reasoning about rings // Proceedings of 22th ACM Conf. on Principles of Programming Languages. — 1995.— Pp. 8594.

18. Emerson E. A., Kahlon V. Exact and efficient verification of parameterized cache coherence protocols // 12th IFIP Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME). — LAquila, Italy: 2003. Pp. 247-262.

19. Emerson E. A., Kahlon V. Model checking guarded protocols // LICS.— IEEE Computer Society, 2003. — Pp. 361-370.

20. Emerson E. A., Kahlon V. Parameterized model checking of ring-based message passing systems // Computer Science Logic. — Vol. 3210/2004 of LNCS. 2004. - Pp. 325-339.

21. Emerson E. A., Namjoshi K. S. On model checking for non-deterministic infinite-state systems // LICS '98: Proceedings of the 13th Annual IEEE Symposium on Logic in Computer Science. — Washington, DC, USA: IEEE Computer Society, 1998. P. 70.

22. Floyd R. Assigning meanings to programs // Proc. AMS Symp. on Applied Mathematics. — Vol. 19.— Providence: Amer. Mathematical Soc., 1967.— Pp. 19-31.

23. Fokkink W. Introduction to Process Algebra / Ed. by W. Brauer, G. Rozen-berg, A. Salomaa. — Secaucus, NJ, USA: Springer-Verlag New York, Inc., 2000.

24. Fossaceca J., Sandoz J., Winterbottom P. The pathstar access server: facilitating carrier-scale packet telephony // Bell Labs Technical Journal. — 1998. Vol. 3, no. 4. - Pp. 86-102.

25. German S. M., Sistla A. P. Reasoning about systems with many processes // J. ACM. 1992. - Vol. 39, no. 3. - Pp. 675-735.

26. Ghemawat S., Gobioff H., Leung S.-T. The google file system // SOSP '03: Proceedings of the nineteenth ACM symposium on Operating systems principles. New York, NY, USA: ACM, 2003. - Pp. 29-43.

27. Gregoire J. State space compression in spin with gets // Proc. Second Spin Workshop. Vol. 32 of DIMACS. - 1996. - Pp. 90-108.

28. Gribomont E. P., Zenner G. Automated verification of szymanski's algorithm // TACAS '98: Proceedings of the 4th International Conference on Tools and Algorithms for Construction and Analysis of Systems. — London, UK: Springer-Verlag, 1998. Pp. 424-438.

29. Griffioen D., Vaandrager F. Normed simulations // Computer-Aided Verification, CAV '98 / Ed. by A. J. Ни, M. Y. Vardi. Vol. 1427. - Vancouver, Canada: SV, 1998.- Pp. 332-344.

30. Grumberg 0., Long D. E. Model checking and modular verification // ACM Trans. Program. Lang. Syst.— 1994. — Vol. 16, no. 3. — Pp. 843-871.

31. Gyuris V., Sistla A. P. On-the-fly model checking under fairness that exploits symmetry // CAV '97: Proceedings of the 9th International Conference on Computer Aided Verification. — London, UK: Springer-Verlag, 1997.- Pp. 232-243.

32. Hennessy J. L., Patterson D. A. Computer architecture: a quantitative approach. — San Francisco, CA, USA: Morgan Kaufmann Publishers Inc., 2002.

33. Hennessy M., Milner R. Algebraic laws for nondeterminism and concurrency // J. ACM. — 1985. — Vol. 32, no. 1.- Pp. 137-161.

34. Hoare C. An axiomatic basis for computer programming // С ACM.— 1969.- Vol. 12, no. 10.- Pp. 576-585.

35. Hoare T. The verifying compiler: A grand challenge for computing research // J. ACM. 2003. - Vol. 50, no. 1. - Pp. 63-69.

36. Holzmann G. Design And Validation Of Computer Protocols. — Prentice-Hall, 1991.-512 pp.

37. Holzmann G., Peled D. An improvement in formal verification // FORTE 1994 Conference. 1994. - Pp. 197 - 211.

38. Holzmann G., Puri A. A minimized automaton representation of reachable states // Software Tools for Technology Transfer, Vol. 3, No. 1. — 1998.

39. Holzmann G., Smith M. Software model checking: Extracting verification models from source code // Formal Methods for Protocol Engineering and Distributed Systems. — Kluwer Academic Publ., 1999. — Pp. 481-497.

40. Holzmann G. J. The SPIN Model Checker : Primer and Reference Manual. — Addison-Wesley Professional, 2003. — September. — 596 pp.

41. Ip С. N.} Dill D. L. Verifying systems with replicated components in mur-phi // Form. Methods Syst. Des. 1997. - Vol 14, no. 3.- Pp. 273-310.

42. Kahlon V. Model checking: beyond the finite: Ph.D. thesis / The University of Texas at Austin. — 2004. — Supervisor-Ernest Allen Emerson, II.

43. Kesten Y., Pnueli A. Control and data abstraction: The cornerstones of practical formal verification // International Journal on Software Tools for Technology Transfer. 2000. — Vol. 2, no. 4. - Pp. 328-342.

44. Lesens D. Invariants of parameterized binary tree networks as greatest fixpoints // Algebraic Methodology and Software Technology. — 1997. — Pp. 337-350.

45. Lesens D., Saidi H. Abstraction of parameterized networks. — 1997.

46. Lesens D., Saidi H. Automatic verification of parameterized networks of processes by abstraction // 2nd International Workshop on the Verification of Infinite State Systems (INFINITY'97). 1997. - Pp. 268-278.

47. Lynch N. A. Distributed Algorithms. — San Francisco, CA, USA: Morgan Kaufmann Publishers Inc., 1996.

48. Maidl M. A unifying model checking approach for safety properties of parameterized systems // CAV '01: Proceedings of the 13th International Conference on Computer Aided Verification. — London, UK: Springer-Verlag, 2001.- Pp. 311-323.

49. Manna Z., Pnueli A. An exercise in the verification of multi-process programs // Beauty is our business: a birthday salute to Edsger W. Dijkstra. — 1990.- Pp. 289-301.

50. Manolios P. Mechanical Verification of Reactive Systems: Ph.D. thesis / University of Texas at Austin. — 2001.

51. Marelly R., Grumberg 0. Gormel — grammar oriented model checker // Tech. Rep. 697. — Haifa, Israel: The Technion, 1991.

52. McMillan K. Symbolic Model Checking. — Kluwer Academic Publishers, 1993.

53. Meyer A., Stockmeyer L. The equivalence problem for regular expressions with squaring requires exponential space"//' 13th IEEE Sympron Switching -and Automata Theory. — 1972. — Pp. 125-129.

54. Namjoshi К. S. A simple characterization of stuttering bisimulation // Proceedings of the 17th Conference on Foundations of Software Technology and Theoretical Computer Science. — London, UK: Springer-Verlag, 1997. Pp. 284-296.

55. Nilsson M. Structural Symmetry and Model Checking: Ph.D. thesis / Uppsala University, Uppsala, Sweden. — 2005.— 157 pp.

56. Nipkow Т., Paulson L. C., Wenzel M. Isabelle/HOL — A Proof Assistant for Higher-Order Logic. Springer, 2002. - Vol. 2283 of LNCS.

57. Page R., Tarjan R. Three partition refinement algorithms // SI AM Journal on Computing. — 1987. — Vol. 6, no. 16. — Pp. 973-989.

58. Park D. Concurrency and automata on infinite sequences // Proceedings of the 5th Gl-Conference on Theoretical Computer Science. — London, UK: Springer-Verlag, 1981.-Pp. 167-183.

59. A partial order approach to branching time logic model checking / R. Gerth, R. Kuiper, D. Peled, W. Penczek // Inf. Comput.- 1999,- Vol. 150, no. 2,- Pp. 132-152.

60. Partial order reductions preserving simulations / W. Penczek, M. Szreter, R. Gerth, R. Kuiper // Proc. of Concurrency, Specification and Programming (CSP'99).-Warsaw: 1999.-Pp. 153-172.

61. Peled D. Partial order reduction: linear and branching temporal logics and process algebras // POMIV '96: Proceedings of the DIMACS workshop on Partial order methods in verification. — New York, NY, USA: AMS Press, Inc., 1997.-Pp. 233-257.

62. Peled D. A. Software Reliability Methods / Ed. by D. Gries, F. B. Schneider. — Secaucus, NJ, USA: Springer-Verlag New York, Inc., 2001.

63. Pratt V. Semantical considerations on floyd-hoare logic // Proc. 17th Ann. IEEE Symp. on Foundations of Computer Science. — 1976. — Pp. 109-121.

64. Braden R., Zhang L., Berson S. et al. Resource reservation protocol (rsvp). — 1997. http://tools.ietf.org/html/rfc2205.

65. Riazanov A., Voronkov A. The design and implementation of vampire // Al Commun. 2002. - Vol. 15, no. 2. - Pp. 91-110.

66. Rudd Т., Orr M., Bicking I. Cheetah: The python-powered template engine // 10th International Python Conference.— 2002. http://www. python.org/workshops/2002-02/papers/08/index.htm.

67. Shahar E. Tools and Techniques for Verifying Parameterized Systems: Ph.D. thesis / Weizmann Institute of Science, Israel. — 2001. — 120 pp.

68. Shtadler Z., Grumberg O. Network grammars, communication behaviors and automatic verification // Proceedings of the International Workshopon Automatic Verification Methods for Finite State Systems. — London, UK: Springer-Verlag, 1990. Pp. 151-165.

69. Software verification with blast / T. A. Henzinger, R. Jhala, R. Majumdar, G. Sutre // 10th SPIN Workshop on Model Checking Software (SPIN).-LNCS 2648. Springer-Verlag, 2003. - Pp. 235-239.

70. A survey of regular model checking / P. Abdulla, B. Jonsson, M. Nils-son, M. Saksena // Proc. 15th Int. Conf. on Concurrency Theory.— Vol. 3170/2004 of Lecture Notes in Computer Science. — 2004. — Pp. 35-48.

71. Symbolic model checking with rich assertional languages / Y. Kesten, O. Maler, M. Marcus et al. // CAV '97: Proceedings of the 9th International Conference on Computer Aided Verification. — London, UK: Springer-Verlag, 1997. Pp. 424-435.

72. System description: Spass version 3.0 / C. Weidenbach, R. Schmidt, T. Hillenbrand et al. // Automated Deduction CADE-21 : 21st International Conference on Automated Deduction. — 2007. — Pp. 514-520.

73. Tel G. Introduction to Distributed Algorithms. — Cambridge University Press, 2000.

74. Thistle J., Nazari S. Analysis of arbitrarily large networks of discrete-event systems // 44th IEEE Conference on Decision and Control (CDC'05).— Seville, Spain: 2005.

75. Thistle J., Nazari S. Structural conditions for model-checking of parameterized networks // 7th International Conference on Application of Concurrency to System Design (ACSD'07).— Bratislava, Slovak Republic: 2007.

76. Van Glabbeek R. J., Peter Weijland W. Branching time and abstraction in bisimulation semantics // J. ACM. — 1996. — Vol. 43, no. 3. — Pp. 555-600.

77. Verification by network decomposition / E. Clarke, M. Talupur, T. Touili, H. Veith // CONCUR 2004. Vol. 3170. - 2004. - Pp. 276-291.

78. Villapol M. Modelling and Analysis of the Resource Reservation Protocol using Coloured Petri Nets: Phd thesis / Institute for Telecommunications Research and Computer Systems Engineering Centre, University of South Australia. 2003. — 362 pp.

79. Ахо А., Хопкрофт Д., Ульман Д. Построение и анализ вычислительных алгоритмов. — М.: Мир, 1979.

80. Царьков Д. Верификация распределённых программ методом проверки на модели: Дис. канд. физ.-мат. наук: 05.13.11 / Московский Государственный Университет им. М.В. Ломоносова. — 2002.— 185 с.

81. Дейкстра Э. Дисциплина программирования. — М.: Мир, 1978.

82. Дейт К. Введение в системы баз данных. — М.: Вильяме, 2006. — 1328 с.

83. Кларк Э., Грамберг О., Пелед Д. Верификация моделей программ: Model Checking. — М.: Издательство Московского центра непрерывного математического образования, 2002.

84. Ляпунов А. О логических схемах программ // Проблемы кибернетики. Т. 1. - М.: Физматгиз, 1958. - С. 46-74.

85. Ляпунов А., Янов Ю. О логических схемах программ // Труды конференции «Пути развития советского математического машиностроения и приборостроения». — Т. 3. — М.: 1956. — С. 5-8.

86. Никифоров Б. Электроника на службе безопасности движения // Современные технологии автоматизации. — 2006. — JN® 1. — С. 40-45.

87. Смелянский Р. Математическая модель функционирования распределённых ВС // Вестник МГУ. 1990. - Т. 15, № 3.

88. Страуструп Б. Язык программирования С++. — М.: Бином, 1999.— С. 991.

89. Таненбаум Э. Компьютерные сети.— СПб.: Питер, 2007.

90. Таненбаум Э., ван Стеен М. Распределённые системы. Принципы и парадигмы. — СПб.: Питер, 2003.