Спецификация и анализ распределенных систем с использованием инструментальных средств, поддерживающих модели сетей Петри тема диссертации и автореферата по ВАК РФ 05.13.11, кандидат физико-математических наук Быстров, Александр Васильевич

• Быстров, Александр Васильевич
• кандидат физико-математических наук
• 2008

Оглавление диссертации кандидат физико-математических наук Быстров, Александр Васильевич

Введение

1 Модели СП и инструментальные средства, поддерживающие СП

1.1 Основные определения теории СП.

1.2 Свободные СП.

1.3 Регулярные и иерархические СП.

1.3.1 Алгебра регулярных сетей

1.3.2 Иерархические сети

1.4 Временные СП.

1.4.1 Дискретно-временные СП.

1.4.2 Непрерывно-временные СП.

1.5 Раскрашенные СП.

1.5.1 Неиерархические раскрашенные сети Петри

1.5.2 Временные раскрашенные СП

1.5.3 Раскрашенные СП с приоритетами.

1.5.4 Иерархические раскрашенные СП.

1.6 Обсуждение возможностей инструментальных средств, поддерживающих сетевые модели

2 Сетевые средства спецификации управления в языке параллельного программирования Барс

2.1 Структуры управления.

2.2 Типы управления.

2.2.1 Описание типов управления.

2.2.2 Программирование с типами управления.

2.3 Базовый язык асинхронного параллельного программирования Барс.

2.4 С-язык.

2.5 Программная симуляция иерархических сетей с ожиданием

3 Анализ временных сетевых моделей посредством системы RT-MEC

3.1 Структурный анализ ВСП

3.1.1 Теоретическое обоснование.

3.1.2 Анализ живости НВСП.

3.1.3 Анализ на основе ^-компонент.

3.1.4 Анализ на основе Т-компонент.

3.2 Семантический анализ ВСП.

3.2.1 Семантика ДВСП в терминах временных первичных структур событий.

3.2.2 Семантика НВСП в терминах временных локальных структур событий.

3.3 Концепции, организация и возможности системы RT-MEC

3.3.1 Структура и функции.

3.3.2 Реализация и эксперименты.

4 Проектирование, симуляция и валидация иерархических временных раскрашенных сетевых моделей посредством системы XNES

4.1 ИВТ-сети.

4.2 Особенности структурной и функциональной организации системы XNES.

4.2.1 Графический редактор.

4.2.2 Симулятор

4.2.3 Трассировщик

4.2.4 Визуализатор.

4.2.5 Подключаемые модули (плагины)

4.2.6 Эксперименты

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

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

