авторефераты диссертаций БЕСПЛАТНАЯ  БИБЛИОТЕКА

АВТОРЕФЕРАТЫ КАНДИДАТСКИХ, ДОКТОРСКИХ ДИССЕРТАЦИЙ

<< ГЛАВНАЯ
АГРОИНЖЕНЕРИЯ
АСТРОНОМИЯ
БЕЗОПАСНОСТЬ
БИОЛОГИЯ
ЗЕМЛЯ
ИНФОРМАТИКА
ИСКУССТВОВЕДЕНИЕ
ИСТОРИЯ
КУЛЬТУРОЛОГИЯ
МАШИНОСТРОЕНИЕ
МЕДИЦИНА
МЕТАЛЛУРГИЯ
МЕХАНИКА
ПЕДАГОГИКА
ПОЛИТИКА
ПРИБОРОСТРОЕНИЕ
ПРОДОВОЛЬСТВИЕ
ПСИХОЛОГИЯ
РАДИОТЕХНИКА
СЕЛЬСКОЕ ХОЗЯЙСТВО
СОЦИОЛОГИЯ
СТРОИТЕЛЬСТВО
ТЕХНИЧЕСКИЕ НАУКИ
ТРАНСПОРТ
ФАРМАЦЕВТИКА
ФИЗИКА
ФИЗИОЛОГИЯ
ФИЛОЛОГИЯ
ФИЛОСОФИЯ
ХИМИЯ
ЭКОНОМИКА
ЭЛЕКТРОТЕХНИКА
ЭНЕРГЕТИКА
ЮРИСПРУДЕНЦИЯ
ЯЗЫКОЗНАНИЕ
РАЗНОЕ
КОНТАКТЫ

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

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

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

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

В.Е. Козюра РАЗВЕРТКИ РАСКРАШЕННЫХ СЕТЕЙ ПЕТРИ И ИХ ПРИМЕНЕНИЕ ДЛЯ ВЕРИФИКАЦИИ МОДЕЛЕЙ РАСПРЕДЕЛЕННЫХ СИСТЕМ 05.13.11 математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей

Автореферат Диссертации на соискание ученой степени кандидата физико-математических наук Новосибирск 2004

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

Научный консультант: кандидат физико-математических наук Непомнящий В.А.

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

Ведущая организация: Ярославский государственный университет (г. Ярославль)

Защита состоится _года в час. мин. на заседа нии диссертационного совета Д003.060.01 при Объединенном институте информатики Сибирского отделения РАН по адресу:

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

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

Автореферат разослан 2004 г.

Ученый секретарь Специализированного совета Д003.060. д.ф.-м.н. Л. В. Чубаров

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

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

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

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

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

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

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

Бибер, Х. Фляйшхак, Ф. Валнер, и др. Кроме существенных улучшений алгоритмов и критериев построения развертки был разработан метод про верки моделей первоначально Дж. Эспарцой для логики S4, а впоследствии Ф. Валнером для логики линейного времени LTL. Алгоритмы проверки моделей для логики LTL с использованием разверток были развиты в по следующих работах. В работах В. Бибера и Х. Фляйшхака метод развертки и метод проверки моделей Эспарцы был применен к сетям Петри с интер вальным временем.



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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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





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

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

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

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

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

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

