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

• Автор: Козюра, В.Е.
• Шифр специальности: 05.13.11
• Научная степень: Кандидатская
• Год защиты: 2004
• Место защиты: Новосибирск
• Количество страниц: 85 с. : ил.

Содержание
Введение

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

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
Развертки раскрашенных сетей Петри.
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 Система РГ4У
5.1.2 Реализация метода проверки
моделей с использованием разверток.
5.2 Экспериментальные результаты
5.2.1 Задача об обедающих философах.
5.2.2 Битовый протокол
5.2.3 Кольцевой протокол
5.2.4 Протокол Отправитель получатель.
Заключение.
Литература


В работе [] дается метод обнаружения тупиковых состояний с использованием системы неравенств, описывающих рассматриваемую сеть Петри. Дж. Эспарца в работе [] предложил метод проверки моделей для одно-безопасных сетей Петри и логики S4 с использованием развертки. В работе [] для сетей Петри с интервальным временем была построена развертка и применен алгоритм проверки моделей Эспарцы. В работе [] Ф. Валнер предложил длгоритм проверки моделей для LTL логики, основанный на развертках сети Петри. В его работе известный теоретикоавтоматный подход к верификации LTL формул [] быт перенесен на одно-безопасные сети Петри без тупиковых состояний. На последнем этапе алгоритма Валнера строится дополнительный граф, состоящий из точек сечения рассматриваемой развертки. В работах [, ] была показана возможность модификации алгоритма, позволяющая избежать построения данного дополнительного графа и описана реализация данного подхода с приведением экспериментальных результатов. Работы [, ] посвящены теоретическим аспектам методов проверки моделей с использованием разверток. В работе [] были доказаны некоторые сложностные оценки алгоритмов проверки моделей с использованием разверток. Работа [] посвящена рассмотрению возможностей применения методов развертки к неограниченным сетям Петри. Стоит также отмстить работу [], в которой метод развертки был применен к синхронизированному произведению двух сетей Петри. Развертка РСП без применения критериев финитизации в общем случае была рассмотрена в работе [] для использования её в методе упрямых множеств. В этой работе, помимо отсутствия финитизации, также использовалось старое представление раскрашенных сетей Петри. Все это заставило автора сделать вывод о неэффективности использования разверток РСП, и в его дальнейших работах было показано, как применять метод упрямых множеств для РСП без построения развертки. Развертки РСП не рассматривались более в литературе. Хотя для стандартных сетей Петри были развиты критерии финитизации, эффективные алгоритмы построения разверток, техника работы со свойством достижимости и по обнаружению тупиков, а также алгоритмы проверки моделей дтя логики 1ЛЪ, возможность применения данной техники к РСП оставалась открытым вопросом. Цель диссертации состоит в разработке эффективных методов и алгоритмов верификации моделей распределенных систем, базирующихся на раскрашенных сетях Петри. Разработка эффективных методов построения разверток РСП без временных конструкций. Исследование метода развертки для РСП, расширенных спецификациями эквивалентности и временными конструкциями. Разработка метода проверки моделей с использованием разверток РСП, расширенных спецификациями эквивалентности и временными конструкциями. Реализация разработанных методов и проведение экспериментов, подтверждающих, что метод развертки РСП является эффективным и может быть применен для верификации моделей распределенных систем. Методы исследований базируются как на применении аппарата сетей Петри, так и на алгоритмах и методах теории проверки моделей. В области сетей Петри используются теория раскрашенных сетей Петри и методы разверток стандартных сетей Петри. В диссертациионой работе формально строится максимальный ветвящийся процесс для РСП, используя их современное представление [, ], и конструктивно доказывается его существование. В работе определены развертки РСП как конечный префикс максимального ветвящегося процесса, полученный с помощью некоторого критерия финитизации, для которых доказываются свойства конечности, безопасности и полноты. Первое свойство дает нам конечность развертки, полученной при применении трех заданных критериев финитизации. Второе гарантирует отсутствие в развертках лишней информации о поведении РСП. Третье свойство дает нам существование во всех трех типах развертки полной информации о графе достижимости РСП. Методы финитизации, разработанные для стандартных сетей Петри, были применены дтя построенного максимального ветвящегося процесса РСП. В работе описаны два алгоритма построения разверток РСП и даны оценки сложности данных алгоритмов.