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

Российская академия наук

Сибирское отделение Институт систем информатики им. А. П. Ершова

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

В.Е. Козюра

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

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

Автореферат

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

Новосибирск 2004

Работа выполнена в Институте систем информатики им. А.П.Ершова Сибирского отделения Российской академии наук

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

Непомнящий В.А.

Официальные оппоненты: доктор физико-математических наук

Ломазова Ирина Александровна кандидат физико-математических наук Викентьев Александр Александрович

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

Ярославский государственный университет (г. Ярославль)

Защита состоится 14 сентября 2004 года в 15 час. 00 мин. на заседании диссертационного совета К003.032.01 в Институте систем информатики им А. П. Ершова Сибирского отделения РАН по адресу:

630090, г. Новосибирск, пр. Лаврентьева, 6.

С диссертацией можно ознакомиться в читальном зале ИСИ СО РАН (пр. Лаврентьева, 6).

Автореферат разослан 40 августа_2004 г.

Ученый секретарь диссертационного совета К003.032.01

к.ф.-м.н.

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

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

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

Однако, при полном моделировании работы сети мы сталкиваемся с так называемой проблемой взрыва числа состояний. Эта проблема состоит в том, что при росте размеров рассматриваемой сети ее полная модель достаточно быстро становится необозримо большой. Это не позволяет надеяться на построение полной модели для реальных систем. Отдельным и, как это

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

Одним из относительно новых и интенсивно развивающихся направлений в области создания эффективных методов верификации распределенных систем является метод развертки сетей Петри. Данный метод позволяет во многих случаях существенно уменьшить размер модели, не теряя при этом свойств рассматриваемой сети. Использование разверток для анализа сетей Петри было предложено К.Л. МакМилланом и развито впоследствии такими авторами, как Дж. Эспарца, С. Ремер, К. Хелиянко, В. Бибер, X. Фляйшхак, Ф. Валнер, и др. Кроме существенных улучшений алгоритмов и критериев построения развертки был разработан метод проверки моделей первоначально Дж. Эспарцой для логики S4, а впоследствии Ф. Валнером для логики линейного времени ШЪ. Алгоритмы проверки моделей для логики ШЪ с использованием разверток были развиты в последующих работах. В работах В. Бибера и X. Фляйшхака метод развертки и метод проверки моделей Эспарцы был применен к сетям Петри с интервальным временем.

В России также велись исследования по верификации распределенных систем с использованием сетей Петри. Отметим, в частности, работы Н.А. Анисимова по ручному моделированию с использованием сетей Петри, О.Л. Бандман по спецификации поведения сетевых протоколов, И.Б. Вирбицкай-те по использованию техники частичного порядка для верификации временных сетей Петри и В.А. Соколова по анализу параллельных программ.

Среди различных расширений стандартных сетей Петри выделяются сети Петри высокого уровня - раскрашенные сети Петри (РСП), для которых развит теоретический аппарат, накоплен значительный опыт использования и реализована система симуляции и анализа Design/CPN. В РСП вместо стандартных фишек используются типизированные знаковые элементы. Это позволяет определять эффективные спецификации симметрии и эквивалентности на РСП и использовать их для сужения пространства состояний. Кроме того, в РСП помимо классической интервальной временной модели описана и используется так называемая модель временных штампов. РСП обладают большей выразительной силой по сравнению со стандартными сетями Петри и позволяют удобно описывать достаточно сложные

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

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

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

• Для раскрашенных сетей Петри была предложена уникальная временная модель с использованием временных штампов. Хотя данная модель позволяет описывать многие временные события естественным образом, использовать ее значительно сложнее, чем классическую интервальную модель времени.

• Формально введенные понятия симметрии и эквивалентности для РСП, позволяющие существенно сужать пространство состояний системы, представляют собой дополнительные трудности при определении новых понятий для РСП.

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

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

- разработка эффективных методов построения разверток РСП без временных конструкций;

- исследование метода развертки для РСП, расширенных спецификациями эквивалентности и двумя временными конструкциями;

- разработка метода проверки моделей с использованием разверток РСП, расширенных спецификациями эквивалентности и двумя временными конструкциями;

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

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

Научная новизна

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

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

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

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

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

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

Апробация работы проведена на следующих международных научных конференциях:

International Conference on Parallel Computing in Electrical Engineering (PARELEC 2002). Warsaw, Poland;

4th International Conference of Perspectives of System Informatics (PSV01), Novosibirsk, Russia, 2001;

5th International Workshop on Concurrency, Specification and Programming, Warsaw, Poland, 2001;

Четвертый Сибирский Конгресс по Прикладной и Индустриальной Математике (ИНПРИМ- 2000), Новосибирск, Россия, 2000.

Кроме того, полученные результаты обсуждались на семинарах лаборатории теоретического программирования ИСИ СО РАН и кафедры систем информатики НГУ.

Публикации. По теме диссертации опубликовано 10 научных работ.

Структура работы. Диссертация состоит из введения, пяти глав, заключения и списка литературы из 56 наименований. Содержание составляет 85 страниц. Работа включает 26 иллюстраций и 4 таблицы.

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

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

