Исследование и разработка методов верификации протоколов распределенных систем на основе бисимуляционной эквивалентности сетей Петри тема диссертации и автореферата по ВАК РФ 05.13.11, кандидат технических наук Поступальский, Павел Алексеевич

• Поступальский, Павел Алексеевич
• кандидат технических наук
• 1997

Оглавление диссертации кандидат технических наук Поступальский, Павел Алексеевич

Введение

1 Задача верификации протоколов распределенных систем

1.1 Распределенные системы.

1.1.1 Эталонная модель взаимодействия открытых систем.

1.2 Верификация протоколов распределенных систем

1.2.1 Методы анализа логической корректности

1.2.2 Задача верификации в терминах эталонной модели ВОС.

1.2.3 Требование к формальной модели для верификации протоколов.

1.3 Обзор формальных моделей.

1.4 Методология полной верификации протоколов.

1.4.1 Спецификация протокола объектами сети Петри.

1.4.2 Построение модели верификации

1.4.3 Сравнение спецификации сервиса и его логической реализации.

1.5 Автоматизированная система верификации.

1.5.1 Обзор автоматизированных систем, использующих бисимуляционную эквивалентность

1.5.2 Требования к автоматизированной системе верификации

2 Методы верификации протоколов

2.1 Сети Петри.

2.2 Верификация протоколов.

2.3 Проверка помеченных сетей Петри на бисимуляцион-ную эквивалентность.

2.4 Построение сокращенного графа достижимости

2.5 Распределенная бисимуляционная эквивалентность

3 Автоматизированная система разработки спецификаций

3.1 Подсистема базового редактора

3.1.1 Термины графичесого интерфейса с пользователем

3.1.2 Инструментальная Панель Базового редактора

3.1.3 Меню Базового редактора

3.2 Подсистема архитектурного редактора.

3.2.1 Инструментальная Панель Архитектурного редактора

3.3 Подсистема верификации и анализа логической корректности

3.3.1 Реализация алгоритма построения дерева достижимости.

3.3.2 Реализация алгоритма проверки на бисимуляци-онную эквивалентность.

4 Практическое применение методов и средств

4.1 Дуплексный Б-протокол.

4.2 Протокол альтернативного бита.

4.3 Верификация протоколов альтернативного бита и S-протокола.

Введение диссертации (часть автореферата) на тему «Исследование и разработка методов верификации протоколов распределенных систем на основе бисимуляционной эквивалентности сетей Петри»

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

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

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

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

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

Связь с планами отраслей наук и народного хозяйства. Представленные в диссертации исследования проводились в рамках следующих программ: 1. В рамках научно-исследовательских тем Института автоматики и процессов управления ДВО РАН:

• "Исследование и разработка методов анализа и синтеза протоколов сетей ЭВМ", N гос. регистрации 01.9.10016815.

• "Формальные методы и средства разработки программного обеспечения распределенных вычислительных систем", N гос. регистрации 01.9.50 006912.

2. В рамках проектов Российского фонда фундаментальных исследований:

• "Основы композициональной теории сетей Петри", грант 93013-17372.

• "Композициональные методы разработки сетевых протоколов", грант 96-01-00177.

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

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

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

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

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

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

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

1. Разработаны методологические основы полной верификации протоколов на базе формализма композициональных сетей Петри;

2. Разработаны методы обобщения алгоритмов бисимуляционной эквивалентности систем переходов для верификации объектов сети Петри;

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

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

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

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

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

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

• международные конференции: международная конференция "Приложения и теория сетей Петри" (Шеффилд, Великобритания, 1992); международный симпозиум "Новейшие технологии и автоматизация производства (ЕТЕА'94)" (Токио, Япония, 1994); международный симпозиум "Спецификация, тестирование и верификации протоколов (Р8ТУ-95)" (Варшава, Польша, 1995); международный семинар "Моделирование, анализ и симуляция компьютерных и телекоммуникационных систем" (Дарем, США,

1995); международная конференция "Математическое моделирование и криптография (РММС-95)" (Владивосток, Россия, 1995); международная конференция " Новейшие технологии и приложения в коммуникациях ^аСОМ-96)" (Портланд, Орегон, США,

1996); международная конференция "Анализ и синтез информационных систем" (Орландо, США, 1996); международная конференция "Системы мультимедиа и параллельность" (Тулуза,

Франция, 1997);

