Моделирование и анализ сетевых транспортных протоколов с помощью раскрашенных сетей Петри тема диссертации и автореферата по ВАК РФ 01.01.09, кандидат физико-математических наук Чалый, Дмитрий Юрьевич

• Чалый, Дмитрий Юрьевич
• кандидат физико-математических наук
• 2006

Оглавление диссертации кандидат физико-математических наук Чалый, Дмитрий Юрьевич

Введение

Предмет исследования.

Научная новизна работы

Практическая ценность результатов.

Апробация работы.

Содержание работы.

1 Коммуникационные транспортные протоколы

1.1 Современные коммуникационные сети

1.2 Модель взаимодействия открытых систем

1.3 Семейство протоколов TCP/IP.

1.4 Transmission Control Protocol (TCP).

1.5 Протокол ARTCP

1.6 Модели коммуникационных протоколов и сетевого трафика.

2 Моделирование транспортных протоколов с помощью раскрашенных сетей Петри

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

2.2 Моделирование служебных структур протокола.

2.3 Иерархическая структура модели

2.4 Построение модели функциональной части протокола.

2.5 Моделирование обработки пользовательских вызовов.

2.6 Моделирование передачи сегментов в сеть.

2.7 Моделирование обработки пришедших сегментов.

2.8 Модификация модели.

2.9 Общая схема модельных экспериментов.

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

Предмет исследования

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

Транспортные протоколы являются важным элементом коммуникационной архитектуры сети Интернет (согласно исследованиям [72], около 95% всех переданных байтов и 85-95% всех переданных пакетов). Основной задачей протокола транспортного уровня является предоставление сервиса программным процессам для надежного и эффективного обмена информацией через ненадежную среду передачи — коммуникационную сеть. С точки зрения транспортного протокола сеть представляется в виде «черного ящика>, где информация может теряться, переупорядочиваться, искажаться и, возможно, дублироваться. Под эффективностью работы транспортного протокола понимается прежде всего эффективное использование сетевых ресурсов — таких как, например, пропускная способность каналов передачи и буферов маршрутизаторов.

Предметом нашего исследования является транспортный протокол TCP (Transmission Control Protocol), который является основным транспортным протоколом коммуникационной архитектуры сети Интернет. Так как этот протокол постоянно изменяется и дополняется, то можно говорить о семействе протоколов TCP.

Исследование свойств транспортных протоколов, в частности различных версий протокола TCP, является важной и актуальной задачей, которая рассматривалась в ряде работ. Основным объектом исследований являлись алгоритмы управления потоком транспортных протоколов, а основным методом исследований, который использовался в этих работах — имитационное моделирование. Яркими представителями таких работ являются: [66], где рассматривались различные версии алгоритма управления потоком протокола TCP; [67], где представляется новый протокол TCP Westwood, и на ряде примеров обосновывается его эффективность; [1], где представляется новый протокол ARTCP (Adaptive Rate TCP) и на ряде модельных экспериментов обосновывается его преимущество перед стандартным TCP.

Другим популярным методом исследования является построение аналитических моделей. Например, в работе [68] рассматривается модель алгоритма управления потоком и вопросы порождения протоколом TCP самоподобного трафика. Методы имитационного моделирования могут быть весьма экономичными для выявления многих ошибок, однако проверить все возможные взаимодействия и пути выполнения протокола вряд ли представляется возможным.

Одним из подходов к решению задачи корректности транспортных протоколов может быть построение формальных моделей и их последующий анализ с помощью формальных методов (например, методов model checking). Значительный интерес в этом направлении представляют работы И. А. Ломазовой (напр., [10]), посвященные формализму сетей Петри и методам анализа их свойств. Вопросы корректности коммуникационных протоколов рассматривались также, например, в [15, 11]. Основным подходом в работе [15] является построение моделей протоколов с помощью автоматов и их последующая верификация, а в работе [11] приводится метод построения моделей Estelle-спецификаций с помощью раскрашенных сетей Петри. Применение этих подходов затруднено тем, что стандартные документы, задающие спецификацию семейства транспортных протоколов TCP, изложены на неформальном языке. Был представлен ряд работ по построению моделей протокола TCP в терминах раскрашенных сетей Петри (например, [77, 78]). В работе [77] представляются результаты моделирования процесса обмена данными ряда версий протокола TCP, а в работе [78] рассматривается модель процессов установки и завершения соединений. Как видно, эти работы рассматривают некоторые фрагменты оригинального протокола; перед нами же стояла задача промоделировать стандарт протокола целиком. Другой особенностью этих работ является то, что основной акцент они делают именно на построении моделей, а не на разработке методов их исследования. В нашей работе кроме задачи построения моделей, рассматриваются вопросы анализа различных свойств протоколов, таких как производительность и корректность. Очевидно, что корректность, как характеристика, имеет несомненный приоритет над производительностью.