В первой главе даны предварительные понятия, используемые в работе. В разд. 1.1 описываются базовые понятия, связанные с сетями Петри и их развертками. В подразд. 1.1.1 основными являются определения О-сети, являющейся ограниченным вариантом стандартной сети Петри и ветвящегося процесса для стандартной сети Петри. Ветвящийся процесс определяется как пара, состоящая из некоторой О-сети и гомоморфизма из исходной сети Петри в О-сеть, удовлетворяющего условиям сохранения некоторых аспектов поведения исходной сети Петри в рассматриваемой О-сети. В подразд. 1.1.2 формально определены точки сечения и развертки сетей Петри. Определения точек сечения являются основой для определения критериев финитизации максимального ветвящегося процесса. Развертка сети Петри определяется как конечный префикс ее максимального ветвящегося процесса, полученный с помощью какого-либо критерия финитизации. В разделе описаны некоторые важные свойства полученных разверток. Для описания поведенческих свойств развертки и, в частности, для определения критериев финитизации вводится понятие конфигурации. Конфигурация развертки соответствует последовательности срабатывания исходной сети Петри. Введение понятия конфигурации позволяет рассматривать такие свойства развертки, как безопасность и полнота. Безопасность полученной развертки означает, что любой ее конфигурации соответствует некоторая достижимая разметка сети Петри. Свойство полноты развертки означает, что для любой достижимой разметки исходной сети Петри существует соответствующая ей конфигурация развертки. Подразд. 1.1.3 посвящен описанию двух различных подходов к обнаружению тупиковых состояний в сетях Петри с использованием разверток. Первый подход был предложен МакМиланом в его работах, посвященных определению основных понятий теории разверток сетей Петри и возможностям их применения для верификации свойств распределенных систем. Во втором подходе поведение сети Петри представляется в виде системы линейных неравенств. Тупиковое состояние системы соответствует некоторому специальному решению такой системы.

Разд. 1.2 посвящен описанию раскрашенных сетей Петри. В подразд. 1.2.1 даны основные определения РСП. Модель типов данных РСП базиру-

ется на понятии мультимножества и на определенных над ним операторах и функциях. Понятие мультимножества является основой для определения цветовых множеств (или цветов) РСП. В подразделе описывается функционирование полученной РСП и дается определение достижимой разметки. Также приведен алгоритм построения графа достижимости для заданной РСП, рассматриваемого в дальнейшем в качестве пространства состояний при проведении процедуры проверки моделей (см. разд. 1.3). В подразд. 1.2.2 приводятся определения спецификаций симметрии и эквивалентности на РСП. Спецификация симметрии является частным случаем спецификации эквивалентности и в дальнейших частях работы будет рассмотрена только в контексте более общего случая эквивалентности. В подразд. 1.2.3 описаны РСП, расширенные двумя временными конструкциями. Первая модель представляет собой классическую дискретную модель интервального времени или так называемую модель времени по Мерлину. В данной модели с каждым переходом связывается интервал срабатывания. Переход может сработать, только, когда его временное значение находится в соответствующем интервале срабатывания. Вторая временная модель представляет собой модель временных штампов, введенную К. Йенсеном специально для РСП. В отличие от интервальной временной модели в модели Йенсе-на имеется понятие глобальных часов, посредством которых представляется текущее время. Некоторые множества цветов получают дополнительный временной признак. Элемент РСП, принимающий значение из такого множества, дополнительно несет значение, называемое временным штампом. Оно определяет момент времени, раньше которого данный элемент не может использоваться при срабатывании какого-либо перехода.

В разд. 1.3 описаны методы проверки моделей для двух логических систем: логики линейного времени ШЪ и логики мю-исчисления. В подразд. 1.3.1 формально описаны синтаксис и семантика логики ЦТЦ. В качестве семантической модели описано множество так называемых '«'-слов над некоторым специальным алфавитом. Кроме данной классической семантики приведена интерпретация формул ШЪ на сетях Петри. Описывается подмножество статтерно-эквивалентных формул логики ШЪ. Это подмножество используется в дальнейшем для проведения проверки моделей на сетях Петри с использованием разверток. Подразд. 1.3.2 посвящен описанию логики мю-исчисления. Логика мю-исчисления является логикой ветвящегося времени и благодаря наличию элементов, соответствующих наибольшей и наименьшей неподвижной точке некоторого логического преобразования, представляет собой логическую систему с большой выразительной силой. В качестве семантической модели логики мю-исчисления рассматриваются

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

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

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

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

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

Разд. 2.4 содержит описание метода обнаружения тупиковых состоянии в РСП. Метод формально описан и доказана теорема о корректности применения данного метода к РСП. Основу данного метода составляет описанное в первой главе представление работы стандартной сети Петри в виде системы неравенств. В данном разделе аналогичная система строится для

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