• всесоюзные конференции, школы и семинары: V совещание по распределенным вычислительным системам и сетям (8Б8-92) (Калининград, 1992); 17 Всесоюзная школа-семинар по вычислительным сетям (Алма-Ата, 1992); Дальневосточная математическая школа (Находка, 1994).

• семинары Института автоматики и процессов управления ДВО РАН в 1991-1997 гг.

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

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

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

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

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

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

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

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

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

Заключение и основные выводы

Список литературы диссертационного исследования кандидат технических наук Поступальский, Павел Алексеевич, 1997 год

1. Агеев М.Д., Касаткин Б.А., Киселев J1.B., Молоков Ю.Г., Никифоров В.В., Рылов Н.И. Автоматические подводные аппараты. - Ленинград: Судостроение, 1981 (Техника освоения океана), с.224

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

3. Анисимов H.A. Формализация сервиса вычислительной сети на основе алгебраического подхода // Одиннадцатый Всесоюзный семинар по вычислительным сетям (Рига, октябрь 1986), М.;Рига: ВИНИТИ, 1986, ч.2, с.14-19.

4. Анисимов H.A. Алгебра структур протоколов на основе теории сетей Петри // Автоматика и вычислительная техника, 1987, N 1, с.9-15.

5. Анисимов H.A., Бузин A.M., Голенков Е.А. Технологические принципы разработки программного обеспечения информационно вычислительных сетей // Управляющие системы и машины, 1988, N 4, с.86-91.

6. Анисимов H.A. Рекурсивное определение иерархии протоколов на основе сетей Петри // Четырнадцатая Всесоюзная школа семинар по вычислительным сетям (Минск, 1989), - М.; Минск: ВИНИТИ, 1989, ч.2, с.101-106.

7. Анисимов H.A. Определение операции разрушения языка спецификации LOTOS на основе сетей Петри // Проектирование вычислительных средств / Труды Всесоюзн. научно-техн. конф. (6-8 июня 1989). Каунас.

8. Анисимов H.A., Голенков Е.А., Кишинский К.П., Коваленко A.A. Графический LOTOS на базе сетей Петри и средства его обработки // Технология программирования 90-х / Тез. докл. межд. конф. (Киев, 14-17 мая, 1991), -Киев: ИК АН УССР, 1991, с.97-98.

9. Анисимов H.A., Коваленко A.A., Поступальский П.А., Симанчук A.C. Графический редактор протоколов сетей ЭВМ на базе сетей Петри // Семнадцатая Международная школа семинар по вычислительным сетям (Алма-Ата, 1992), - М.; Алма-Ата: ВИНИТИ, 1992, ч.2, с.3-8.

10. Аничкин С.А., Белов С.А., Бернштейн A.B. и др. Протоколы информационно вычислительных сетей : Справочник. - М.: Радио и связь, 1990, 504 с.

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

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

13. Блэк Ю. Сети ЭВМ: Протоколы, стандарты, интерфейсы / Пер. с англ. М.: Мир, 1990, 506 с.

14. Бутрименко A.B., Разработка и эксплуатация сетей ЭВМ, -М: Финансы и статистика, 1981.

15. Вельбицкий И.В., Ходаковский В.Н., Шолмов Л.И. Технологический комплекс производства программ на машинах ЕС ЭВМ и БЭСМ-6. -М.: Статистика, 1980. 263 с.

16. Ефимушкин В.А. Процедура синхронизации мультимедиа потоков. // Восемнадцатая Международная конференция и школа по информационно-вычислительным сетям (Украина, Гурзуф, 1995), с. 162-165.

17. Ершов А.П. Комплексное развитие системного программного обеспечения: постановка проблемы. -Новосибирск, 1983. -20 с. (Препр./АН СССР, ВЦ СО, N 469).

18. Зайцев С.С., Кравцунов М.И., Ротанов C.B. Сервис открытых информационно вычислительных сетей: Справочник. - М.: Радио и связь, 1990. - 240 с.

19. Кириллов В.Ю. Об автоматной интерпретации сетей Петри // Изв. АН СССР. Техн. Кибернет. 1987, N 5, 151-163.

20. Котов В.Е. Алгебра регулярных сетей Петри. // Кибернетика, 1980, N 5, с.10-18.

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