Научная новизна работы

Основные научные результаты работы состоят в следующем:

• В терминах раскрашенных сетей Петри разработана модель последнего варианта официального стандарта спецификации протокола TCP;

• Предложены методы модификации этой модели для представления новых версий протокола TCP;

• На основе построенной модели протокола TCP предложена модель протокола ARTCP (Adaptive Rate TCP);

• Предложены алгоритмы восстановления от множественных потерь сегментов для протокола ARTCP;

• Формально верифицированы процессы открытия и закрытия транспортного соединения;

• На ряде сценариев проведена сравнительная оценка производительности последней версии протокола TCP и предложенных модификаций протокола ARTCP.

Практическая ценность результатов

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

Апробация работы

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

1. Международная конференция «Parallel Computer Technologies» (Нижний Новгород, 2003 год);

2. Всероссийская научная конференция «Методы и средства обработки информации» (Москва, 2003 год);

3. Международной конференции по вычислительной математике (Новосибирск, 2004 год);

4. Междисциплинарной конференции НБАТТ-21 (Петрозаводск, 2004 год);

Результаты также обсуждались на семинаре «Моделирование и анализ информационных систем» ЯрГУ.

Содержание работы

В главе 1 демонстрируется положение транспортного протокола TCP в коммуникационной архитектуре TCP/IP и подробно рассматриваются все его компоненты, принципы работы и алгоритмы. Один из основных результатов работы — модель транспортных протоколов, представляется в главе 2. В начале главы рассматривается формализм раскрашенных сетей Петри и приводятся основные методы анализа моделей, построенных в терминах этого формализма. Глава продолжается описанием модели транспортных протоколов семейства TCP. Там же рассматриваются методы модификации этой модели и возможные варианты использования в модельных экспериментах. Вопросы анализа свойств протоколов рассматриваются в главе 3. В начале главы рассматриваются вопросы верификации транспортных протоколов. Для этого рассматривается набор темпоральных формул, с помощью которых верифицируется процесс обработки пользовательских вызовов транспортным протоколом. Там же приводятся результаты экспериментов по верификации процессов открытия и закрытия транспортного соединения. Далее приводятся результаты анализа поведения протокола ARTCP в условиях множественных потерь сегментов и рассматриваются алгоритмы, которые направлены на увеличение производительности протокола при этих условиях. В конце главы приводятся экспериментальные данные по сравнительному анализу новых версий протоколов TCP и предложенного усовершенствования алгоритма протокола ARTCP. Работа завершается выводами.

Заключение диссертации по теме «Дискретная математика и математическая кибернетика», Чалый, Дмитрий Юрьевич

Заключение

В диссертации рассмотрены вопросы моделирования и анализа коммуникационных транспортных протоколов семейства TCP с помощью раскрашенных сетей Петри. В работе изложена разработанная технология построения модели последней спецификации протокола TCP и методы ее модификации для моделирования будущих версий этого протокола. Для создания и исследования модели использован пакет Design/CPN [98]. Одним из дальнейших направлений работы будет перенос этой модели в более современный пакет CPN Tools [99].

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

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

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

Список литературы диссертационного исследования кандидат физико-математических наук Чалый, Дмитрий Юрьевич, 2006 год

1. Алексеев И.В. Адаптивная схема управления потоком для транспортного протокола в сетях с коммутацией пакетов. // Дисс. на соискание степени к.ф.-м.н. Ярославль. 2000.

2. Алексеев И.В., Соколов В.А., Чалый Д.Ю. Моделирование и анализ транспортных протоколов в информационных сетях. // Ярославский государственный университет. Ярославль, 2004.