В третьей главе описывается применение метода развертки к раскрашенным сетям Петри, расширенным спецификациями эквивалентности и двумя временными конструкциями. Разд. 3.1 описывает построение разверток РСП в случае имеющейся в сети спецификации эквивалентности. Наличие эквивалентности позволяет дополнительно существенно сократить размер развертки и, таким образом, делает пространство поиска значительно меньше. Доказана теорема о полноте и безопасности полученной развертки. На примерах "Обедающие философы" и "Отправитель - Получатель" показывается дополнительное уменьшение развертки при применении данного подхода. В случае "Обедающих философов" рассматривается симметрия по числу философов. Использование развертки с симметрией не является для данного примера более эффективным, чем построение усеченного графа достижимости. В связи с этим представляет интерес следующий более сложный пример системы "Отправитель - Получатель". Рассматривается абстракция от отправляемых данных, т.е. все данные, отправляемые "Отправителем" "Получателю", считаются идентичными. Для данного примера использование развертки с абстракцией дает гораздо большее уменьшение размера пространства состояний, чем применение данной абстракции к графу достижимости системы. Так, например, при использовании 20 различных экземпляров данных и 20 составляющих компонентов как в системе "Отправителя", так и в системе "Получателя", полный размер графа достижимости составляет 1.73 • 10174, в то время как размер развертки составляет лишь 1.2810й. При использовании упомянутой выше спецификации абстракции от данных размер графа достижимости уменьшается до 5.97 • 1082. Такой размер графа достижимости не позволяет надеяться на проведение полного машинного эксперимента для верификации системы. Размер соответствующей развертки с применением абстракции составляет всего лишь 8.0105, что является уже вполне реальным числом для проведения полностью автоматического эксперимента.

В разд. 3.2 описывается применение метода развертки к РСП с интервальным временем (ИВРСП). В данной временной модели с каждым переходом связывается временной интервал, состоящий из двух натуральных чисел, задающих наиболее раннее и наиболее позднее время срабатывания перехода. Развертка ИВРСП определяется с помощью построения так называемого временного расширения. Временное расширение ИВРСП - это обычная РСП без времени, моделирующая работу временной сети. Для каждого перехода исходной ИВРСП вводятся соответствующие места вре-

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

Разд. 3.3 посвящен определению разверток для РСП с моделью временных штампов (ВРСП). Применяется подход, аналогичный описанному в разд. 3.2. Основная трудность заключается в громоздкости модели временных штампов и, следовательно, в нетривиальности определения временного расширения ВРСП. После определения временного расширения, определяется его усеченная развертка, которая берется в качестве определения для развертки исходной ВРСП. Доказывается теорема о соответствии поведения исходной ВРСП и ее временного расширения. Эта теорема обосновывает корректность описанного подхода к определению разверток ВРСП.

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

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

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

Разд. 43 содержит описание метода проверки моделей на временных раскрашенных сетях Петри. Описанный в разд. 4.1 метод переносится как на РСП с интервальной временной структурой, так и на РСП с временными штампами в качестве временной конструкции. Для указанных двух временных расширений РСП определяется семантика логики линейного времени (LTL) и доказываются теоремы, позволяющие использовать развертки временных РСП для проведения процедуры проверки моделей. Напомним, что развертка временной РСП определяется как усеченная развертка соответствующего временного расширения. Таким образом, для доказательства указанных теорем необходимо доказать следующие два утверждения. Во-первых, временное расширение сохраняет свойства, описываемые формулами LTL, т.е. истинность формулы LTL в РСП эквивалентна ее истинности во временном расширении РСП. Во-вторых, что при построении усеченной развертки мы не теряем информацию, связанную с истинностью или ложностью формул линейной логики. Первое утверждение оформлено в виде теоремы, второе, как более локальный факт, в виде утверждения. В этом разделе приводятся формальные доказательства обоих упомянутых утверждений.

В пятой главе описываются реализации классического подхода к проверке моделей РСП и метода проверки моделей, основанного на развертках. С каждой из систем проведен ряд экспериментов, результаты которых также изложены в данной главе. Разд. 5.1 посвящен описанию реализованных систем проверки моделей для РСП. В подразд. 5.1.1 представлена система верификации PNV (Petri Net Verifier), в которой в качестве логического языка используется мю-исчисление и в качестве модели - граф достижимости РСП. В качестве метода проверки моделей применен стандартный алгоритм проверки моделей для мю-исчисления, описанный в разд. 4.1. В системе PNV имеется ряд возможностей, не используемых в данной работе. Это перевод спецификации РСП в программу на языке СПЕКТР-2 и создание моделирующей программы на языке C++. В качестве входного языка взят язык Standard ML, предложенный в работах К. Йенсена и принятый в качестве стандарта в системе Design/CPN. Спецификация сети на описанном входном языке подается на транслятор, который преобразует ее в интерпре-

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

Разд. 5.2 содержит описание экспериментов, проведенных с двумя, описанными выше, системами. Результаты проведенных экспериментов показали возможность и целесообразность применения метода проверки моделей с использованием разверток для верификации моделей распределенных систем. В подразд. 5.2.1 рассматривается РСП, представляющая задачу об обедающих философах. Для данной сети рассматриваются свойства прогресса и тупиков. Свойства прогресса описывают динамическое поведение системы, например, возможность сколь угодно частого срабатывания некоторых переходов или недопустимость ситуаций, в которых некоторые переходы будут блокированы. Тупиковым называется такое состояние системы, в котором никакое действие не является возможным. Свойства описываются в двух логических системах - логике ШЪ и логике мю-исчисления. Затем полученные спецификации проверяются как с помощью системы РКУ, так и с помощью системы, базирующейся на развертках РСП. В подразд. 5.2.2 рассматривается верификация модели однобитового коммуникационного протокола (АВР). Протокол состоит из частей "Приемник" и "Передатчик", взаимодействующих посредством двух ненадежных каналов. Ненадежность каналов означает, что любой из отправленных пакетов