22. Непомнящий В.А., Рякин О.М. Прикладные методы верификации программ, -М.: Радио и связь, 1988.

23. Советов Б.Я., Яковлев С.А. Построение сетей интегрального обслуживания.- JI: Машиностроение, 1990.

24. Таль А.А., Юдицкий С.А. Иерархия и параллелизм в сетях Петри I, II //Автоматики и телемеханика, 1982, N 7, с.113-122, N 9, с.83-88.

25. Хоар Ч. Взаимодействующие последовательные процессы, М.: Мир, 1989. -264 с.

26. Якубайтис Э.А. Архитектура вычислительных сетей. М.: Статистика, 1980.- 279 с.

27. Якубайтис Э.А. Информационно-вычислительные сети. М.: Финансы и статистика, 1984. - 232 с.

28. N.A.Anisimov. A Notion of Petri Net Entity for Communication Protocol Design (Institute for Automation and Control Processes, 1989).

29. N. A. Anisimov. A Petri Net Entity as a Formal Model for LOTOS, a Specification Language for Distributed and Concurrent Systems, in: Parallel Computing Technologies, ed. N. N. Mirenkov (World Scientific, 1991), 440-450.

30. N. A. Anisimov. An Algebra of Regular Macronets for Formal Specification of Communication Protocols. Computers and Artificial Intelligence, 10 (1991), 541560.

31. N. A. Anisimov, A. A. Kovalenko, P. A. Postupalski,A. S. Simancuk, A Graphical Petri Net Based Editor for Visualization of Distributed and Parallel Systems. Lecture Notes in Computer Science, 631 (Springer-Verlag, 1992) 847-848.

32. N. A. Anisimov. A Disabling of Event Structures, in: PARLE'93, Parallel Architectures and Language Europe, ed. A. Bodem M. Reeve, G. Wolf, Lecture Notes in Computer Science, 694 .(Springer-Verlag, 1993) 724-728.

33. N. A. Anisimov, A. A. Kovalenko, P. A. Postupalski, Two-Levels Formal Model for Protocol Specification Based on Petri Nets, in Network Information Processing

34. Systems. Proc. of the IFIP TC6 Int. Symp. ed.K. Boyanov, (Bulgarian Academy of Sciences, 1993) 143-154.

35. N.A.Anisimov, A.A.Kovalenko, P.A.Postupalski,. Compositional Petri Net Environment, in: Proc. of the 1994 IEEE Symposium on Emerging Technologies & Factory Automation: ETFA '94, November 6-10, 1994, Tokyo, Japan, 420-427.

36. Anisimov N.A., Kovalenko A.A., Towards Petri Net Calculi based on Synchronization via Places, Proc. of the 1995 IEEE Symposium on Parallel Algorithms/Architecture Synthesis, March 15-17, 1995, Aizu, Japan, 264-270.

37. Anisimov N., Koutny M., On Compositionality and Petri Nets in Protocol Engineering, Protocol Specification, Testing and Verification XV, P.Dembiniski, M.Sredniawa eds. (Chapman & Hall, 1995), pp.71-86

38. N.Anisimov, K.Kishinski, A.Miloslavski. Petri Net Based Model for Design of CTI-applications, to appear in Proc. of the conference "Computational Engineering on Systems Application: CESA'96", July 9-12, 1996, Lille, France.

39. N.Anisimov, M.Koutny, Compositional Petri Nets in Protocol Engineering. Technical Report, 1997.

40. J.C.M. Baeten, W.P. Weijland, Process Algebra. Cambridge Tracts in Theoretical Computer Science, 18, Cambridge University Press, 1990.

41. K. A. Bartlett, R. A. Scantlebury, and P. T. Wilkinson, A Note on Reliable Full-Duplex Transmission over Half-Duplex Lines, Communication of the ACM, 12 (1969) 260-265.

42. Bjorn Victor, Faron Moller, The Mobility Workbench. A Tool for the 7r-Calculus.

43. R. De Nicola, Extensional Equivalences for Transition Systems, Acta Informatica, vol. 24, 1987, pp.211-237.

44. J.-C.Fernandez, An Implementation of an Efficient Algorithm for Bisimulation Equivalence, Science of Computer Programming, vol.13, 1989/90.