3. Соколов В.А., Тимофеев Е.А., Чалый Д.Ю. Моделирование, оптимизация и верификация транспортных протоколов.// Труды первой Всероссийской конференции МСО-2003. Под. ред. J1.H. Королева. Москва, 2003.

4. Чалый Д.Ю. Моделирование протоколов TCP и ARTCP с помощью раскрашенных сетей Петри.// Моделирование и анализ информационных систем. № 2 за 2003 год. Ярославль, 2003. стр. 11-17.

5. Соколов В.А., Чалый Д.Ю. Методы исследования поведения транспортных протоколов в условиях интенсивного сетевого трафика. // Труды Международной конференции по вычислительной математике. Под. ред. Ю.И. Шокина и др. Новосибирск, 2004. стр. 126— 131.

6. Чалый Д.Ю. Моделирование коммуникационных протоколов коммуникационной сети Интернет. // Материалы 3-й междисциплинарной конференции НБАТТ-21. Под. ред. С. Е. Ка-рашурова. Петрозаводск, 2004. стр. 76-77.

7. Соколов В.А., Чалый Д.Ю. Построение и анализ формальных моделей семейства транспортных протоколов TCP. // Труды III Международной конференции «Параллельные вычисления и задачи управления», (принято к публикации)

8. Кларк Э., Грамберг О., Пелед Д. Верификация моделей программ: Model-Checking. МЦ-НМО, Москва, 2002.

9. Ломазова И.А. Сети Петри и анализ поведенческих свойст распредленных систем. Ярославль, 2002. 164 с.

10. Непомнящий В.А., Алексеев А.Г., Быстрое А.В., Куртов С.А., Мыльников С.П., Оку-нишникова Е.В., Чубарев П.А., Чурина Т.Г. Верификация Estelle-спецификаций распределенных систем посредством раскрашенных сетей Петри. Новосибирск, 1998.

11. Chaly D. Ju., Sokolov V. A. An Extensible Coloured Petri Net Model of a Transport Protocol for Packet Switched Networks. // In Proceedings of Parallel Computer Technologies'2003, LNCS Vol. 2551, Springer-Verlag, 2003. p. 66-75.

12. Alekseev I.V., Sokolov V.A. ARTCP: Efficient Algorithm for Transport Protocol for Packet Switched Networks. // In Proceedings of Parallel Computer Technologies'2001. Lecture Notes in Computer Science, Vol. 2127. Springer-Verlag, 2001. стр. 159-174.

13. Alekseev I.V., Sokolov V.A. Modelling and Traffic Analysis of the Adaptive Rate Transport Protocol. // Future Generation Computer Systems. Number 6, Vol. 18. NH Elsevier, 2002. стр. 813-827.

14. Holzmann G. Design and Validation of Computer Protocols. Prentice-Hall, 1991.

15. Transmission Control Protocol. DARPA Internet Program. Protocol Specification. RFC793, September, 1981. Web site: www.rfc-editor.org

16. Clark D. D. Window and Acknowledgement Strategy in TCP. RFC813, July, 1982. Web site: www.rfc-editor.org

17. Postel J. The TCP Maximum Segment Size and Related Topics. RFC879, November, 1983. Web site: www.rfc-editor.org

18. Nagle J. Congestion Control in IP/TCP Internetworks. RFC896, January, 1984. Web site: www.rfc-editor.org

19. Reynolds J., Postel J. Assigned Numbers. RFC1010, May, 1987. Web site: www.rfc-editor.org

20. Jacobson V., Braden R. TCP Extensions for Long-Delay Paths. RFC1072, October, 1988. Web site: www.rfc-editor.org

21. Braden R. (Ed.) Requirements for Internet Hosts — Communication Layers. RFC1122, October, 1989. Web site: www.rfc-editor.org

22. Socolofsky Т., Kale С. A TCP/IP Tutorial. RFC1180, January 1991. Web site: www.rfc-editor.org

23. Jacobson V., Braden R., Zhang L. TCP Extension for High-Speed Paths. RFC1185, October, 1990. Web site: www.rfc-editor.org

24. O'Malley S., Peterson L. TCP Extensions Considered Harmful. RFC1263, October, 1991. Web site: www.rfc-editor.org