может быть потерян. Искажения отправленного пакета средой считаются недопустимы. Кроме свойств прогресса и тупиков, описанных выше для случая обедающих философов, для коммуникационного протокола имеет смысл рассматривать, так называемые, свойства безопасности. Свойства безопасности описывают, например, правильный порядок приема сообщений или правильную работу "Приемника" по формированию подтверждений на полученные сообщения. Как свойства прогресса и тупиков, так и свойства безопасности, были описаны в логиках ЬТЬ и мю-исчисления и верифицированы как с помощью системы Р№У, так и с помощью системы, базирующейся на развертках РСП. В подразд. 5.2.3 описана и верифицирована модель кольцевого протокола. Протокол описывает взаимодействие нескольких станций, соединенных в кольцо. По кольцу циркулирует фрейм фиксированной длины. Станция, обладающая в данный момент фреймом, имеет возможность отправить или считать некоторый пакет данных. Протокол является полностью детерминированным, что исключает целесообразность использования для него методов, базирующихся на частичном порядке и, в частности, методов развертки. Данный протокол был верифицирован с использованием системы РКУ. Для кольцевого протокола, помимо проверки свойств прогресса, тупиков и безопасности, был проведен ряд экспериментов, связанных с обнаруженной в работах группой авторов лаборатории теоретического программирования ИСИ СО РАН неэффективностью работы данного протокола. Эта неэффективность также была установлена в экспериментах с системой Р№У и для достаточно общих случаев было показано ее отсутствие при внесении в систему требуемых изменений. В под-разд. 5.2.4 рассматривается модель коммуникационного протокола "Отправитель - Получатель", в которой передача сообщений производится через специальный буфер. Отправка подтверждений о получении сообщений отсутствует. Для данного протокола проверялись свойства прогресса и безопасности. Проведенные эксперименты показали эффективность использования метода проверки моделей с использованием разверток для данного примера.

Основные выводы и результаты. В рамках диссертации были получены следующие результаты.

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

ноты. Приведены два алгоритма построения разверток РСП. Описаны методы обнаружения тупиков в РСП с использованием разверток.

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

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

• Реализован блок проверки моделей в системе PNV. Проведена прото-типная реализация метода проверки моделей с использованием разверток. Проведен ряд экспериментов с системой PNV и системой проверки моделей с использованием разверток.

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

1. Козюра В.Е. Реализация системы проверки моделей раскрашенных сетей Петри с использованием разверток. — Новосибирск, 2002. — 32 с. -(Препр. / Сиб. отд-ние РАН. ИСИ; № 94).

2. Козюра В.Е., Непомнящий В.А., Новиков P.M. Верификация раскрашенных сетей Петри методом проверки моделей. — Новосибирск, 2001. —

24 с. - (Препр. / Сиб. отд-ние РАН. ИСИ; № 89).

3. Козюра В.Е., Новиков P.M. Использование метода проверки моделей для верификации коммуникационных протоколов, представленных раскрашенными сетями Петри // Тез. докл. IV сибирского конгресса по прикладной и индустриальной математике (ИНПРИМ-2000). - Новосибирск, 2000. -Ч. V. - С. 44.

4. Козюра В.Е., Новиков P.M. Верификация коммуникационных протоколов с использованием системы PNV // Материалы молодежной научн. конф., посвященной 10-летию ИВТ СО РАН, Новосибирск, Академгородок,

25 - 26 декабря, 2000.

5. Kozura V.E. Unfoldings of Coloured Petri Nets. - Novosibirsk, 2000. -34p. - (Prepr. / SD RAS IIS; № 80).

6. Kozura V.E. Unfoldings of Coloured Petri Nets // Proc. 4th Internat. A.Ershov Memorial Conf. Perspectives of System Informatics", (PSI'Ol). -Berlin a.o.: Springer-Verlag, 2001. - P. 268-278. - (Lect. Notes Comput. Sci.; Vol. 2244).

7. Kozura V.E. Unfoldings of Timed Coloured Petri Nets. - Novosibirsk, 2001. - 33p. - (Prepr. / SD RAS US; № 82).

8. Kozura V.E. Unfoldings of Timed Coloured Petri Nets // Proc. of the Workshop on Concurrency, Specification and Programming 2001 (CS&P'2OO1), Warsaw 3-5 October 2001. - P. 128-139.

9. Kozura V.E. LTL model checking of coloured Petri nets based on net unfoldings // Joint Bulletin of NCC & IIS. Ser.: Comput. Sci. - 2001. - №15. -P. 83-101.

10. Kozura V.E., Nepomniaschy V.A., Novikov R.M. Verification of Distributed Systems Modelled by High-level Petri Nets // Proc. Internat. Conf. on Parallel Computing in Electrical Engineering (PARELEC 2002), Warsaw, Poland. -IEEE Computer Society, 2002. - P.61-66.

Личный вклад автора.

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

В.Е. Козюра

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

Подписано в печать 27.0 7.04 Формат бумаги 60 х 84 1/16

Объем 1.0 уч.-изд.л. № ЛЯ Тираж 100 экз.

ЗАО РИЦ «Прайс-курьер» 630090, г. Новосибирск, пр. Акад. Лаврентьева, 6, тел. (383-2) 34-22-02