45. J.CI. Fernandez, Aldebaran, A tool for verification of communicating processes. User Nanual.

46. R.J.Van Glabbeek, The Linear Time — Branching Time Spectrum, in: CON-CUR'90, Theories of Concurrency: Unification and Extension, ed. J.C.M.Baeten, J.W.Klop, Lecture Notes in Computer Science, vol.458, Springer-Verlag, 1990.

47. M.Hillerström, Verification of CCS-processes, M. Sc. Thesisis, Computer Science Department, Aalborg University, Denmark, 1987.

48. C.A.R.Hoare, Communicating Sequental Processes. Printice-Hall, 1985.

49. P. Jancar, Decidability Questions for Bisimulation of Petri Nets and Some Related Problems, Report ECS-LFCS-93-261, University of Edinburg, 1993, 12 p.

50. R. Janicki, M. Koutny, On Some Implementation of Optimal Simulations. Proceedings of Computer-Aided Verification'90, Lecture Notes in Computer Sciences, 254, Springer Verlag, 1991, pp.166-175.

51. K. Jensen, G. Rozenberg (Eds.) High-level Petri Nets. Theory and Application, Springer-Verlag, 1991, 724 p.

52. P.C.Kanellakis, S.C.Smolka, CCS Expressions, Finite State Processes and Three Problems of Equivalence. In: Proc. of the Second ACM Symposium on Principles of Distributed Computing, 1983.

53. H.P.Korver, The Current State og Bisimulation Tools, Report P9101, Programming Research Group, University of Amsterdam, 1991, 28 p.

54. K.G. Larsen, Context-Dependent Bisimulation Between Processes, Ph.D Thesisis, University of Edinburg, 1986.

55. R.Paige, R.E.Tarjan, Three Partitioning Refinement Algorithms. SIAM Journal of Computing, Vol.16, No.6, 1987, pp.973-989.

56. J.L.Peterson. Petri Net Theory and the Modelling of Systems, Prentice-Hall Inc., 1981

57. L. Pomello, G. Rosenberg, and C. Simone, A Survey of Equivalence Notions for Net Based Systems, in: Advances in Petri Nets 1992, ed.G. Rozenberg, Lecture Notes in Computer Science, 609, Springer-Verlag, 1992.

58. W.Reisig. Petri Nets: An Introduction. EATCS Monograph on Theoretical Computer Science (Springer-Verlag, 1985).

59. C.Sunshine. A Formal Techniques for Protocol Specification and Verification. Computer, Vol.12, 1979, pp.20-27.

60. E. Best, F. De Cindio, and R. Hopkins, DEMON — an ESPRIT Basic Research Action (No.3148), EATCS Bulletin No.41 (1990) 87-103.

61. E.Best, R.Devillers, A.Kiehn, and L.Pomello, Concurrent Bisimulations in Petri Nets. Acta Informatica, vol. 28, 1991, pp.231-261.

62. E. Best, R. Devillers, J. G. Hall, The Box Calculus: a New Causal Algebra with Multi-label Communication, in: Advances in Petri Nets 1992, ed.G. Rozenberg, Lecture Notes in Computer Science, 609 (Springer-Verlag, 1992) 21-69.

63. E. Best (ed), First-Year Results of hte Esprit Basic Research WG 6067 CALIBAN (Causal Calculi Based on Nets) Hildesheimer Informatic Berichte 11/93 (Universität Hildesheim, 1993)

64. E. Best, J. Esparza, Model Checking of Persistent Petri Nets, 35-52

65. W.Brauer, W.Reisig, G.Rozenberg (eds). Petri Nets. Part I and II. Proc. of an Advanced Course, Bad Honnef. Lecture Notes in Computer Science, vol.254/255, Springer-Verlag, 1987

66. G. V. Bochmann, C. A. Sunshine. Formal Methods in Communication Protocol Design. IEEE Trans. Commun. COM-28 (1980) 624-631.

67. G. Bochmann, Usage of Protocol Development Tools: The Results of a Survey, in: Protocol Specification, Testing, and Verification, VII: Proc. of the IFIP WG 6.1 7th International Symposium, eds. H. Rudin, C. H. West (North-Holland, 1987) 139-161.

68. T. Bolognesi, E. Brinksma. Introduction to the ISO Specification Language LOTOS. Computer Network and ISDN Systems 14 (1987), 25-29.