25. Jacobson V., Braden R., Borman D. TCP Extensions for High Performance. RFC1323, May, 1992. Web site: www.rfc-editor.org

26. Braden R. TIME-WAIT Assasination Hazards in TCP. RFC1337, May, 1992. Web site: www.rfc-editor.org

27. Connoly Т., Amer P., Conrad P. An Extension to TCP: Partial Order Service. RFC1693, November, 1994. Web site: www.rfc-editor.org

28. Stevens W. TCP Slow Start, Congestion Avoidance, Fast Retransmit and Fast Recovery Algorithms. RFC2001, January, 1997. Web site: www.rfc-editor.org

29. Mathis M., Mahdavi J., Floyd S., Romanow A. TCP Selective Acknowledgement Options. RFC2018, October, 1996. Web site: www.rfc-editor.org

30. Bradner S. Key Words for Use in RFCs to Indicate Requirement Levels. RFC2119, March,1997. Web site: www.rfc-editor.org

31. Touch J. TCP Control Block Interdependence. RFC2140, April, 1997. Web site: www.rfc-editor.org

32. Borman D. TCP and UDP over IPv6 Jumbograms. RFC2147, May, 1997. Web site: www.rfc-editor.org

33. Parker S., Schmechel C. Some Testing Tools for TCP Implementors. RFC2398, August,1998. Web site: www.rfc-editor.org

34. Allman M., Floyd S., Partridge C. Increasing TCP's Initial Window. RFC2414, September, 1998. Web site: www.rfc-editor.org

35. Poduri К., Nichols К. Simulation Studies of Increased Initial TCP Window Size. RFC2415, September, 1998. Web site: www.rfc-editor.org

36. Shepard Т., Partridge C. When TCP Starts Up With Four Packets Into Only Three Buffers. RFC2416, September, 1998. Web site: www.rfc-editor.org

37. Ramakrishnan K., Floyd S. A Proposal to Add Explicit Congestion Notification (ECN) to IP. RFC2481, January, 1999. Web site: www.rfc-editor.org

38. Allman M., Glover D., Sanchez L. Enhancing TCP Over Sattelite Channels Using Standard Mechanisms. RFC2488, January, 1999. Web site: www.rfc-editor.org

39. Paxson V., Allman M., Dawson S., Fenner W., Griner J., Heavens /., Lahey K., Semke J., Volz B. Known TCP Implementation Problems. RFC2525, March, 1999. Web site: www.rfc-editor.org

40. Allman M., Paxson V., Stevens W. TCP Congestion Control. RFC2581, April, 1999. Web site: www.rfc-editor.org

41. Floyd S., Henderson T. The NewReno Modification to TCP's Fast Recovery Algorithm. RFC2582, April, 1999. Web site: www.rfc-editor.org

42. Allman M., Dawkins S., Glover D., Griner J., Tran D., Henderson Т., Heideman J., Touch J., Kruse H., Ostermann S., Scott K., Semke J. Ongoing TCP Research Related to Satellites. RFC2760, February, 2000. Web site: www.rfc-editor.org

43. Handley M., Padhye J., Floyd S. TCP Congestion Window Validation. RFC2861, June, 2000. Web site: www.rfc-editor.org

44. Xiao X., Hannan A., Paxson V., Crabbe E. TCP Processing of the IPv4 Precedence Field. RFC2873, June, 2000. Web site: www.rfc-editor.org

45. Floyd S., Mahdavi J., Mathis M., Podolsky M. An Extension to the Selective Acknowledgement (SACK) Option for TCP. RFC2883, July, 2000. Web site: www.rfc-editor.org

46. Hadi Salim J., Ahmed U. Performance Evaluation of Explicit Congestion Notification (ECN) in IP Networks. RFC2884, July, 2000. Web site: www.rfc-editor.org

47. Lahey K. TCP Problems with Path MTU Discovery. RFC2923, September, 2000. Web site: www.rfc-editor.org

48. Paxson V., Allman M. Computing TCP's Retransmission Timer. RFC2988, November, 2000. Web site: www.rfc-editor.org