Сети Петри — одна из наиболее популярных моделей параллельных систем, используемых как для теоретических исследований, так и практических применений в различных областях — распределенных баз данных и операционных систем, архитектур вычислительных машин, систем и сетей, систем программного обеспечения, протоколов коммуникаций, семантики параллельных языков, систем с элементами искусственного интеллекта и т.д. Модели сетей Петри играют такую же важную роль в изучении параллельных систем, что и конечные автоматы для последовательных. К достоинствам сетей Петри относятся наглядное графическое представление их структуры и эффективные методы анализа их поведения. В течение четырех последних десятилетий теория сетей Петри породила большое разнообразие моделей, теорем, алгоритмов и инструментов, предназначенных для спецификации, разработки и верификации параллельных/распределенных систем. Складываются устойчивые системы базовых понятий и общепринятых методик, появляются специальные периодические издания, регулярно проводятся научные конференции, посвященные данной тематике. С помощью сетевых моделей установлен ряд фундаментальных фактов, которые позволили лучше понять природу параллельных вычислений. Так, выделены три базовых отношения между событиями параллельных систем: причинная зависимость, параллелизм и недетерминированный выбор (конфликт). С одной стороны, дальнейшее продвижение в данной области связано с изучением обоснованных с теоретической точки зрения подклассов сетевых моделей (например, элементарных сетевых систем (elementary net systems), систем с условиями/событиями (condition/event systems), сетей со свободным выбором (free choice nets), позволяющих рассматривать сети Петри как математические объекты и формально исследовать их свойства, правила конструирования и преобразования. С другой стороны, появились различные расширения сетей Петри: разнообразные модели временных и стохастических сетей, сети с предикатами (predicate/transition nets), сети Петри с раскрашенными фишками (coloured Petri nets) и т. д., призванные служить математическим инструментом для моделирования и анализа реальных параллельных систем со сложной структурной организацией. Кроме того, в настоящее время также разрабатывается целый ряд инструментальных систем, основанных на моделях сетей Петри.

Среди отечественных исследований по спецификации, моделированию и анализу сложных (в том числе, параллельных/распределенных) систем отметим работы Н.А. Анисимова, О.Л. Бандман, И.Б. Вирбицкайте, В.В. Воеводина, Н.В. Евтушенко, В.А. Захарова, Ю.Г. Карпова, В.Е. Котова, И.А. Ломазовой, В.А Малышкина, В.А. Непомнящего, А.К. Петренко, Р.Л. Смелянского, В.А. Соколова, Л.А. Черкасовой.

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

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

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

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

3. развитие и совершенствование методов исследования взаимосвязей различных поведенческих моделей и моделей реального времени в семантике "истинного параллелизма";

4. эффективный анализ, моделирование и валидация иерархических и временных расширений моделей СП.

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

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

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

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

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

• алгоритмы структурного и семантического анализа систем реального времени, представленные временными сетями Петри,

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

Практическая значимость. Результаты диссертации были успешно реализованы в рамках транслятора языка параллельного программирования Барс, а также экспериментальных систем XNES (extensible NEtworks Simulator) и RT-MEC (Real-Time Model and Equivalence Checker), которые поддерживают различные методы проектирования, анализа, валидации сложных распределенных систем и систем реального времени, представленных различными сетевыми моделями.

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

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

Представление работы. Основные идеи и конкретные результаты диссертационной работы обсуждались на следующих международных научных симпозиумах, конференциях и семинарах: 2-й Международный симпозиум по информатике в России (Екатеринбург, 2007). 13th Intern. Workshop " Concurrency: Specification and Programming" (Berlin, 2004); 1-ая и 2-ая Всероссийская научная конференция "Методы и средства обработки информации" (Москва: МГУ, 2003, 2005); 4-ый Сибирский Конгресс "Прикладная и Индустриальная Математика" (Новосибирск, 2000); Международный семинар "Распределенная обработка информации" (Новосибирск, 1998); 1st Intern. Workshop "Formal Description Technique, ESTELLE'98" (Evry, France, 1998);

Intern. Workshop "Discrete Event Systems" (Cagliari, Italy, 1998); Intern. Conference "Parallel Computing in Electrical Engineering" (Bialystok, Poland, 1998); 3rd Intern. Conference "Parallel Computing Technologies" (St. Petersburg, Russia, 1995, 1999); 1-ая Всесоюзная конференция "Проблемы создания супер-ЭВМ, супер-систем и эффективность их применения (Минск, 1987))"; 4th Int. Conference of Young Computer Scientists (Bratislava, 1984);

Кроме того, доклады по теме работы были сделаны на ряде семинаров Института информатики Университета г. Хильдесхайма (Германия), Института прикладной математики (г. Гренобль, Франция), Института кибернетики (г. Киев), Института программных систем РАН (г. Переславль-Залесский), Института математики СО РАН (г. Новосибирск), Института систем информатики СО РАН (г. Новосибирск), кафедр Новосибирского государственного университета и др.

Публикации. По теме диссертации опубликовано 30 научных работ, в том числе 3 в изданиях, рекомендуемых ВАК РФ; 1 монография; 9 в трудах международных симпозиумов, конференций и семинаров; 5 в трудах национальных симпозиумов, конференций и семинаров; 9 в сборниках научных трудов.

Участие в проектах и грантах. Результаты исследований, изложенные в диссертации, легли в основу ряда научно-исследовательских проектов, поддержанных в разные годы различными грантами Российского фонда фундаментальных исследований (гранты 93-01-00986, 96-01-01655, 00-01-00898, 03-07-90331, 07-07-00173), Фондом фирмы Фольксваген (грант 1/70 564), Фондом ИНТАС (грант 1010-СТ93-0048), Фондом ИНТАС-РФФИ (грант 95-0378) и др.

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

Во всех работах опубликованных в соавторстве автор участвовал в постановке задач, разработке методов решения и анализе результатов. Также в работах [8,10,11,1317] диссертантом предложены синтаксис и семантика подъязыка управления языка Барс, алгоритмы управления вычислениями и программно реализованы соответствующие компоненты транслятора и симулятора. Результаты, изложенные в работах [6,44,45] получены автором самостоятельно, за исключением того, что разработка структуры и функций системы RT-MEC была выполнена совместно с И.Б. Вирбиц-кайте. В работах [1,24-29,33,90-94] диссертант принимал участие в создании модели ИВТ-сетей, им сформулированы требования и разработана архитектура программных комплексов XNES/SPV; он также участвовал в их программной реализации и отладке. Работы [9,7,12] написаны в неделимом соавторстве.

Структура и объем работы. Диссертация состоит из введения, четырех глав, заключения, списка литературы и приложения. Общий объем диссертации 136 е., основной текст - 126 е., приложение - 10 е., библиографический список - 121 наименование. Работа содержит 36 рисунков и 11 таблиц.

Заключение диссертации по теме «Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей», Быстров, Александр Васильевич

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

• Разработан и реализован программный комплекс XNES (eXtended Net Editor , and Simulator), предназначенный для проектирования, симуляции и валидации распределенных систем, представленных моделями ИВТ-сетей (модификациями иерархических временных раскрашенных сетей Петри). Комплекс XNES базируется на мультиплатформенном языке Python, открытой библиотеке Petri Net Kernel и открытом формате хранения PNML (Petri Net Markup Language). XNES включает следующие основные модули: графический редактор для построения сетевых моделей; симулятор для имитационного моделирования и отладки ИВТ-сетей; трассировщик для протоколирования сеанса симуляции; ви-зуализатор для построения высоко-уровневой визуализационной модели протокола; подключаемые модули (плагины) для расширения возможностей системы XNES.

• С использованием системы XNES проведены эксперименты с рядом протоколов коммуникаций с целью анализа их корректности. В частности, исследовались сетевые модели таких протоколов, как InRes, ATMR, RE и i-протокол.

Заключение

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

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

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

• Разработан и реализован программный комплекс XNES (extended Net Editor and Simulator), являющийся одним из основных компонент системы SPV (SDL Protocol Verifier), предназначенной для проектирования, анализа и верификации протоколов коммуникаций, представленных моделями ИВТ-сетей (модификациями иерархических временных раскрашенных сетей Петри). С помощью комплекса проведены эксперименты с рядом протоколов коммуникаций с целью анализа их корректности, включая сетевые модели таких известных протоколов, как InRes-протокол, ATMR-протокол, i-протокол и кольцевой протокола RE.

Список литературы диссертационного исследования кандидат физико-математических наук Быстров, Александр Васильевич, 2008 год

1. Алексеев Г.И., Быстров А.В., Мыльников С.П., Реализация системы проектирования сетевых моделей в MS-WINDOWS // Сб.: Проблемы теоретического и экспериментального программирования. Новосибирск: ВЦ СО АН СССР, 1993. - С. 73-80.

2. Ачасова С.М., Бандман O.JI. Корректность параллельных вычислительных процессов. Новосибирск: Наука, 1990. - 252с.

3. Быстров А.В. Синхросети средство описания взаимодействия асинхронных процессов // Proc. 4th International Conference of Young Computer Scientists. - Bratislava, 1984. - P. 52-56.

4. Быстров А.В. Сетевые средства синхронизации процессов // Тр. Всесоюзного научно-технического семинара "Программное обеспечение многопроцессорных систем". Калинин, 1985. - С. 44-46.

5. Быстров А.В. Структурный анализ поведения непрерывно-временных сетей Петри // Препринт ИСИ СО РАН ССР. № 137. - Новосибирск: ИСИ СО РАН, - 2006. - 30 с.

6. Быстров А.В., Вирбицкайте И.Б. Автоматический анализ и верификация распределенных систем реального времени // Труды 6-ого межд. семинара "Распределенная обработка информации" (РОИ'98 & DDP'98). Новосибирск: Изд-во СО РАН, 1998. - С. 236-240.

7. Быстров А.В., Городняя JI.B. Обработка исключительных ситуаций в асинхронных программах // Сб.: Теоретические и прикладные вопросы параллельной обработки информации. Новосибирск: ВЦ СО АН СССР, 1984. -С. 91-99.

8. Быстров А.В., Городняя Л.В., Дудоров Н.Н. Основные черты базового языка // Высокопроизводительные вычислительные системы. Т. 11. - Москва: ИПУ АН СССР, 1981. - С. 32-38.

9. Быстров А.В., Городняя JI.B., Котов В.Е. Сетевой подход к преобразованию программ и процессов // Сб.: Оптимизация и преобразование программ. Ч. 1. - Новосибирск: ВЦ СО АН СССР, 1983. - С. 114-222.

10. Быстров А.В., Дудоров Н.Н., Котов В.Е. О базовом языке системы МАРС // Сб.: Языки и системы программирования. Новосибирск: ВЦ СО АН СССР, 1979. - С. 85-106.

11. Бульонков М.А., Быстров А.В., Дудоров Н.Н., Котов В.Е. Базовый язык параллельного программирования для многопроцессорных систем БАРС. (Описание языка) // Алгоритмы и программы. № 4(61). - Москва: ВМТМ Центр, 1984. - С. 23-25.

12. Бульонков М.А., Быстров А.В., Дудоров Н.Н. Сети с синхронизацией -функционирование и корректность // Сб.: Теория программирования и средства описания параллельных дискретных систем. Новосибирск: ВЦ СО АН СССР, 1985. - С. 115-127.

13. Бульонков М.А., Быстров А.В., Дудоров Н.Н., Котов В.Е. Предварительное описание языка Барс // Препринт ВЦ СО АН ССР. № 556. - Новосибирск: ВЦ СО АН ССР, 1985. - 44 с.

14. Бульонков М.А., Быстров А.В., Дудоров Н.Н., Котов В.Е. Базовый язык параллельного программирования Барс // Программирование. 1986. - № 6. -С. 32-40.

15. Вирбицкайте И.Б., Покозий Е.А. Метод параметрической верификации поведения временных сетей Петри // Программирование. 1999. - № 4. - С. 16-29.

16. Вишневский Ю.Л., Котов В.Е., Марчук А.Г. Модульная асинхронная развиваемая система // Кибернетика. 1984, № 3. - С. 22-29.

17. Зайцев С. С. Описание и реализация протоколов сетей ЭВМ. М.: Наука, 1989.

18. Котов В.Е. Модель асинхронных параллельных вычислений и ее языковая и архитектурная реализация // Диссертация на соискание ученой степени доктора физико-математических наук, Новосибирск. - 1980. - 343 с.

19. Котов В.Е. Сети Петри. М.: Наука, 1984. - 160 с.

20. Ломазова И.А. Вложенные сети Петри: моделирование и анализ распределенных систем с объектной структурой // М.: Научный мир, 2004. - 208 с.

21. Питерсон Дж. Теория сетей Петри и моделирование систем. М.: Мир, 1984.

22. Сузи P. Python в подлиннике (+ CD-ROM) / Издательство: BHV. Серия: В подлиннике, 2002. 768 с.

23. Specification, verification and net models of concurrent systems. Novosibirsk: IIS SB RAS, 1994. - R 116-127.

24. Akaza M., Lee D., Kumagai S. Optimal cycle time and facility utilisation of production systems including repetitive process with set-up time modelled by time marked graphs // IEICE Transactions. 1992. - Vol. E75-A(10).

25. Alur R., Courcoubetis C., Dill D. Model-checking for real-time systems // Proc. 5th Symp. Logic in Comput. Sci. 1990. - P. 414-425.

26. Alur R., Courcoubetis C., Halbwachs N., Dill D., Wong-Toi H. Minimization of timed transition systems // Lect. Notes Comput. Sci. 1992. - Vol. 630. - P. 340-354.

27. Alur R., Dill D. The theory of timed automata // Lecture Notes in Computer Science. Vol. 600. - 1991. - P. 45-73.

28. Aura Т., Lilius J. Time processes for time Petri nets // Lecture Notes in Computer Science. 1997. - Vol. 1248. - P. 136-155.

29. Bause F., Kabutz H., Kemper P., Kritzinger P. SDL and Petri net performance analysis of communicating systems // Proc. IFIP 15th Intern. Symp. on Protocol Specifi-cation, Testing and Verification. Warsaw, Poland. - 1995. - P. 259-272.

30. Berthomieu В., Diaz M. Modelling and verification of time dependent systems using time Petri nets // IEEE Transaction on Software Engineering. 1991. -Vol. 17, N 3. - P. 259-273.

31. Best E., Grahlmann B. PEP more than a Petri Net tool // Lecture Notes in Computer Science. - 1996. - Vol. 1055. - P. 397-401.

32. E. Best, R.P. Hopkins. B(PN)2 a basic Petri Net Programming Notation. Lecture Notes in Computer Science. - Vol. 694. - 1993. - P. 379-390.

33. Budkowski S., Dembinski P. An introduction to Estelle: a specification language for distributed systems // Computer Networks. 1988. - Vol. 14. - P. 3-23.

34. Bystrov A.V., Virbitskaite, I.B. RT-Mec: a Tool for Validation and Verification of Petri Nets with Time Parameters // Proc. International Workshop on Discrete Event Systems. Cagliari (Italy), 1998. The IEE Publisher, London. - P. 510-514.

35. Bystrov A.V., Virbitskaite I.B. Implementing Model Checking and Equivalence Checking for Time Petri Nets by the RT-MEC Tool // Lecture Notes in Computer Science. 1999. - Vol. 1662. - P. 194-200.

36. Cherkasova L. A., Kotov V. E. Descriptive and analytical process algebras // Lecture Notes in Computer Science. 1989. - Vol. 424. - P. 77-104.

37. Чурина Т. Г., Аргиров В. С. Моделирование спецификаций языка SDL с помощью ИВТ-сетей. Препринт ИСИ СО РАН. № 124. - Новосибирск, 2005. -62 с.

38. Cohen, R., Segall, A.: An efficient reliable ring protocol // IEEE Transactions on Communications. Vol. 39 (11). - 1991. - P. 1616-1624.

39. Churina T. G., Okunishnikova E. V. Coloured Petri nets approach to the validation of Estelle specifications // Proc. Workshop on Concurrency, Specification and Programming. Warsaw, Poland, 1997. - P. 25-36.

40. Clarke E., McMillan K., Campos S., Hartonas-Gramhausen V. Symbolic Model Checking. Lecture Notes in Computer Science. Vol. 1102. - 1996. - P. 285-268.

41. Cohen R., Segall A. An efficient reliable ring protocol // IEEE Transact. Com-muns. 1991. - Vol. 39, N. 11. - P. 1616-1624.

42. Commoner F., Holt A.W., Even S,, Pnueli A. Marked Directed Graphs // Journal of Computer and System Sciences. 1990. - Vol. 5. - P. 511-527.

43. Desel J., Esparza J. Free-choice Petri nets // Cambridge Tracts in Theoretical Computer Science. 1995. - Vol. 40.

44. Dimitrov V., Petkov A. Verification oriented Estelle specification of communication protocols // Reseach into Networks and Distributed Applications. Amsterdam: North-Holland. - 1988. - P. 953-960.

45. Emersen E., Sistla A. Symmetry and model Checking // Lecture Notes in Computer Science. 1993. - Vol. 697. - P. 463-478.

46. Esparza J. Model checking using net unfoldings // Science of Computer Programming. 1994. - Vol. 23. - P. 151-195.

47. Esparza J., Silva M. A polinomial time algorithm to decide liveness of bounded free choice nets // Theoretical Computer Science. 1992. - Vol. 102(1).

48. Ferenc В., Hogrefe D., Sarma A. SDL with applications from protocol specification.- Englewood Cliffs, NJ: Prentice Hall, 1991.

49. Feldbrugge F. Petri net tools overview 1992 // Lecture Notes in Computer Science.- 1993. Vol. 674. - P. 169-209.

50. Ferenc В., Hogrefe D., Sarma A. SDL with applications from protocol specification // Prentice Hall, 1991.

51. Fernandez J.-C., Mounier L. 'On the fly' verification of behavioral equivalences and preorders // Lecture Notes in Computer Science. 1991. - Vol. 577. - P. 181-191.

52. Fisher J.,Dimitrov E. Verification of SDL'92 specifications using extended Petri nets // Proc. IFIP Fifteenth Intern. Conf. on Protocol Specification, Testing and Verification. Warsaw, 1995. - P. 455-458.

53. Fleischhack, H., Grahlmann, В.: A compositional Petri net semantics for SDL. Lecture Notes in Computer Science. Vol. 1420. - 1998. - P. 144-164.

54. Genrich H. J. Predicate/transition Nets // Lecture Notes in Computer Science. -Vol. 254. 1987. - P. 207-248.

55. Ghezzi C., Mandrioli D., Moraska S., Pezze M. A general way to put time in Petri nets // Proc. 5th Internat. Workshop on Software Specification and Design. -Pittsburg, Pennsylvania. May 1989. - P. 60-67.

56. Godefroid P. Partial-order methods for the verification of concurrent systems. An approach for state-explosion problem // Lecture Notes in Computer Science. -1996. Vol. 1032. - 143 p.

57. Grahlmann, В.: Combining Finite Automata. Parallel Programs and SDL using Petri Nets. Lecture Notes in Computer Science. Vol. 1384. - 1998. - P. 102-117.

58. Hansen P.B. Concurrent Programming Concepts // Computing Surveys. Vol. 5, No 4. - 1979.

59. Henzinger T.A., Manna Z., Pnueli A. Timed transition systems // Lecture Notes in Computer Science. 1991. - Vol. 600. - P. 226-251.

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

61. Hoogers P.W., Kleijn H.C.M., Thiagarajan P.S. An event structure semantics for general Petri nets // Theor. Comput. Sci. 1996. - Vol. 153. - P. 129-170.

62. Husberg, N., Manner, Т.: Emma: Developing an Industrial Reachability Analyser for SDL // Lecture Notes in Computer Science. Vol. 1708. - 1999. - P. 642-661.

63. Imai, K., Ito, Т., Kasahara, H., Morita, N.: ATMR: Asynchronous transfer mode ring protocol // Computer Networks and ISDN Systems. Vol. 26. - 1994. - P. 785-798.

64. Information Processing Systems Open Systems Interaction - ESTELLE: A Formal Description Technique Based on an Extended State Transition Model: Iner-national standard. - 1989. - ISO 9074.

65. Jensen К. Coloured Petri nets: A high level language for system design and analysis // Lecture Notes in Computer Science. Vol. 483. - 1991. - P. 343-416.

66. Jensen K. Coloured Petri nets. Springer-Verlag. - Vol. 1,2,3. - 1996.

67. Jensen K., Kristensen L., Wells L. Coloured Petri Nets and CPN Tools for modelling and validation of concurrent systems // Int. Journal on Software Tools for Technology Transfer. 2007. - Vol. 9, N. 3. - P. 213-254.

68. Kaivola R. Using Compositional preorders in the Verification of Sliding Window Protocol // Lecture Notes in Computer Science. Vol. 1254. - 1997. - P. 48-59.

69. Kindler E., Weber M. The Petri Net Kernel. Documentation of the Application Interface // http://www2.informatik.hu-berlin.de/top/pnk/literatur/PNK-Doc-engl.ps

70. Kozura V.E., Nepomniaschy V.A., Novikov R.M. Verification of distributed systems modeled by high-level Petri nets // Proc. Intern. Conf. on Parallel Computing in Electrical Engineering. Warsaw, Poland, IEEE Сотр. Society (2002) 61-66.

71. Kristensen, L.M., Christensen, S., Jensen, K.: The practitioner's guide to coloured Petri nets // Internat. J. Software Tools for Technology Transfer 2 (2) (1998) 98132

72. Lai R., Jirachiefpattana A. Verifying Estelle protocol specifications using numerical Petri nets // Comput. Syst. Sci & Eng. 1996. - Vol. 11, N. 1. - P. 15-33.

73. Lauer P.E., Campbell R.H. Formal Semantics for a Class of High-Level Primitives Coordinating Concurrent Processes // Acta Informaticaio N 5. - 1975. - P. 297-332.

74. Marsan M. A. Stochastic Petri nets: elementary introduction // Lecture Notes in Computer Science. Vol. 424. - 1989. - P. 1-29.

75. Merlin P., Faber D. J. Recoverability of communication protocols // IEEE Trans, of Communication. 1976. - Vol. COM-24(9).

76. McMilan, K. Using unfolding to avoid the state explosion problem in the verification of asynchronous circuits // Lecture Notes in Computer Science. Vol. 663. - 1992. - P. 164-177.

77. Nepomniaschy V.A., Alekseev G.I., Bystrov A.V., Churina T. G., Mylnikov S. P., Okunishnikova E. V. Petri net modelling of Estelle-specified communication protocols // Lecture Notes in Computer Science. 1995. - Vol. 964. - P. 94-108.

78. Nepomniaschy V.A., Alekseev G.I., Bystrov A.V., Churina T.G., Mylnikov S.P., Okunishnikova E.V. EPV — Petri Net Based Estelle Protocol Verifier // Proc. 1st Intern. Workshop on the Formal Description Technique Estelle. France, Evry, 1998. - P. 101-108.

79. Nielsen, M. Rozenberg, G. Thiagarajan, P.S. Behavioural notions for elementary net systems // Distributed Computing. 1990. - Vol. 4, No. 1. - P. 45-57.

80. Peng, H., Tahar, S., Khendek, F. SPIN vs. VIS: A case study on the formal verification of the ATMR protocol / Proc. 3rd Intern. Conf. on Formal Engineering Methods. IEEE Сотр. Society (2000) 79-87

81. Petri C. Concurrency // Lecture Notes in Computer Science. Vol. 84. - 1980. -P. 261-276.

82. Ramchandani C. Analysis of asynchronous concurrent systems by timed Petri nets // PhD Thesis. MIT TR-120. Cambridge (Mass). 1974.

83. Reisig W. Petri Nets: An Introduction // EATCS Monographs on Theoretical Computer Science. 1985. Vol. 10.

84. Richier J, L., Rodriguez C., Sifakis J., Voiron J. Verification in XESAR of the Sliding Window protocol // Proc. 7th IFIP Int. Symp. on Protocol Specification, Testing and Verification. 1987. - P. 235-248.

85. Rozenberg G., Thiagarajan P, S. Petri Nets: Basic Notions, Structure, Behaviour. Lecture Notes in Computer Science. Vol. 224. - 1986. - P. 585-668.

86. Roux J.-L,, Berthomieu B. Verification of local area network protocol with Tine, a software package for time Petri nets // Proc. 7th Europ. Workshop on Application and Theory of Petri Nets, 1986. P. 183-205.

87. Sifakis J. Performance evaluation of systems using nets // Lecture Notes in Computer Science. Vol. 84. - 1981. - P. 307-320.

88. Schneider S., Davies J., Jackson D.M., Reed G.M., Reed J.M., Roscoe A.W. Timed CSP: theory and practice // Lecture Notes in Computer Science. Vol. 600. -1991. - P. 640-675.

89. Specification and Description Language (SDL). Recommendation, Z.100, CCITT. -1992.

90. Starke P. Some properties of timed nets under the earliest firing time // Lecture Notes in Computer Science. Vol. 424. - 1990. - P. 418-432.

91. Starke P. INA: Integrated net analyzer. Handbuch, 1992.

92. Stenning N. V. A data transfer protocol // Computer Networks. 1976. - Vol. 1, N. 2. - P. 99-110.

93. H. Storrle. Tool Comparison, Manuscript, 1998.

94. Thiagarajan P. S. Elementary net systems. Lecture Notes in Computer Science. -Vol. 254. 1987. - P. 26-59.

95. Trompedeller M. Petri net tools, 1993. Last update: 1995, www.dsi.unimi.it/Users/Tesi/trompede/petri/alfa.html.

96. Valero V., de Frutos D., Cuartero F. Timed processes of timed Petri nets // Lecture Notes in Computer Science. Sci. 1995. - Vol. 935. - P. 490-509.

97. Varpaaniemi K., Halme J., Hiekkanen K., Pyssysalo T. PROD Reference Manual // Technical Report В 13. University of Helsinki. - 1995.

98. I.В. Virbitskaite. Characterizing time net processes categorically // Lecture Notes in Computer Science. Vol. 2127. - 2001. - P. 128-141.

99. Virbitskaite I.В., Pokozy E.A. A partial order method for the verification of time Petri nets // Lecture Notes in Computer Science. 1999. - Vol. 1684. - P. 547-558.

100. Wang F. Timing behavior analysis for real-time systems // Proc. 10th Symp. Logic in Comput. Sci, 1995, P. 112-122.

101. Wikarski D. Petri Net Tools a Comparative Study // Technical Report 97-4. -TU Berlin. - 1997.

102. Yoneda Т., Shibayama A., Schlingloff B.H., Clarke E.M. Efficient verification of parallel real-time systems // Lecture Notes in Computer Science. 1993. - Vol. 697. - P. 321-333.

103. Weber M., Kindler E. The Petri net markup language, Petri Net Technology for Communication Based Systems // Lecture Notes in Computer Science. 2003. -Vol. 2472. - P. 124-144.