69. G.Booch, Object oriented design with applications, Benjamin/Cummings Publis-ing Co., USA, 1991.

70. S. Budkowski, P. Dembinski, An Introduction to Estelle: A Specification Language for Distributed Systems. Computer Network and ISDN Systems 14 (1987) 3-23.

71. R. H. Cambell, A. N. Habermann, The Specification of Processes Synchronization by Path Expressions. Lecture Notes in Computer Science 16 (Springer-Verlag, 1974) 89-102.

72. R. Cleaveland, J. N. Gada, P. M. Lewis, S. A. Smolka, O. Sokolowsky, S. Zhang, The Concurrensy Factory Practical Tools for Specification, Simulation, Verification, and Imnplementation of Concurrent Systems.

73. R. Cleaveland, J. Parrow, S. Steffen, A Semantic-Based Tools for the Verivica-tion of Finite-State Systems, in Proc. IFIP Symposium on protocol Specofication, Texting and Verification 287-302 Amsterdam, 1990.

74. R. Cleaveland, J. Parrow, S. Steifen, The Concurrency Workbench, in Proc. Workshop on Automatic Verification Methods for Finite-State Systems LNCS 407 (1989) 24-37.

75. R. Cleaveland, J. Parrow, S. Steffen, The Concurrency Workbench:Operating Instructions. Technical Note 10. University of Edinburg 1988.

76. R. Cleaveland, On Automatically Distinguished Inequivalent Processes, in Proc. Workshop on Computer-Aided Verification, DIMACS technical report 90-31, 1990.

77. D. W. Davies, D. L. A. Barber, Communication Networks for Computers (Joihn Wiley k Sons, 1973).

78. D. W. Davies, D. L. A. Barber, W. L. Price, C. H. Solomondies, Computer Networks and their Protocols (Joihn Wiley & Sons, 1979).

79. J. D. Day, H. Zimmermann. The OSI Reference Model. Proceedings IEEE 71 (1983) 1334-1340.

80. P. Degano, R. De Nicola, and U. Montanari, A Distibutional Semantics for CCS based on Condition/Event Systems. Acta Informatica, 26 (1988) 59-91.

81. M.Diaz. Modeling and Analysis of Communication and Cooperation Protocols Using Petri Net Based Models, Computer Networks 6 (1982) 419-441.

82. H.Ehrig, B.Mahr, Fundamentals of Algebraic Specifications I (Springer-Verlag, 1985).

83. Espiau B., Simon D., Kapellos K. Formal Verification of Missions and Tasks. Workshop: Undersea Robotics and Intelligent Control, lisboa, Portugal March 2-3, 1995.

84. F.Feldbrugge, Petri Net Tool Overview 1992, Petri Net Newsletter 41 (Gesellschaft für Informatik, 1992) 2-42.

85. J. Godskeen, K.Larsen, M.Zeeberg, TAV User Manual, Technocal Report R89-19, 1989.

86. U.Goltz and A.Mycroft, On the Relationship of CCS and Petri Nets. Lecture Notes in Computer Science, 172 (Springer-Verlag, 1984) 196-208.

87. U.Goltz, A Class of CCS Programs Representable by Finite Petri Nets. Lecture Notes in Computer Science, 324 (Springer-Verlag, 1988) 339-350.

88. J. F. Groote, F. W. Vaandrager. An efficient algorithm for branching bissimulation and stuttering equivalence. In Proceedings 17th ICALP, Warwick, LNCS, vol. 443, 626-638, 1990.

89. M. Hinchey, Formal methods for system specification an ounce of prevention is worth a pound of cure, IEEE Potentials, pp.50-52, October, 1993.

90. C.A.R.Hoare, Formal Methods in Computer System Design, CERN School of Computing, Oxford, UK, 15-26, CERN Sei. Rept. 6 (1989) 1-7.

91. G.Holzmann, Design and Validation of Computer Protocols. (Printice-Hall, 1991) p.500

92. ISO, IS 7498. Information Processing Systems Open Systems Interconnection -Basic Reference model, 1983.

93. ISO, IS 9074, Information Processing Systems Open Systems Interconnection -"Estelle (Formal Description Technique based on an Extended State Transition Model)", (1988) p.180.