49. Allman M., Balakrishnan H., Floyd S. Enhancing TCP's Loss Recovery Using Limited Transmit. RFC3042, January, 2001. Web site: www.rfc-editor.org

50. Ramakrishnan K., Floyd S., Black D. The Addition of Explicit Congestion Notification (ECN) to IP. RFC3168, Septempber, 2001. Web site: www.rfc-editor.org

51. Floyd S. Inappropriate TCP Resets Considered Harmful. RFC3360, August, 2002. Web site: www.rfc-editor.org

52. Allman M., Floyd S., Partridge C. Increasing TCP's Initial Window. RFC3390, October, 2002. Web site: www.rfc-editor.org

53. Handley M., Floyd S., Padhye /., Widmer J. TCP Friendly Rate Control (TFRC): Protocol Specification. RFC3448, January, 2003. Web site: www.rfc-editor.org

54. Balakrishnan H., Padmanabhan V. N., Fairhurst G., Sooriyabandara M. TCP Performance Implications of Network Path Assymetry. RFC3449, December, 2002. Web site: www.rfc-editor.org

55. Allman M. TCP Congestion Control with Appropriate Byte Counting (ABC). RFC3465, February, 2003. Web site: www.rfc-editor.org

56. Ludwig R., Meyer M. The Eifel Detection Algorithm for TCP. RFC3522, April, 2003. Web site: www.rfc-editor.org

57. Spring N., Wetheral D., Ely D. Robust Explicit Congestion Notification (ECN) Signaling with Nonces. RFC3540, June, 2003. Web site: www.rfc-editor.org

58. Floyd S. Highspeed TCP for Large Congestion Windows. RFC3649, December, 2003. Web site: www.rfc-editor.org

59. Floyd S. Limited Slow-Start for TCP with Large Congestion Windows. RFC3742, March, 2004. Web site: www.rfc-editor.org

60. Floyd S., Henderson Т., Gurtov A. The NewReno Modification to TCP's Fast Recovery Algorithm. RFC3782, April, 2004. Web site: www.rfc-editor.org

61. Ludwig R., Gurtov A. The Eifel Response Algorithm for TCP. RFC4015, February, 2005. Web site: www.rfc-editor.org

62. Raghunarayan R (Ed.). Management Information Base for the Transmission Control Protocol (TCP). RFC4022, March, 2005. Web site: www.rfc-editor.org

63. Karn P., Partridge C. Improving Round-Trip Time Estimates in Reliable Transport Protocols. // In Proceedings of ACM SIGCOMM'87. 1987.

64. Fall K., Floyd S. Simulation-based Comparisons of Tahoe, Reno, and SACK TCP. // Computer Communications Review, 26(3). 1996. стр. 5-21.

65. Shao S., Sanadidi M. Y., Gerla M. A Simulation Study of the Interoperability of TCPW with RED and ECN. // In Proceedings of SPECTS 2003, Montreal, Canada, July 2003.

66. Figueiredo D.R., Liu В., Feldmann A., Misra V., Towsley D., Willinger W. On TCP and self-similar traffic. // Performance Evaluation, №61. Elsevier, 2005. p. 129-141.

67. Paxson V. Measurements and Analysis of End-to-End Internet Dynamics. // PhD thesis, University of California, Berkeley. 1997.

68. Leland W., Willinger W., Taqqu M., Wilson D. On the Self-Similar Nature of Ethernet Traffic (Extended Version). // IEEE/ACM Transactions on Networking. 2(1). 1994. p. 1-15.

69. Taqqu M., Willinger W., Sherman R. Proof of Fundamental Result in Self-Similar Traffic Modelling. // Computer Communications Review. № 27. 1997. p. 5-23.

70. Thompson K., Miller G.3., Wilder R. Wide-Area Internet Traffic Patterns and Characteristics. // In IEEE Networks, November, 1997.

71. Youngmi loo, Ribeiro V., Feldmann A., Gilbert A., Willinger W. TCP/IP traffic dynamics and network performance: A lesson in workload modeling, flow control, and trace-driven simulations. // ACM Computer Communication Review, April, 2001.

72. Network Simulator Ns-2. Web site: http://www.isi.edu/nsnam/ns/

73. Comer D. Internetworking with TCP/IP, Volume 2: Design Implementation and Internals. // Prentice Hall, NJ, 1994.