04-142*6

Введение.

Глава

Предварительные понятия.

1.1 Развертки сетей Петри.

1.1.1. Ветвящиеся процессы.

1.1.2. Определения разверток сетей Петри.

1.1.3. Методы обнаружения тупиков.

1.2 Раскрашенные сети Петри.

1.2.1 Общие определения.

1.2.2 Симметрия и эквивалентность.

1.2.3 Раскрашенные сети Петри со временем.

1.2.3.1 Модель интервального времени.

1.2.3.2 Модель временных штампов.

1.3 Метод проверки моделей.

1.3.1 Логика линейного времени.

1.3.2 Логика мю-исчисления.

1.3.3 Алгоритм проверки моделей для логики линейного времени.

1.3.4 Алгоритм проверки моделей для логики мю-исчисления.

Глава

Развертки раскрашенных сетей Петри.

2.1 Ветвящийся процесс для раскрашенных сетей Петри.

2.2 Определения и основные свойства разверток.

2.3 Алгоритмы построения разверток.

2.4 Алгоритмы обнаружения тупиков.

Глава

Развертки раскрашенных сетей Петри, расширенных эквивалентностью и временем.

3.1 Применение эквивалентности в развертках.

3.2 Развертки сетей с интервальным временем.

3.3 Развертки сетей с временными штампами.

Глава

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

4.1 Метод проверки моделей и обоснование его корректности.

4.2 Применение метода проверки моделей к сетям, расширенным свойством эквивалентности.

4.3 Применение метода проверки моделей для временных сетей.

4.3.1 Модель интервального времени.

4.3.2 Модель временных штампов.

Глава

Реализация методов проверки моделей для раскрашенных сетей Петри.

5.1 Системы верификации раскрашенных сетей Петри.

5.1.1 Система PNV.

5.1.2 Реализация метода проверки моделей с использованием разверток. и 5.2 Экспериментальные результаты.

7 5.2.1 Задача об обедающих философах.

5.2.2 Битовый протокол.

5.2.3 Кольцевой протокол.

5.2.4 Протокол "Отправитель - получатель".

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

Теории и приложениям сетей Петри посвящена богатая литература, см., например, [9]. В России велись исследования по моделированию, спецификации и верификации распределенных систем с использованием сетей Петри. Отметим, в частности, работы O.JI. Бандман [2,3] по спецификации поведения сетевых протоколов, Н.А. Анисимова [15] по спецификации протоколов, В.А. Соколова [12] по анализу паралельных программ и И.Б. Вирбицкайте [4] по использованию техники частичного порядка для верификации временных сетей Петри.

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

Последние два десятилетия метод проверки моделей активно развивался в работах многих авторов и показал себя как эффективное и многообещающее средство для верификации распределенных систем. Благодаря своей естественности и возможности быть интегрированным в среду разработки и анализа распределенных систем, метод проверки моделей был принят в качестве одного из стандартов для верификации спецификаций систем, описанных на каком-либо формальном языке. В качестве входных данных для процедуры проверки моделей поступают описание самой системы (чаще всего задаваемое в виде некоторой структуры с конечным числом состояний) и логическая спецификация (обычно, формула временной логики), описывающая проверяемое свойство системы. В качестве формализмов для описания структуры системы чаще всего используются такие модели, как структуры Крипке и помеченные системы переходов [19, 20, 51]. Активно используемые логические спецификации подразделяются на логики линейного времени (LTL) и логики ветвящегося времени. Среди наиболее используемых логик ветвящегося времени следует отметить логику Хеннесси-Милнера, логику модального мю-исчисления, базирующуюся на теории неподвижных точек, и логику вычислимых деревьев (CTL - Computational Tree Logic) [51]. Методы проверки моделей подразделяются на локальную и глобальную проверку моделей. При локальной проверке моделей по заданной логической спецификации и некоторому участку (состоянию) системы необходимо определить, является ли данная спецификация истинной на заданном участке или нет. При глобальной проверке моделей по заданной логической спецификации и описанию системы необходимо определить те состояния системы, в которых формула логической спецификации является истинной. Методы проверки моделей предоставляют полностью автоматический способ решения данных задач. Обзор современного состояния теории проверки моделей можно найти, например, в работе [19].

К сожалению, при полном моделировании работы сети мы сталкиваемся с так называемой "проблемой взрыва числа состояний" (state explosion problem). Эта проблема состоит в том, что при росте размеров рассматриваемой сети, ее полная модель достаточно быстро становится необозримо большой. Это не позволяет надеяться на построение полной модели для реальных протоколов. Отдельным и, как это следует из вышесказанного, достаточно важным направлением верификации распределенных систем является разработка методов, направленных на решение проблемы взрыва числа состояний. Среди таких методов можно выделить следующие: метод упрямых множеств (stubborn set method), использование двоичных разрешающих диаграмм (symbolic binary decision diagrams ), методы, основанные на частичном порядке (partial order methods), а также использование симметрии и эквивалентности на рассматриваемых моделях [54].

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