94. K.Jensen et al, Design/CPN: A Tool Supporting Coloured Petri Nets, User Manual, Meta Software Corporation, 150 Cambridge Park Drive, Cambridge MA 02140 (1988).

95. K. G. Larsen, Efficient Local Correctness Checking. In Proceedings of Fourth International Workshop on Computer Aided Verification Methods, Montreal, June 1992. Lecture Notes In Computer Science, Springer Verlag, 663, 1992.

96. P.E.Lauer, R.H.Campbel. Formal Semantics of a Class of High-Level Primitives for Coordinating Concurrent Processes. Acta Informatica 5 (1975) 297-332.

97. R.Loogen and U.Goltz, A Non-Interleaving Semantic Model for Nondeterministic Concurrent Processes. Aachener Informatik-Berichte 87—15, (RWTH Aachen, 1987).

98. E.Madeleine, R. De Simone, D. Verigamini, Ecrins A Proof Laboratory for Process Calculii, User Manual INRIA 1989.

99. R.Milner, A Calculus for Communication Systems. Lecture Notes in Computer Science, 92 (Springer-Verlag, 1980) p.170.

100. R.Milner. Communication and Concurrency (Prentice-Hall International, 1989).

101. S.C.Nash. Formal and Protocol Language (FAPL), Computer Networks and ISDN Systems 14 (1987) 61-77.

102. E.-R.Olderog, Operational Petri Nets Semantics for CCSP. in: Advances in Petri Nets 1987, ed. G. Rozenberg, Lecture Notes in Computer Science, 266 (SpringerVerlag, 1987) 196-233.

103. B.Pehrson. Protocol Verification for OSI. Computer Networks and ISDN Systems 18 (1989/90) 185-201.

104. K.A.Petri, Kommunication mit Automaten, Schriften des Rheinish, Westfälischen Institutes fur Instrumentelle Mathematik and der Universität Bonn (1962).

105. Prabhakaran B., Raghavan S., Synchronization Models Multimedia Presentations With User Interaction, ACM Multimedia '93 , pp 157-166, California, USA, June 1993.

106. C.V.Ramamoorthy, Y.Yaw, and W.T.Tsai, A Petri Net Reduction Algorithm for Protocol Analysis, in: Proc. ACM SIGCOM'86 Symp., Computer Communication Review 16 (1986) 157-166.

107. V.Roy, R.De Simone, An Autograph primer. INRIA Technical Report 112 1989.

108. V.Roy, R.De Simone, Auto Autograph. Workshop on Computer-Aided Verification Princeton 1990.

109. H.Rudin. Network Protocols and Tools to Help Produce Them, in: Ann. Rev. Comput. Sei. 2 (1987) 291-316.

110. R.Saraco, P.A.J.Tilanus, CCITT SDL: Overview of the Language and its Applications, Computer Networks and ISDN Systems 13 (1987) 65-74.

111. Senac P., Diaz M., and Saqui-Sannes P., Toward a formal specification of multimedia synchronization scenarios, Annals of Telecommunications, pp 297-314, Volume 49, No 5-6, May 1994.

112. D.Taubner, Finite Representation of CCS and TCSP Programs by Automata and Petri Nets, Lecture Notes in Computer Science, 369 (Springer-Verlag, 1989) p.168.

113. S.T.Vuong, D.D.Cowan. A Decomposition Method for the Validation of Structured Protocols, in: Proc. Conf. INFOCOM'82 (1982) 209-220.

114. S. Vuong, K. Cooper, and M. Ito, "Formal Methods for Modeling Multimedia Synchronization Requirements" Proc. of ICNP'95 Int. Conf on Network Protocols, Tokyo Nov 7-10, 1995.

115. P.Ward and S.Mellor, Structured development for real-time systems, Yourdon Press, USA, 1985.

116. Construction and Analysis of Condensed State Spaces, in: Advanced Theory Tutorial Notes. 15th Int. Conf. on Application and Theory of Petri Nets, ed. K.Ensen (Zaragoza, Spain, June 1994)

117. H.Zimmermann. OSI Reference Model the ISO Model of Architecture for Open Systems Interconnection. IEEE Trans. Commun. COM-28 (1980) 425-432.

118. H.Zimmermann. On Protocol Engineering, in: Proc.IFIP Information Processing 83 (1983) 283-292.