74. Han В., Billington J. Experience with Modelling TCP's Connection Management Procedures. // Proceedings of 5th Workshop and Tutorial on Practical Use of Coloured Petri Nets and the CPN Tools. Aarhus, Denmark. 2004. p. 57.-77.

75. Kumar A. Comparative Performance Analysis of Versions of TCP in a Local Network with a Lossy Link. // IEEE/ACM Transactions on Networking, №6. 1998. p. 485-498.

76. Ost A., Haverkroft B.R. Analysis of Windowing Mechanisms with Infinite-State Stochastic Petri Nets. // Performance Evaluation Review, №26(2). 1998. p. 38-46.

77. Gordon S. Verification of the WAP Transaction Layer Using Coloured Petri Nets. // PhD Thesis, University of South Australia, 2001.

78. Clarke E. M., Emerson E. A., Sistla A. P. Automatic Verification of Finite State Concurrent System Using Temporal Logic. // ACM Transactions on Programming Languages and Systems, №8(2), 1986. стр. 244-263.

79. Jensen K. Coloured Petri Nets. Basic Concepts, Analysis Methods and Practical Use. Vol. 1, Basic Concepts. // Monographs in Theoretical Computer Science. Springer-Verlag, 1997. 2nd corrected printing.

80. Jensen K. Coloured Petri Nets. Basic Concepts, Analysis Methods and Practical Use. Vol. 2, Analysis Methods. // Monographs in Theoretical Computer Science. Springer-Verlag, 1997. 2nd corrected printing.

81. Jensen K. Coloured Petri Nets. Basic Concepts, Analysis Methods and Practical Use. Vol. 2, Practical Use. // Monographs in Theoretical Computer Science. Springer-Verlag, 1997.

82. Jensen K. Coloured Petri Nets with Time Stamps. // Computer Science Department, Aarhus University, Denmark, 1991.

83. Jensen K. An Introduction to the Theoretical Aspects of Coloured Petri Nets. // In (eds.): de Bakker J. W., de Roever W.-P., Rozenberg G. A Decade of Concurrency, LNCS Vol. 803, Springer-Verlag, 1994. стр. 230-272.

84. Shin /., Levis A.H. Performance Prediction Model Generator Powered by Occurrence Graph Analyzer of Design/CPN. // Proceedings of 2nd Workshop on Practical Use of Coloured Petri Nets and Design/CPN. Aarhus, Denmark. 1999. p. 191-210.

85. Christensen S., Haagh Т. B. Overview of CPN ML Syntax. // University of Aarhus, 1996.

86. Design/CPN Reference Manual for X-Windows, Version 2.0. // Meta Software Corporation, 1993.

87. Jensen K., Christensen S., Kristensen L. M. Design/CPN Occurence Graph Tool Manual, Version 3.0.// Department of Computer Science, Aarhus University, Aarhus, Denmark, 1996.

88. J0rgensen J. В., Kristensen L. M. Design/CPN OE/OS Graph Manual, Version 1.0. 11 Department of Computer Science, Aarhus Unversity, Denmark, 1996.

89. Lindstr0m В., Wells L. Design/CPN Performance Tool Manual, Version 1.0. // Department of Computer Science, Aaurhus University, Aarhus, Denmark, 1999.

90. Christensen S., Mortensen К. H. Design/CPN ASK-CTL Manual, Version 0.9. // Department of Computer Science, Aaurhus University, Aarhus, Denmark, 1996.

91. Christensen S., Kristensen L. M., Mailund T. Design/CPN Sweep Line Method Library. // Department of Computer Science, Aarhus University, Denmark, 2001.

92. University of Aarhus. Design/CPN Online. Web site: http://www.daimi.au.dk/designCPN/

93. University of Aarhus. CPNTools Online. Web site: http://www.daimi.au.dk/"cpntools/

94. Ullman J. D. Elements of ML Programming. // Prentice Hall, Englewood Cliffs, NJ, 1994.

95. Milner R., Tofte M., Harper R., MacQueen D. The Definition of Standard ML (Revised). // MIT Press, 1997.

96. Standard ML of New Jersey. Web site: http://cm.bell-labs.com/cm/cs/what/smlnj.