Среди различных расширений стандартных сетей Петри выделяются сети Петри высокого уровня — раскрашенные сети Петри (РСП) [35, 36], для которых развит теоретический аппарат, накоплен значительный опыт использования и реализована система симуляции и анализа Design/CPN [46]. В РСП вместо обычных фишек используются типизированные знаковые элементы. Также есть возможность задания функций на дугах и переходах. Это расширение позволяет выражать в достаточно компактном виде сложные системы, не теряя при этом возможностей применять методы, разработанные для стандартных сетей Петри. Данная работа посвящена применению метода проверки моделей с использованием разверток к раскрашенным сетям Петри.

Использование разверток для анализа стандартных сетей Петри было предложено МакМилланом в работе [48]. Было предложено использовать конечный префикс максимального ветвящегося процесса вместо полного графа достижимости. Размер развертки является экспоненциальным в общем случае, и в последующих работах были предложены некоторые улучшения определений и алгоритмов построения развертки [25, 45]. Так в работе [25] было предложено рассматривать обобщенное понятие порядка на конфигурациях, и с его помощью, был предложен критерий финитизации, являющийся оптимальным для одно-безопасных сетей Петри. В работе [45] было показано, что для п-безопасных сетей Петри данный критерий не является оптимальным и было предложено существенное улучшение критерия для n-безопасных сетей Петри. В работе [45] также был предложен алгоритм построения развертки, линейно зависящий от произведения числа мест и переходов развертки.

Первоначально МакМиллан предложил использовать развертки для анализа достижимости и обнаружения тупиков. Эти методы были улучшены в последующих работах [31, 50]. В работе [31] предложено улучшение метода определения достижимости данного состояния сети. В работе [50] дается метод обнаружения тупиковых состояний с использованием системы неравенств, описывающих рассматриваемую сеть Петри. Дж. Эспарца в работе [24] предложил метод проверки моделей для одно-безопасных сетей Петри и логики S4 с использованием развертки. В работе [16] для сетей Петри с интервальным временем была построена развертка и применен алгоритм проверки моделей Эспарцы. В работе [57] Ф. Валнер предложил алгоритм проверки моделей для LTL логики, основанный на развертках сети Петри. В его работе известный теоретико-автоматный подход к верификации LTL формул [56] был перенесен на одно-безопасные сети Петри без тупиковых состояний. Этот подход был развит в последующих работах

14, 22, 27, 28, 33]. На последнем этапе алгоритма Валнера строится дополнительный граф, состоящий из точек сечения рассматриваемой развертки. В работах [27, 28] была показана возможность модификации алгоритма, позволяющая избежать построения данного дополнительного графа и описана реализация данного подхода с приведением экспериментальных результатов. Работы [14, 33] посвящены теоретическим аспектам методов проверки моделей с использованием разверток. В работе [33] были доказаны некоторые сложностные оценки алгоритмов проверки моделей с использованием разверток. Работа [14] посвящена рассмотрению возможностей применения методов развертки к неограниченным сетям Петри. Стоит также отметить работу [26], в которой метод развертки был применен к синхронизированному произведению двух сетей Петри.

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

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

- Разработка эффективных методов построения разверток РСП без временных конструкций.

- Исследование метода развертки для РСП, расширенных спецификациями эквивалентности и временными конструкциями.

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

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

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

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

Вся описанная выше работа связана с перенесением методов, разработанных для стандартных сетей Петри на РСП. Однако, описанные в [35, 36] РСП имеют два существенные расширения. Во-первых, благодаря развитому аппарату работы с типами данных (цветами), имеются большие возможности по определению спецификаций симметрии и эквивалентности для РСП, основанные на цветовых значениях. Новым шагом, сделанным в данной работе, является разработка методов развертки РСП, расширенных спецификацией . эквивалентности. Теории построения разверток с использованием отношения эквивалентности не существовало ранее также и для стандартных сетей Петри, хотя некоторый шаг в этом направлении был сделан в работе [53]. Использование таких разверток РСП позволяет дополнительно существенно уменьшить размер рассматриваемой модели. В работе также показано, как можно использовать отношение эквивалентности при проведении проверки моделей с применением разверток. Второй особенностью РСП, отсутствующей в стандартной модели сетей Петри, является применение специальной временной модели, так называемой модели временных штампов. В диссертации показывается возможность применения методов развертки к РСП с временными штампами, а также возможность применения к ним метода проверки моделей для логики LTL. Заметим здесь, что получаемые развертки для РСП с временными штампами являются, в общем случае, бесконечными. Та же проблема возникает и при рассмотрении графа достижимости модели РСП с временными штампами [36]. В работе [36] было предложено использовать спецификации эквивалентности по времени для финитизации графа достижимости. В диссертации предлагается использовать аналогичный подход при построении разверток. Здесь основные методы, развитые в работе, а именно, развертки РСП, развертки РСП, расширенных временными конструкциями, и развертки РСП, расширенные спецификациями эквивалентности, применяются одновременно. В диссертации также показана возможность применения метода проверки моделей к РСП, расширенным спецификациями эквивалентности и временной моделью, основанной на временных штампах.

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

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

Апробация, работы проведена на следующих международных научных конференциях:

1. International Conference on Parallel Computing in Electrical Engineering (PARELEC

2002), Warsaw, Poland.