4th International Conference of Perspectives of System Informatics (PSI'01), Novosibirsk, Russia, 2001;

5th International Workshop on Concurrency, Specification and Program ming, 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. описаны РСП, расширенные двумя временными конструкциями. Первая модель представляет собой классическую дискретную модель интервально го времени или так называемую модель времени по Мерлину. В данной модели с каждым переходом связывается интервал срабатывания. Переход может сработать, только, когда его временное значение находится в соот ветствующем интервале срабатывания. Вторая временная модель представ ляет собой модель временных штампов, введенную К. Йенсеном специаль но для РСП. В отличие от интервальной временной модели в модели Йен сена имеется понятие глобальных часов, посредством которых представля ется текущее время. Некоторые множества цветов получают дополнитель ный временной признак. Элемент РСП, принимающий значение из такого множества, дополнительно несет значение, называемое временным штам пом. Оно определяет момент времени, раньше которого данный элемент не может использоваться при срабатывании какого-либо перехода.

В разд. 1.3 описаны методы проверки моделей для двух логических систем: логики линейного времени LTL и логики мю-исчисления. В под разд. 1.3.1 формально описаны синтаксис и семантика логики LTL. В каче стве семантической модели описано множество так называемых w-слов над некоторым специальным алфавитом. Кроме данной классической семанти ки приведена интерпретация формул LTL на сетях Петри. Описывается подмножество статтерно-эквивалентных формул логики LTL. Это подмно жество используется в дальнейшем для проведения проверки моделей на сетях Петри с использованием разверток. Подразд. 1.3.2 посвящен описа нию логики мю-исчисления. Логика мю-исчисления является логикой вет вящегося времени и благодаря наличию элементов, соответствующих наи большей и наименьшей неподвижной точке некоторого логического преоб разования, представляет собой логическую систему с большой выразитель ной силой. В качестве семантической модели логики мю-исчисления рас сматриваются структуры Крипке. В подразд. 1.3.3 приведены классический алгоритм проверки моделей для автоматных сетей и его адаптация для стандартных сетей Петри. В данном подходе логическая формула также представляется в виде автоматной системы (так называемый автомат Бю хи), и суждение об истинности или ложности данной формулы делается на основе произведения системного автомата и автомата Бюхи, представляю щего отрицание рассматриваемой формулы. В подразд. 1.3.4 приведено описание классического алгоритма проверки моделей для логики мю исчисления. Сложность данного алгоритма является экспоненциальной, что объясняется сложностью вычисления значения формулы мю-исчисления.

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

Во второй главе описываются развертки раскрашенных сетей Петри.

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

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

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

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

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

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

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

На примерах “Обедающие философы” и “Отправитель - Получатель” пока зывается дополнительное уменьшение развертки при применении данного подхода. В случае “Обедающих философов” рассматривается симметрия по числу философов. Использование развертки с симметрией не является для данного примера более эффективным, чем построение усеченного графа достижимости. В связи с этим представляет интерес следующий более сложный пример системы “Отправитель - Получатель”. Рассматривается абстракция от отправляемых данных, т.е. все данные, отправляемые “От правителем” “Получателю”, считаются идентичными. Для данного примера использование развертки с абстракцией дает гораздо большее уменьшение размера пространства состояний, чем применение данной абстракции к гра фу достижимости системы. Так, например, при использовании 20 различ ных экземпляров данных и 20 составляющих компонентов как в системе “Отправителя”, так и в системе “Получателя”, полный размер графа дости жимости составляет 1.7310174, в то время как размер развертки составляет лишь 1.281011. При использовании упомянутой выше спецификации абст ракции от данных размер графа достижимости уменьшается до 5.971082.

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

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

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

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

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

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

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

3.1, рассматриваемого произведения для проведения проверки моделей.

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

Разд. 4.3 содержит описание метода проверки моделей на временных раскрашенных сетях Петри. Описанный в разд. 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 дается описание реализации сис темы проверки моделей для логики линейного времени с использованием разверток. Система является прототипной реализацией и в отличие от сис темы PNV не является полностью автоматической. Целью реализации дан ной системы было показать возможность реализации эффективного метода проверки моделей для РСП и привести несколько примеров верификации моделей распределенных систем. На вход системе поступает произведение системной РСП и автоматной РСП, представляющей отрицание логической спецификации и критерий финитизации максимального ветвящегося про цесса. Для данного произведения система строит соответствующую раз вертку и граф, состоящий из точек сечения развертки. Структура получен ного графа, а именно, наличие или отсутствие в нем сильно связных ком понент, является критерием истинности или ложности логической специ фикации на рассматриваемой сети.

Разд. 5.2 содержит описание экспериментов, проведенных с двумя, описанными выше, системами. Результаты проведенных экспериментов показали возможность и целесообразность применения метода проверки моделей с использованием разверток для верификации моделей распреде ленных систем. В подразд. 5.2.1 рассматривается РСП, представляющая задачу об обедающих философах. Для данной сети рассматриваются свой ства прогресса и тупиков. Свойства прогресса описывают динамическое поведение системы, например, возможность сколь угодно частого срабаты вания некоторых переходов или недопустимость ситуаций, в которых неко торые переходы будут блокированы. Тупиковым называется такое состоя ние системы, в котором никакое действие не является возможным. Свойст ва описываются в двух логических системах логике LTL и логике мю исчисления. Затем полученные спецификации проверяются как с помощью системы PNV, так и с помощью системы, базирующейся на развертках РСП. В подразд. 5.2.2 рассматривается верификация модели однобитового коммуникационного протокола (ABP). Протокол состоит из частей "При емник" и "Передатчик", взаимодействующих посредством двух ненадеж ных каналов. Ненадежность каналов означает, что любой из отправленных пакетов может быть потерян. Искажения отправленного пакета средой счи таются недопустимы. Кроме свойств прогресса и тупиков, описанных выше для случая обедающих философов, для коммуникационного протокола имеет смысл рассматривать, так называемые, свойства безопасности. Свой ства безопасности описывают, например, правильный порядок приема со общений или правильную работу "Приемника" по формированию подтвер ждений на полученные сообщения. Как свойства прогресса и тупиков, так и свойства безопасности, были описаны в логиках LTL и мю-исчисления и верифицированы как с помощью системы PNV, так и с помощью системы, базирующейся на развертках РСП. В подразд. 5.2.3 описана и верифициро вана модель кольцевого протокола. Протокол описывает взаимодействие нескольких станций, соединенных в кольцо. По кольцу циркулирует фрейм фиксированной длины. Станция, обладающая в данный момент фреймом, имеет возможность отправить или считать некоторый пакет данных. Про токол является полностью детерминированным, что исключает целесооб разность использования для него методов, базирующихся на частичном порядке и, в частности, методов развертки. Данный протокол был верифи цирован с использованием системы PNV. Для кольцевого протокола, по мимо проверки свойств прогресса, тупиков и безопасности, был проведен ряд экспериментов, связанных с обнаруженной в работах группой авторов лаборатории теоретического программирования ИСИ СО РАН неэффек тивностью работы данного протокола. Эта неэффективность также была установлена в экспериментах с системой PNV и для достаточно общих слу чаев было показано ее отсутствие при внесении в систему требуемых изме нений. В подразд. 5.2.4 рассматривается модель коммуникационного про токола “Отправитель – Получатель”, в которой передача сообщений произ водится через специальный буфер. Отправка подтверждений о получении сообщений отсутствует. Для данного протокола проверялись свойства про гресса и безопасности. Проведенные эксперименты показали эффектив ность использования метода проверки моделей с использованием разверток для данного примера.

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

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

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

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

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

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

ПУБЛИКАЦИИ ПО ТЕМЕ ДИССЕРТАЦИИ 1. Козюра В.Е. Реализация системы проверки моделей раскрашенных сетей Петри с использованием разверток. — Новосибирск, 2002. — 32 с. – (Препр. / Сиб. отд-ние РАН. ИСИ;

№ 94).

2. Козюра В.Е., Непомнящий В.А., Новиков Р.М. Верификация раскра шенных сетей Петри методом проверки моделей. — Новосибирск, 2001. — 24 с. – (Препр. / Сиб. отд-ние РАН. ИСИ;

№ 89).

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

4. Козюра В.Е., Новиков Р.М. Верификация коммуникационных прото колов с использованием системы 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'01). – 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 IIS;

№ 82).

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

9. Kozura V.E. LTL model checking of coloured Petri nets based on net un foldings // 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 Dis tributed Systems Modelled by High-level Petri Nets // Proc. Internat. Conf. on Parallel Computing in Electrical Engineering (PARELEC 2002), Warsaw, Po land. –IEEE Computer Society, 2002. – P.61–66.

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

В.Е. Козюра РАЗВЕРТКИ РАСКРАШЕННЫХ СЕТЕЙ ПЕТРИ И ИХ ПРИМЕНЕНИЕ ДЛЯ ВЕРИФИКАЦИИ МОДЕЛЕЙ РАСПРЕДЕЛЕННЫХ СИСТЕМ Подписано в печать 15.12.03 Объем 1.0 уч.-изд.л.

Формат бумаги 60 84 1/16 Тираж 100 экз.

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

 

Похожие работы:





 
2013 www.netess.ru - «Бесплатная библиотека авторефератов кандидатских и докторских диссертаций»

Материалы этого сайта размещены для ознакомления, все права принадлежат их авторам.
Если Вы не согласны с тем, что Ваш материал размещён на этом сайте, пожалуйста, напишите нам, мы в течении 1-2 рабочих дней удалим его.