2. 4th International Conference of Perspectives of System Informatics (PSI'01), Novosibirsk,

Russia, 2001.

3. 5th International Workshop on Concurrency, Specification and Programming, Warsaw,

Poland, 2001.

4. Четвертый Сибирский Конгресс no Прикладной и Индустриальной Математике

ИНПРИМ - 2000), Новосибирск, Россия, 2000.

Кроме того, полученные результаты обсуждались на семинарах лаборатории теоретического программирования ИСИ СО РАН и кафедры систем информатики НГУ.

Публикации. По теме диссертации опубликовано 10 научных работ.

Структура работы. Диссертация состоит из введения, пяти глав, заключения и списка литературы из 57 наименований. Содержание составляет 85 страниц. Работа включает 26 иллюстраций и 4 таблицы.

Заключение

В рамках диссертации были получены следующие результаты.

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

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

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

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

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

1. Ачасова С.М., Бандман O.JL Корректность параллельных вычислительных процессов. Новосибирск: Наука, 1990.252 стр.

2. Бандман О Л. Проверка корректности сетевых протоколов с помощью сетей Петри. Автоматика и вычислительная техника. N 6. 1986. с. 82-91.

3. Вирбицкайте И.Б., Покозий Е.А. Использование техники частичных порядков для верификации временных сетей Петри. Программирование N 1.1999. с.28 — 41.

4. Коз юра В.Е. Реализация системы проверки моделей раскрашенных сетей Петри с использованием разверток. Препринт N 94. Новосибирск 2002. 32 стр.

5. Козюра В.Е., Непомнящий В.А., Новиков P.M. Верификация раскрашенных сетей Петри методом проверки моделей. Препринт N 89. Новосибирск 2001. 24 стр.

6. Козюра В.Е., Новиков P.M. Использование метода проверки моделей для верификации коммуникационных протоколов, представленных раскрашенными сетями

7. Петри. Четвертый сибирский конгресс по прикладной и индустриальной математике (ИНПРИМ 2000). Тезисы докладов. Часть V. Стр. 44.

8. Козюра В.Е., Новиков Р.М. Верификация коммуникационных протоколов с использованием системы PNV. Материалы молодежной научной конференции, посвященной 10-летию ИВТ СО РАН, Новосибирск, Академгородок, 25 26 декабря, 2000.

9. Котов В.Е., Сети Петри. М.Наука, 1984.

10. Соколов В.А., Легалов А.И. Применение сетей Петри для анализа программ, написанных на языке параллельного программирования. Моделирование и анализ информационных систем. Ярославский государственный университет. N 1. 1993. с. 27 -44.

11. Чаплыгин С.М. Верификация распределенных систем, представленных раскрашенными сетями Петри, методом проверки моделей. Выпускная квалификационная работа. НГУ. Новосибирск 2003.

12. Abdulla А.Р., Purushothaman I., Nylen A. Unfoldings of Unbounded Petri Nets. Proc. of CAV 2000. Lect. Notes Comput. Sci. 2000. Vol. 1855. P. 495-507.

13. Anisimov N.A., Kovalenko A.A., Postupalski P.A. Two-levels Formal Model for Protocol Specification Based on Petri Nets. Proc. IFIP TC6 Intern. Symp. Network Information Systems. Bulgaria, 1993. P. 143 -154.

14. Bieber В., Fleischhack H. Model Checking of Time Petri Nets Based on Partial Order Semantics. Proc. CONCUR'99. Lect. Notes Comput. Sci. 1999. Vol. 1664. P. 210-225.

15. Bodin E.V., Kozura V.E., Shilov N.V. Experiments with Model Checking for ц-Calculus in specification and verification project REAL. Proceedings of the Fifth New Zealand Formal Program Development Colloquium. 1999. P. 1-18.

16. Cheng A., Christensen S., Mortensen К. H. Model Checking Coloured Petri Nets Exploiting Strongly Connected Components. DAIMIPB 519, March 1997.

17. Clarke E.M., Grumberg O., Peled D.A. Model Checking, MIT Press, 1999.

18. Cleaveland R., Klein M., Steffen B. Faster Model Cheking for Modal Mu-Calculus. Proc of CAV-92, Mjntreal, Canada. Lect. Notes Comput. Sci. 1992. Vol. 663. P. 410-422.

19. Cohen R., Segall A. An efficient reliable ring protocol. IEEE Transact. Communs. 1991. Vol.39, N.ll.P.l 616-1624.

20. Couvreur J.-M., Grivet S., Poitrenaud D. Designing an LTL Model-Checker Based on Unfolding Graphs. Lect. Notes Comput. Sci. 2000. Vol. 1825. P. 123-145.

21. Engelfriet J. Branching Processes of Petri Nets. Acta Informatica. 1991. Vol. 28. P. 575591.

22. Esparsa J. Model-Checking Using Net Unfoldings. Lect. Notes Comput. Sci. 1993. Vol. 668. P. 613-628.

23. Esparsa J., Romer S., Volger W. An Improvement of McMillan's Unfolding Algorithm. Proc. TACAS'96. Lect. Notes Comput. Sci. 1997. Vol. 1055. P. 87-106.

24. Esparsa J., Romer S. An unfolding algorithm for synchronous product of transition systems. In Proc. of CONCUR'99. Lect. Notes Comput. Sci. 1999. Vol. 1664. P. 2-20.

25. Esparza J., Heljanko K. A New Unfolding Approach to LTL Model-Checking. Lect. Notes Comput. Sci. 2000. Vol. 1853. P. 475^86.

26. Esparza J., Heljanko K. Implementing LTL Model Checking with Net Unfoldings. Lect. Notes Comput. Sci. 2001. Vol. 2057. P. 37-56.

27. Farwer В., Lomazova I. A Systematic Approach towards Object-based Petri Net Formalisms Proc.PSI 2001, Lecture Notes Comput. Sci. 2001. Vol. 2244. P. 255-267.

28. Gerth R., Peled D., Vardi M., Wolper P. Simple On-the-fly Automatic Verification of Lineal Temporal Logic. In Protocol Specification, Testing, and Verification PSTV'95. 1995. P. 3-18.

29. Godefroid P., Wolper P. Using partial orders for the efficient verification of deadlock freedom and safety properties. Formal Methods in System Design, 2(2). 1993. P. 149-164.

30. Graves B. Computing reachability properties hidden in finite net unfoldings. Lect. Notes Comput. Sci. 1997. Vol. 1346. P. 327-341.

31. Heljanko K. Model Checking with Finite Complete Prefixes is PSPACE-Complete. Proc. of CONCUR'2000. Lect. Notes Comput. Sci. 2000. Vol. 1877. P. 108-122.

32. Holzmann G. I. Design and validation of computer protocols. Englewood Cliffs, NJ: Prentice Hall, 1991.

33. Jensen K. Coloured Petri Nets. Vol. 1. — Berlin a.o.: Springer, 1995.

34. Jensen K. Coloured Petri Nets. Vol. 2. — Berlin a.o.: Springer, 1995.

35. Kaivola R. Using compositional preorders in the verification of sliding window protocol. In Proc. of CAV'97, Lecture Notes Comput. Sci. Vol. 1254, P. 48-59.

36. Khomenko V., Koutny M., Vogler W. Canonical Prefixes of Petri Net Unfoldings. Proc. of CAV 2002, Lecture Notes Comput. Sci. 2002. Vol. 2404, P. 582=59^—

37. Kozura V.E. Unfoldings of Coloured Petri Nets. Tech. Rep. N80. Novosibirsk 2000. 34 pages.

38. Kozura V.E. Unfoldings of Coloured Petri Nets. Proc. of Perspectives of System Informatics 2001 (PSI'01), Lect. Notes Comput. Sci. 2001. Vol 2244. P. 268-278.

39. Kozura V.E. Unfoldings of Timed Coloured Petri Nets. Tech. Rep. N82. Novosibirsk 2001. 33 pages.

40. Kozura V.E. Unfoldings of Timed Coloured Petri Nets. Proceedings of the Workshop on Concurrency, Specification and Programming 2001 (CS&P'2001) Warsaw 3-5 October 2001. P. 128-139.

41. Kozura V.E. LTL model checking of coloured Petri nets based on net unfoldings. Joint Bulletin of,the Novosibirsk Computing Center and A.P.Ershov Institute of Informatics Systems, Series: Computer Science, V.15. Novosibirsk, 2001. P. 83-101.

42. Kristensen L.M., Christensen S., Jensen K. The practitioner's guide to coloured Petri nets. Intern. Journal on Software Tools for Technology Transfer. 1998. Vol.2, N 2. P. 98-132.

43. Lamport L. What good is temporal logic? Information Processing 83.1983. P.657-668.

44. McMillan K.L. Using Unfolding to Avoid the State Explosion Problem in the Verification of Asynchronous Circuits. Lect. Notes Comput. Sci. 1992. Vol.663. P. 164-174.

45. McMillan K.L. A technique of a state space search based on unfoldings. Formal Methods in System Design, 6(1). 1995. P. 45-65.

46. Melzer S., Romer S. Deadlock Checking Using Net Unfoldings. Proc. of the Conf. on Computer Aided Verification (CAV'97), Haifa 1997. Lect. Notes Comput. Sci. Vol.1254. P. 352-363.

47. Mueller-Olm M., Schmidt D., Stefen B. Model-Checking. A Tutorial Introduction. Lect. Notes Comput. Sci. 1999. Vol. 1694. P. 330-354.

48. V. A. Nepomniaschy, Nikolay V. Shilov, E. V. Bodin, Vitaly E. Kozura: Basic-REAL: Integrated Approach for Design, Specification and Verification of Distributed Systems. IFM 2002. P. 69-88.

49. Schmidt K. How to calculate symmetries of Petri nets. Acta Informatica 36. 2000. P. 545590.

50. Valmari A. The State Explosion Problem. Lect. Notes Comput. Sci. 1998. Vol. 1491. P. 429528.

51. Valmari A. Stubborn Sets of Coloured Petri Nets. Proc. of the 12th Intern. Conf. on Application and Theory of Petri Nets. Gjern, 1991. P. 102-121.

52. Vardy M.Y., Wolper P. An automata-theoretic approach to automatic program verification. In Proc. of 1st IEEE Symp. on Logic in Computer Science. 1986. P. 322-331.

53. Wallner F. Model-Checking LTL Using Net Unfoldings. Proc. of the Conf. on Computer Aided Verification (CAV'95), Vancouver, 1995. Lect. Notes Comput. Sci. 1998. Vol. 1427. P. 207-218.