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

Гб Ой

К Я1Ш 19с5 РОССИЙСКАЯ АКАДЕМИЯ НАУК и 11 "". ДАЛЬНЕВОСТОЧНОЕ ОТДЕЛЕНИЕ

ИНСТИТУТ АВТОМАТИКИ И ПРОЦЕССОВ УПРАВЛЕНИЯ

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

АНИСИМОВ Николай Александрович

КОМПОЗИЦИОНАЛЬНЫЕ МЕТОДЫ РАЗРАБОТКИ ПРОТОКОЛОВ НА ОСНОВЕ СЕТЕЙ ПЕТРИ

05.13.11 - Математическое и программное обеспечение вычислительных машин, комплексов, систем и сетей

АВТОРЕФЕРАТ диссертации на соискание ученой степени доктора технических наук

Владивосток 1094

Работа выполнена в Институте автоматики и. процессов управлении Дальневосточного отделения .Российской Академии Наук.

Официальные оппоненты: Доктор технических наук, профессор Бая дм О.Л.

Доктор технических наук Болотов В.П.

Доктор фвдико-математических наук, профессор К летев А.С.

Ведущее предприятие: Институт проблем управления РАН (Москва)

Защита состоите» 1995 года а 10 часов на заседании, специ-

ализированного совета Д 003.30.01 в Институте автоматики « процессов управления Дальневосточного отделения РАН по адресу:

690041, г.Владивосток, ул.Радио, 5

С диссертацией можно ознакомите« в библиотеке Института автоматику и процессов управления Дальневосточного отделения РАН.

Автореферат разослан "/А" декабря 1994 г.

Ученый секретарь ; специализированного совета,

доктор технических наук

Б. И. Коган

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

Актуальность проблемы. Одной из ключевых характеристик информатизации современно!*» общества является псе более широкое проникновение распределенной я аараллсльвоЗ обработки информации, использование распределенных систем различного назваченая, включая локальные и территориальные информационно - вычислительные сети (ИВС). Последние годы отмечены существенным прогрессом в этом направлен ни, связанным с повышением скорости передача информации, появлением принципиально новых телекоммуникационных услуг, включая использованием технологии мультимедиа, внедрениям распределенных систем практически во сферы деятельности общества. Все это предъявляет высочайшие требовали* к характеристикам ИВС и особенно к их наде/.;ности а производительности. В то ase время важнейшие характеристики IJBC во многом опрепгляютел свейстпамя используемых них протоколов - правил взаимодействия между удялеяньшк частями ИВС. Особую роль здесь играют свойства логической корректности, т.е. отсутствие логических ошибок типа тупикозых состоитй, изпрсвзаоэттсяьяых адапов, переполнений и др. Дело в том, что ошиСкп тихого рада не могут бить обнаружены на этшах тестярсва-няя и отладки, а только па раиясм этапа логического проектирозгииа. Болоя того такой анализ протоколов иа логическую корректность ьозиоЛяи только с использованием формальных методов и, кьк показывает опыт, соответствующих автоматизированных средств. Таким образои проблема состоим в создании формальных методов конструирования протоколов ИВС, сСлйяаюписх свойствами логической корректности.

Решений этой проблемы происходит к ¿к но пути развития сбшях теорий параллельных распределенных систем, так и во нути их приложений к специфической области коммуникационных протокплов. Значительный теоретический вклад в этой областа связм с пмсяамя Р.Мпяаера., К.Петри, Ч.Хоар». Ряд существенных результатов, сгязенпых как с фундаментальными, тал и прикладными проблемам«, вкесея отечествеавыиа исслегкйатгдамв: О.Л .Бамдмая,

B.И.Варш&лсквм, Ю.Г.Карпояым, В.Е.Котозкм, В.Г.Л&>з;»з!Ш, Е.И.Пийль,

C.А.Юяицким.

Следует, едкако, отметить, что почти всо кмекнааеся результаты а области описания и аналяза. протоколе» р&спреаглеинда систем применимы только к системами небольшого размера. Когда же речь мясаит о системах реальной сложности, эти изтодц, в sjacce сгоеЭ бгед?рук>щгкся сострбсязга :'. »¡«шизе множества aoctiiíkümijk езстояявй, у к« ira яришкшмы кз-ia экепотеианально-го 1>оста числа состояшЯ. В то жз вреаи практичеехм патрсбаость требует дальнейшего развита« протоколе». Бальштество коишьзуемых протоколов мгюгофуикдковалйпы и состой es msosúscTm согтавлаюгаий - кушротоколоа, фаз, процедур. Более того, 'еозрекееты« ИВС функционируют уже в cooteít-ствии с мпогоуроымвыкя кср&рхкческй оргаякзовшили системами протоколов. Прочло втаяяо в обиход понятие архитектуры взаимодействия - скстемы

сражал, соглошгиий, термкааз да- кострооаия ыпогурcraeaux систем протоколе». Для про4кта;жгаяк такая саягм в настоящее »реыи вэ существует достаточно уйэваетваркгепьгсдх Метод». Tax стаддарткые средства, описания • прстохэгш LOTOS г Eítclle, рагркбкгашыэ в Маздународцой оргацазацна по " стаадартзладаа, хоть ts шввошаот СЕ-гцг^лдарогзгь протоколы любой стевева слгшюстя, во не coscpsíT средств, с5еспе4'лз1шк,ш; их яопгеесиую zoppsxT-шсть. Риигяке этой кробиещд розжжвэ do нуте создания иошюаздиоталышх ьгетодоз рдзрг^отсв, т.е. ¡кеиккв, казагишящх «треть слоашыс протоколыша конструкции из Сокго простых саета&лзвощях, обаскгчазаа про stwm логическую корректность рвэугалЕруккавЗ cacrevai.'

Эти обстоятельства ссдда«аьствук>т сЗ актуальности дроблены создания композикйояальшжс мехадмз 2рое8твроаакая проишаясз реальной сложности и ыногоуродзевых свэтси вротсаапоа.

Связь с планам я отраслей наук и а ар едкого хозяйства. Првдстаьлол-выв в диссертация ессзйвймжявя пргвэдаяась а рамках сяздузсщкх ирограым:

1. В рамках науч!м*ЕС<жздоватм»сг£ях тем Пдствтуга икгвтшш и процессов увраЕдата ДВО РАН:

« "Лгхоыатиааиня научных иосяедозглшй на нееднорааяой вичнедатеяыюй сети", N гос-регистрают 8X055372;

« "Разработка кэзодаэ исследования Е программных средсто иххфорыацаса-Ео - вычмыютеяыалх сетей", Н гос-рд-Естратах 01.85.0107742;

в "Йсследагзашз и разработка мгтад» анализа. н сытггза протоколе о сетей ЭВМ", N гос.рсгастр&дан 01. £'.10016815.

2. В рамках'конжурсаого иаучко-всскедов-атеяьского проекта отделения информатике, аычаслатеяшой техяякк л евтоадтизашш АН "Система автоматизированной разработки протоколоз cetcS ЭВМ".

3. В рамках проекта Российского феяда фупдазлзнтаяьнак исследований "Основы комЕозициовальпой теорий сетей Петре", грант 93-013-17372.

D указанных НИР aatop вршкмал участии р качества руководителя я от-ветствеаного исполвателя.

Цель работы. Цепью дассертгшззшкй работы язязотед создмше формальных мэдеасй и метода® разработки сложвых ывагофУ1Ш®оаальных протоколов и многоуровневых систем протоколов обладающих свойством логической корректности.

Для достикешм указакной цели в работе решаются следующие задача:

1. Разработка методологические прапцншя проектирования логической структуры ИБС.

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

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

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

5. Разработка методов спекк^йкадип я анализа корректности протокольных процедур.

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

7. Применение а экспериментальная про*ерка разработанных ! ;етс;:оз и № . ' толаткзиройишой системы для еяепяфикаиии и проектирования логической структуры коммуи2'.кацаонного оборудования для реальных И ВС.

Методы исследования 5амру;отс1 на использовании жетапоэ теории сетей Петри, методов ллгеСрлт'ссклх теорий параллельных пронесет», элеиептоа общей аЛгеСрц, •теории мпог.сста и др.

Научная новизна раСотид. Основным научным результатом работы является создание теоретических основ разработка протоколов, предстазлгюздпх собой совокупности, формальных моделей и методов н&целевных на поддержку процесса прс-ектнрования логической структуры ИБС в распределенных систем различного назначения. Научим новизна состоит в том, что разработанные ме-тзды поддерживают весь пкхл разработки логической^ структуры начиная от разработки элементарных грсиедур передачи тегшх и кончая иерархической системой протоколов, с5еспгчш,-ая при зтом сЕойства корректности. Все методы базируются на «датой формальной основе - сетях ПеТрн, что сбеспечлвгет их коянеттуйяы.'ое еляеттво, повышает ядгкЕатаость предметней области и по-звопгст использовать мощный арсенал мозкгей, метедов и ерэдета теории сетей Пгтрн.

И диссертации била получены следующие основные паучяие результаты:

1. На оснепе анализа структуры ЙВС были разработаны и обоснованы методологические пркшошы ЪроектирЬзаЛкя логической структуры ИВС, заключыоашеся в разбиении логической структуры и методов еэ проектировала* н&уржча кодаоодшоймыгосю.

2. Разработано базспое ясчисаенко сетей Петри, язляклпйеся основой ала по-строеппя компожкиопаяьаихмэдяк» ^вурайоткп протоколов. Введено новое пол«т не I- и з - точек доступа х сетя Петри, формализующих иифер-

маилю о способах композиции сетей Петра как с помощью мест, так и с помощью переходе»,

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

(а) введено ксаое понятие сетевого объекта, как сета Петрн с (-точками доступа, позволяющего опксыа^ть одновременность логических действия и явно специфицировать направления взаимодействия объекта;

(б) влвяеио привила композиция сетейш объектов, позволяющее строить сложные протокольные конфигурации из Солеа простых и исследовать кг свойства;

(в) иа основе понятия сетевого объекта спресслены основные понятия . теории протоколов - протокола и сервиса, свойство логической корректности протокола как соответствие протокола Представляемому сервису.

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

4, Введено «счисление протокольиш процедур, обеспечивающее процесс корректной разработки протокольных сЗъектоз. В частности:

(а) введено новое понятие протокольной процедуры как сети Штря с I-и е- точками доступа, позволяющее специфицировать протокольные составляющие;

(б) введены правила композиции протокольных процедур, позволяющие строить корректные протокольные объекты.

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

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

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

Предложепкке кемпозгцаопаяьиы» методы использовались в процессе логического проектирования подсистемы передачи данных - мультяпротокольЕого коммуникационного модуля, функционирующего одновременно в соответствии с набором различных протоколов (Х.25/3, HDLC, BSC, ВМО п др.), который в настоящее гремя эксплуатируется в изтоматизпронвиясГ! системе сбора, передачи п распростраяскпя гвдрометеепйформацви Росгидромета (СИЛ "ПОГОДА").

Методические материалы диссертация исг.олыовапясь в учебном процессе 'на кафздре аятомагазевдкг тучных яеедадовдвяй Московского фвзихо - технического института пря ДВО РАП.

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

а). Международных конференциях: Международна* конференция "Параллельные архитектуры il языки а Европе (PARLE'93)" (Мюпхеп, Германия, 1593)t Международная школа-семингр "Формальные модели параллельных вычислений" (Телави, 1989); Международная кояферевцня "Технология программирования 90-х" (Киев, 1991); Международная конференция "Приложения а теория сетей Петри", {Шеффилд,. Англия, 1992); Международные научные совещания по проекту CALIBAN программы ESPRIT (Ньюкастл, Англия, 1993, Сарагоса, Испания, 1S94); Международная конференции "Локальные вычислительные сети (ЛОКСЕТЬ'ИО)" (Рига, 1530); Международная конференция "Параллельные компьютерные тсхвопогяа" (Новосибирск, 1991); Международный симпозиум "Новейшие технологии и автоматизация производства (ETFA'94)" (Токио, Япония, 1994);

б). Всесоюзных конференциях, школах и семинарах: Всесоюзные конференции "Вычислительные сети коммутации пакетов (КОМПАК)" (Рига, 1983,1985, 1987, 19S9); Всесоюзная конференции "Локальные вычислительные сети (JIOK-СБТЬ)" (Рпга, 1S88); Всесоюзные школы-семинары по вычислительным се-

tum (Владивосток, 1989; Винница, 19&1; Звенигород, 1983; Рига, 1S8S; Одесса, 1987, Апма - Ата, 19SS, Минск, 1989, Алма • Ата, 1902); Всесоюзная конференция "Формальные модели параллельных вычислений" (Новосибирск, 1987); Всесоюзная конференция "Территориальные неоднородные ииформациоиво -вычиелктелыше системы* (Новосибирск,' 1988); Всесоюзный симпозиум "Сети Петри в их приложения" (Новосибирск, 1983); Всесоюзные конференции Технология программирована" (Киев, 1986, 1990); XXIX школа-семинар им. М.Л.Гадрилова "Логическое управление в распределённых системах" (Москва, 19S7), Дальневосточная мазематнчесхая школа (Находка, 1987,1983,1989,1994) и др.;

в). На семинарах и коллоквиумах Швейцарского федерального института технологий (Цюрих, 1992); университетов Эдиибурга, Coppas .(Великобритания, 1993); Аахеаа в Хилаесхайма (Германия, 1993), Айзу (Ялояля, 1994);

г). На семи парах Вычислительного вентр» СО РАН, Института автоматика и процессов управления ДВО РАН в 19вЗ-1993 гг.

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

Структура и объём райоты. Диссертация состоит из введения, восьми глав, заключения, списка литературы и приложений. Основное содержание составляет 241 страницу, в том числе 122 иллюстрация. Список литературы включает 257 наименований.

КРАТКОЕ СОДЕРЖАНИЕ РАБОТЫ

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

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

Предметом исследования настоящее работы является логическая структура ИВС м методология её разработки. Логически структура. (J1C) является продуктом выделения из общей архитектуры сети функций взаимодействия, обладающую самостоятельной архитектурой, называемой взаимодействием открытых систем (ROC), которая определяется как стандартизированные процедуры для обмена информацией между "открытыми" системами. ВОС является предметом стандартизации, которая выполняется в ряде междуяародвш организациях но стандартизации. Рассмотрим структуру ВОС, определяющую устройство логической структуры НВС.

б

Фундаментальной общепринятой когшгпыией, регламентирующей архитектуру взаимодействия на. наиболее абстрактной уровне является концепция базовой эталонной модели ВОС (ЭМ ВОС), которая имеет статус международного стандарта IS 7498. ЭМ ВОС представляет собой систему терминов, соглашений, понятий и принципов, предназначенных для конструирования открытых систем. Этот аппарат ориентирован па поддержку уровневой организации архитектуры взаимодействия о помощью тахах понятий как сервис, протокол, точке доступа к сгрвясу и др. ЭМ ВОС является как бы оболочкой, в которую встраиваются конкретные механизмы обмена между системами — протоколами уровней, которые, в свою очередь, также являются предметом стандартизации. В настоящее время процесс разработки протоколов всех уровней практически завершен, в результате чего имеется несколько сот документов общим объёмом более 20000 страниц. Следует отметить, что как ЭМ ВОС так а стандартные спецификации уровней представлены в неформальном виде с помощью естественного языка. Некоторая часть стандартов сопровождается формальными спецификациями, полученными с помощью стандартных средств формального описания Estelle и LOTOS.

Эти материалы являются исходной информацией для разработки логической структуры коакретиой ЛВС, которая представляет собой конкретную конфигурацию ВОС, задаяной »формальном виде. Таким образом под логической структурой ИВС, являющейся основным предметом исследования настоящей работы, понимается логическая реализация ВОС, т.е. проекция ВОС на конкретную ИВС, выраженной в терминах некоторого формального аппарата. Настоящая работа и ставит своей целью разработку формальных моделей и методов, поддерживающих процесс создания логической структуры ИВС.

_ Рассмотрим общий вид такой теории, сформулировав концептуальные прии-пилы разработки логической структуры ИВС. Принцип композНционалъноши проектирования логической структуры, обеспечивающий определённый стиль проектирования при котором её составляющие конструируются как композиция из менее сложных составляющих. Исходя из специфики ВОС, выделено три уровня композициональности: системный, объектный и процедурный 'ровни; Принцип единой формальной основы проектирования, требующий, чтоб все эт&пи проектировали* а» кахиюм уровне композяциональвостя выполнялись а рамках одного единого аппарата.

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

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

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

Пусть А есть некоторое множество. Мультимножеством на множестве А называется функция ц\ А —» {0,1,2,...}. Объединение, разность и произведение мультимножеств обозначаются соответственно как + ni — ßi и /ii x^/ij. Проекция мультимножества¡t на подмножество ВС А обозначается как /<[£? = {(6, п) 6 ¡i | Ье В). Запись рА означает множество всех мультимножеста на А,

Сетью называется набор JV «= (S,T,F), где S = {ai,..- множество мест; Т = {¿,,...,«„} - множество переходов, 5 П Т = 0; F .С pS х Г х /iS -отношение иицедснгности. Сетью Петри называется маркированная сеть £ = (N,\io), где N - сеть, Mo € (tS ~ начальная маркировка* Если для некоторого перехода t имеем {Q',t,Q") 6 F, то Ч = Q' и <• = Q" "называются пред- и постусловиями этого перехода. Функции *() и ()• естественно расширяются на мультимножества ö S рТ.

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

Определяются два правила функционирования сети Петри — интерлквцц-говое и шаговое. В ивтерлизингозом случае переход t €- Т считается возбуждённым при маркировке М если Ч < М. Возбуждённый переход может сработать, приведя к новой маркировке Л/' = Ai — *< -t i*, 4io обозначается как Л/[()Л/'. В шаговом случае мультимножество переходов, называемое шагом, ö € цТ считается возбуждённым, если *в < М. При срабатывании шага (М[в)М') достигается маркировка М' <= М — *G + в*. Множество маркировок, достижимых из маркировки М, обозначается как [М).

Пусть Alph есть некоторый алфавит элементарных имён. Мультипометкой сети Петри называется набор А = (Alph,o), где о-.Т ^lAlph U {г} - пометоч-нах функция с "невидимым" символом т fS Vis,. Иными словами мультипометка сети сопоставляет каждому переходу либо мультимножество, составленаое из элементарных имён, либо невидимый символ г. Функционирование помеченной сети Петри порождает её видимость: запись М(ы))\И' означает, что существует последовательность v = fтакая, что Af\tjt1...ti,)M' и a\(v) = w, где

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

Две с«ти Потри Si = (Л, 21, fi, Moi) п Eje F^ Мщ) с пометками а

и /3 омываются пвтс'рлэвипго Сзсямуляшгепио (Си-) экквапептнымя, записывается как Ei „ rsj, Sj, гели и только если существует отношение бисимуляшш 5? с [Mm) х (Л/oî) raaos, что

1. («и, Мм) е Л

2. если (M,,Mi) С й, то

(а) A/,(!K))Í,/.ÍÍ 3Щ : /МЩУ^.Ц и G Я;

(б) ЩЩ^Щ «+ ЭМ| : Mt{W))'J.!í и (M[,M'j) 6 S;

Шагсв&а C-.i-эк аквотептпвсть сетей Е» в Ц получается заменой ипдекса i на л a BbíiuecTcnuKU определевш н сбйзяачьется как Ej в та J Ej.

Для ешгшшюго и удобного проставления систем, имеющих операаяя с данными и пграиетрти, в работе ресолыугти класс сетей высокого уровня - предахатпые сети (Prciiiciie/TrMeition acts). Предикатная сеть определяется как сеть Пстрн, а которо.! матка может иметь иьбор значений - вектор атрибутов, структура которого змвеит от место, в котором расположена метка. .Переход ечлта/етса розбуадёаныit, «ели see его входные места содержат метки я ах зяйчезиа удзмхт&орзкзт опредея&пгему условию - селектору перехода. При срабатывании перехода уигзлввлавазотся вовые зкачекия вновь сгеверирозад-шлс iktc;:. Кяихячесхоа опрадепеняв ярйдпкмпшх сетей дополняется определением Пом!угкя, s которой видимые имена перекопов могут иметь также вектор зтр$Ебутоз. Как тагсгио, пргдик&тнгя сеть есть просто компактдая залась'сети Петра и шжзт бить "развёрнута." в эквивалентную сеть Петрн. В силу этих причин юг формальные викяшжн а pt&ree прегеедевы для сетей Петри.

В Главе 3 сгодится базовое исчясяеясг сетей Петри с точками доступа, на котором в носл«.".ствкн будут ncctpoeraa макэла протокояьаых структур и пра-вала я* гсияекадиа для различных уровней компогяпионвльности.

Существующий спит построегшя сетевых исчислений для опрекленных областей применения цекиизьет, что » результате получзлотся исчисления, определения операгай в которых доьольио п<укможи и техиячесхи сложны, в то ирама как иа истуятнппый смысл доаопь'-'о «сен. Помимо того, большинство исчкелекяй сияыго спедоглдмфсшшм я несут специфические черты соответствующих лр«тетпых областей. Попытки их использования в другой предметной областа встречают даольяо серьезный трудности. В силу этих причин-, в реботе провесе построегпм. еробявмяэ • ориентвроззшюго сетевого исчисления вмйояи1ется я два атааа. Самана ояр«ая*к>тс» дзв вспомогательные опера-шш ciînxpounsauna сетей с помощью переходов и с пометь» мест, для которых доказывается ряд' стандартных свойств. Затем на вх основе определяются

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

Для использования сетей в качестве опираадов сетевых операций необходима впфориашх о том каким образом сеть ио;кг.о композировать. Эта информация формализуется с помощью понятия точки доступа к сети. Определяется даа типа точек доступа — 1-точки доступа и g-точки доступа.

Пусть N = jS,T,F) есть некоторая сеть. Тогда t-точкой доступа к сети N называется набор а « {tiJ,Alph,<r), гда iid есть кия (идентификатор) точки доступа, Alph есть иеккй алфавит эпемзнтаряых mien и ir: Т —> [¡Alph U {т} есть пометочиая функция. То есть t-точка доступа есть не что иное как пометка, где видимое действие есть муЛАТикюжссгьа элементарных имён. Имя точки доступа iid необходимо для ссылок на неё.

S-точка доступа сети N есть набор f = {3id,p}, гда sid - имя (идентификатор) в-точ;;я доступа, а р С ¡iS - множество такое, что УМ, М' 6 р : М % М'. Понятие ¡¡-точки доступа есть обобщение понятия маркирозка, задающее не одну, а сразу несколько взаимно альтернативных маркировок. Как и t-точка, 8-точка имеет идентификатор jid.

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

Операция слияния переходов сетей Nt *= {Si,Tt, l'\) н Л'г = [S%>Ti, f\) чергз соответственно t-точки доступа"о » (tidaiAlpha,aa) н /} — строит сеть N' = (JV, а\\0 N3) = {S\ T',F) с aS' = SiUSj

» T'-TiUTj \ Га»! U Г,,«, где

= {i е Т («г,(0 5« г V <Ti<i) ^ ri

^луп ~ {et+e31' е„в, е яТ,т g а,(е,) = ^(е^),

сумма ©1 +ва }

Сумма 6i 4 вз называется минимальной если lis существует ©¡, 8j е fiT : г 0 <j,(Qi) = <г,(в',) и в; + ©i < е, + в,.

Овермда слияния переходов объединяет множества мест сети. Кроме того она удаляет подмножество переходов, видимых хотя бы из точек, а или 7?,

П добавляет новое множество переходов синхронизации Г1уп. Каждый такой переход формируется с помощью мультимножества синхронизирующихся переходов и задается формальной суммой 6i + Qj. Невидимые переходы не могут участвовать в синхронизации и, следовательно, пе дают вклад в множество синхронизируемых переходов. Доказан следующий факт, позволяющий вычислять множество переходов синхронизации Tlt/-„.

Тесрема. ЯроСьтсмл нахожденяя верехшюп сиихроаизишн Т,.^ для ояерадаи слкэншг перестаете сегсй сгодится ь" про&леме яахозде.чяя множества шямень-п.'Ш: 1-кг,'?.др:!Ы!Тсв 1-. сетях Петра. п

Другой фундаментальной операцией пэд сетями с то"«»«« доступа является операция слияния мест сетей. Пусть даям евтл ^ — и N1 = (5з,Гг,К2) с точкам:.! доступа ( = (о,/>г) я С = {6, р;) соответственно. Обозначим Я1 = |!,«{||»5г = М.Т1 = '(51)',Т7 « *(55)'. Тогда операция слияния мест (з-елляпне) сетзй N1 й М ®> отношецзю к ( и £ строит новую сеть !Г = {¿V, .V») = (3',Г, Г) такую, что

в 5'= 5, и 5! \ (5^5') и

• Г' = Г1иТ2\(Т1иТ1) и Т1хп и Тгхс(

F'=*Ft Uf,

Яг(Щ QAV-n)

Bo-n?pcux, спград:« сли.таня мест заменяет сливаемые места U 53 на их произяедате. Во-вторых, переходы кппидентпыг елноаемому множеству мест S' (или ргс.цешшотся па |/>з| экземпляров (или (¡оi [, соответственно). Ка:кдз2 тмгаз кош<л перехода (i,.1/), гдо Л/ £ рг (M G />1), соответствует едноЗ из возыокностгй синхроикзаски.

Длг оаерзг.вЗ t- и s - слияния аяалогичш-ш образом окрея^лятот^я их укц-ича форим, которые сссгвятстасяго обозначаются как trn:rg(N,a,l}) и smer3{N, (,'()■

Пргмеяенне cjvjoi аз бззояих операций над сетью с точками доступа может пригестя к cymsств&чилн взчггкйиям f? структуры, что треЗует соответствующего яер?опр<дал«пя точек доступа, которые Суду-r называться трансфер-.пацпхми тэче« двстула и .1за';га::хггься как f я Т.д.

0 главе йзкаэзяо, '¡то сгсерг.:::<я слияния мсст обладает стгндарч ними сродством;: ксми'уг.гткяиоста я мсоаклтияясстм.

На основе даух фундаментальных операций слияния переходов и слияния мест введите* Сдзхжое исчисление сетей Петра с точками доступа (ТД-сети). ТД-сятью палыметса набор ЛР = [Ы, Г, П), где

1. Л* -- (S,T, F) сеть Петри, «взываемая структурой ооъскпи

\ {<*м,0 г'и г3}

и {«№),(<, "г), 9Ï(W,}) 11 s г„ а/, е Р<)

и I < G Г„ лл € ,■«},

- '¿KSXS'v.f-'ffS'x^fj

= {'[(SXS^ + ffi'x^Mî

« °lf(,9\S'5) -I- x,,'*^1

=> ?r(S\S*) + AU ^t'fS3

2. Г = {о1,оа,...,£»„} - множеств? Ь-точех доступа, » ((м/,, А/р/ц, <т;),1 е {),...,»}

3. ПС {{/,,$,£4 - иночество е-точек доступ», где

Л = (Л, (>/,) гсыавяйл а-точке, доступа,

б) ¿и (Ад) хеостеааж 5- точка доступа,

в) — (в,А<) енутре»и«»-точ4а доступа.

В отличии от.обычвой сети Петра, ТД-сеть имеет дза множества точек доступа, задающих два основных способа объсдийсяля сетей - через переходы (Г) и через места (П).

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

Множество е-точек доступа П объекта дает информацию о возможной ко.ч-позяцик сетей через места и состоит из трёх а-точек доступа с идентификаторами Л, / п </. Точка А характеризует множество начальных состояний сети ./V, которое является множество« начальных маркировок. Эта точка является обобэдешем стандартного понятия начальной маркировки, задави К" одну, а несколько альтернативных начальных мархнроаок.

Информация о завершении работы ТД-сети содержатся в точке I и представляет сь&й маоаество терминальных ыархироаск, каетижеине какой-либо из них свидетельствует о зкаершелЕЯ работы сети.

Точка доступа d сагержит ниферыздио о всех состояниях сета, т.е. всех достижимых маршроакая,

В глава вводится баэоаоо всчасяеввз ТД-сотей, состоящее из сиределевия »лекептарцой ТД-сети в шести операций рад ТД-сетами,

Элементарной ТД-сетью ТД-сеть (А^Г.П), где N «= (¡>,Т,Р) - сеть с 5= км.?" - {<},*■ = {(*„<), (м5>} И Л - {{4,}},/» {{*,}},

с1 = {}, {з2}}. Элементарная ТД-сеть сестсат из сщкого перехода 2 с одним входящим и одним выходдщкм мгеташ. Вхаокое »юсто 31 задает голозцую з-тачку доступа к, а выждаое место «з - хвостовую а-точку /, что определяет начальное в конечное состоянаа. Ваутрешгяа точка Л задает всевозможные состояния сети - {«1} в {«'а}.

Пусть АР, = (N,,^,11.) и АР» = (^„Г,,Ца> - ТД-сети сП! =-. {к,н На = {Ма,<*а}.

Послчдовагяглънах композиция ТД-еетей АР, я АРг строкт ТД-соть

(А?!; АРг) =■ «вы Л»),Г, ИIV,{Ьик¿1 и¿))

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

Выбор (альтернативке* келтмичиг,) ТД-сстей АР» и АР» строит ТД-сеть

(АР1 [] АРт) - (ятегд((Я, ы®ц ЩХЫ и Р„ МЛ и ¿,}>

Пары.;слы1ая кэлпо-зичия ТД-сегей АР\ и АРг строит ТД-сеть

№ а||е Я,) = {(Л', „И, I 7 е г, игл 1«,/»}),{Л,!,<«}>

с /( = Ь, I -- ¡19 /¡, Л = ¿х »г!,, где р, <8>р-2~ {¿и у | г € Р\,у € р-х) Параллельная композит!« объединяет цте ТД-сети с.чияпнем через соотпетсткующке Ьточки доступа.

/ГтерацаяТД-сети ЛР-, сг рочт ТД-сеть *(£,) - (зпегд(,\\,!1Х,М, 1\, {Л^'ь'-ч )) Итерация заключается в слгштк мест через гртозпую п хвостовую точки доступа сети.

Разрушение ТД-сетсй Л 1\ и АРг есть 'ГД сеть

(ДР, [> ЛРг) = {(А-, л®» Л'з),Г, и^Л^ь/ьЛиЛ,}).

Ггри разрушении ТД-ссти соединяются слиянием «ест переэ внутреннюю точу доступа первол сети н головную то«у доступа второй.

Глава 4 посвяшпяа взспеяню формального аппарата, поддерживающего уровень система. Осиояивгись па базовом исчислении егтей Петри с тонкими ло-ступв, вводится нтаос пояятче сетевого сОгехта., отладки над ебьехтгми, понятие эквивалоптогти сохектта, гатерзр<гтышя объектов н терминах логической .структуры ИБС.

Сетевым объектом вшиваете* набор Е — (2,Г), № Е есть сеть Петри, на-зыгадмая структурой объекта, а Г = {оь...,й„} - множество 1-точех доступа. Иными словами объект сс'сь сеть Петря с множеством пометок. Из вне с объектом можно вг.гпмож-йстьоэг.т!, га, в чгстотсти, :;2блгодать за его поведение!.; только через точки доступа. Очевидно, что поведение объекта в различных точках доступа может быть рмда<шьм. Так ер&Евтывамие некоторого перехода I может быть "видно" из г ста точек доступа, но вод различными именами. Если же в некоторой точке переход помечен т-егм волом, го а 'этой точкз оп "невидим* и через н?го невозможно взглжг-лсЯетакв в з'тоГе точке. Однако в другой точке этот же'переход может быть "видим* к через него позмоаско пзаикодепствяе.

Точка доступа, лз которой все переводы "невидны", т.е. € Т : е(1) а г, будет называться тр'Е^пли'ой точкой доступа или г-точкой доступа.

Графически объект изображается двумя способами. Первый способ, называемый сетевым способом представлен'.?! объекта, заключается в изображении объекта с помошыс сети Петри, у которой переходы помечаются несколькими именами, где каждое пня содержат и идентификатор соотвегствукние-л '."очки доступа. Используется также и схематическое представления, в котором объект изображается прямоугольником, а точки доступа исходящими из него линиями. Далл; объект Е с. точками доступа сг|, ...,«„ будет записываться как Е[а,, ...,о„].

Операция комио-.ишш двух оЗъекточ Е] (Х|,Г() я Е3 — (Ег,^) через точки доступа а & Гг и 0 Я Г2 строит чопмй объект Е ~ (Г.. Г) = (£,',), г не X = ((Д?| „¡,1 Л'г), Л/оI и ''оа) " Г - П и Гз \ {о,/?}. Иным« словами структура

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

Частным случаем операции композиции объектов является "чистая" композиция, т.е. композиция без синхронизация, которая определяется как композиция через г точки доступа: (Ех jj| Ег) "=/ (£i т][.

Операция абстракции объекта Е — (£,Г) ио отношению к подмножеству точек доступа Я С Г строиг новый объект Е1 - тц(Е) — (Е,Г \ Я). Иными словами операция абстракции просто удаляет из определения объекта подмножество точек доступа, не измокая его структуры (сети £) и, следовательно, не изменяя поведение объекта в оставшихся точках доступа. Этот оператор необходим, хогда имеется полная спецификация объекта, но которая слишком избыточна в конкретном применении и которал должна быть упрошена.

Й работе также используется операция переименования точек доступа, которая заключается в замене одних кааткрнкгтороа другими. Операция имеет вал Ellii'i/tidi, lid'j/lid^, ...,¡¿<^/¿«<4), где каждый идентификатор tid, заменяется на ii£r

В работе показывается; что операция композиции объектов при определенных условиях обладает стандартными свойствамн'коммутатиЕности и ассовд-атинности:

(А 4/> *= № Ei) ({Ei ft) wj|7 &) = (Ei „¡|,n (Ег „Ц, £,)) Эти свойства позволяют применять операцию композиции на практике не заботясь о порядке ее применения.

Для сетевых объектов вводится понятие эквивалентности, базирующееся на бисимуляциошюн эквивалентности сетей Петри. Два объекта Ei ~ (St.Ti) и Е] - (2i,r3) называются эквивалентными в точках о € l\ t: /J С Fj, записывается как Ei „«/i Ег, если и только если tida — tidp и Ei „ksJ Еу.Тоесль объекты эквивалентны в точках доступа если, во-первых, эти точки имеют одинаковый идентификатор, и, во-вторых, маркированные сети объектов "Снсимуляцношю эквивалентны в соответствующих пометках.

Объекты Ei и Е3 называются полностью эквивалентными, что записывается как Ei а Ез, если и только если существует отношение биеммуляции Ш такое, что V» £ Г| £ Fj : Ei Ег с отношением бнеимуляшш 5R; и, наоборот, V/3 £ Гj За £ Г\ 1 Et а&р Ei с тем же отношением биашуляции й. Таким образом полная эквивалентность сбъсхтон определяется как эквивалентность одновременно во всех точках доступа.

В работе доказана теорема, гласящая, что эквивалентность'объектов конгруэнтна ио отношению к операциям композиции и абстракции, т.о. если Е, Е\, Ei - объекты и Е\ & £j, то

1. Е Ег * Е „||4 К,;

2. r„(E,) » r„(i?2).

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

1! главе аппарат объектов применяется для представления понятий протокола и сервиса, а также для постановки а решения основных задач протокольной инжеперпи из. системном уровне композициовальности. Так спецификация сервиса задаегса с пемошыо едкого объекта, называемого сервисным о&ъектом, точка доступа к которому мтерпретируются как точки доступа к сервису. Алфавит каждой точки доступа представляет собой набор примитивов сервиса, где именам г.греходол соответствуют имена примитивов сервиса, а набору термов — параметры прим8!т:;ва. Так объект сервиса с двумя точками лоступа к сервису S'N и Sff имеет вид ijij. Часто используемое понятие "среда переда-

чу" является частями случаем сервисного объекта и может Сыть представлена объектом МЕц\1<rj с изумя точками доступа I а г, в которых выполняются ко-иыеды посылки / приема блоков данных. В главе приводятся примеры наиболее расг;рсс грг.-wmiих видоз сред передача, применяемых в описаниях протоколов.

Понят« протокольного объекта т,-.;сже рстестзевко прадстявляется с вачо-пзыо объекта, где точки доступа задают взаимодействие с другими объектами. Так r-poresuiiuiwii оЗчлкт N-урояка иокет быть представлен в взде объекта PEn[S*i,Sh~iJ. 11|>отс1:ол1л1ый объект юлеет две точки доступа Sn и 5><г_ц к проточолмгым объектами керхкего и нижнего соседних уровней, соответственно. Алфавитом г;их точек доступа являютсясервисные примитивы соотвст-стаетао N- и (H-l)-ypoaiiöii. Через точку S.v-i в сервисных примитивах передайте« протокольное С:::zu соответствующие протоколу N-уроэня. В случ.их, когда необходимо сиеаяфисяровать Бзаимсд»йств1ге непосредстзен.чо по протоколу гместо TO'tsai 5/v-j лспользуется точка доступа Рц, описывающая Езгимодействаа протокольного объекта по "чистому" протоколу с удаленным протокольный обгсктсм пого уровня. Аггфзйнт этой точки доступа состоит iss набора кроютолшых блоков витых, а поведение ебье!" та из »той точки гясту-rui "яклатся" км передача / приём' протокольных блоков денных. Протокольный о¡¡testr а зтац спучхе ¡¡user вал Pß//[S/f, J. Часта, ccaScr.no в рднних протоколах (см., иглрккер, нротсагояи Х.25, IIDLC, BSC и ,??.), нспользует-гг спецификация протокольного с-?И.ект», вмгжщего только одну точку доступа по вротокочу }'n, не определяя сель с объектами иользоватсля. В этом случдо промяолышй объект прноСрммт вид P/v.vfP.v]. Кроне тою, в проточочьныЗ г£ъ>ч;г, когда это ¿лзбмянмо, могут быть включены веномога-тельпие точки доступа, нагрлиер точкя, иртдяазначевных для пз.игмодейсткни с обмктон таЯмерд я объектом управления.

Задача спег.'гфицироьишя йротокояс» ка системном урзмте состоит в построгай» конечной мо-кля протокола, а р^чхзя «»торой спм:кЛг:цкруется кроток«.!. О качестве гпстлчиых частей используются протокольные объекты ciw-ттфпцирусг'сго у[н<вчя н объект исполиугмого прптоко.таи сервиса (среди lie реяа«и ллйиых), объединенные правилом композиции. Сами исх<шы«> обы-кты

J 5

протокола и сервиса разрабатылаются кз более нижнем объекте« уровне коы-почядаонаяыюсти. Обычно используются три модели протокола - одКо- , двух-н трехуроииавц.'! модели, которые имеет соответственно следующий вид:

£* - {Р£л[//Рл] II г] || PE»[rfPN]), (!)

Ê2[5',S"1 (PËN[S'ISs, ¡!'P,-А II ME[í,r\ ¡i '/Pn 1 « (2)

S£í![5',5"¡ = {PEN\S'IStitSN-{\ ¡| SEN.: Il PE:![S"/Ss,S^}- (3)

Объект S£§ называется логической реализацией fi-сервиеа и предста&ляет собой ¡композицию двух копий N-ripo'ï окольного с.Зъекта г. объекта сервиса низле-жавдего урозня.

Исчисление объектов позволяют строго формулировать и решать проблемы анализа логической корректности протоколов и их верификации. Под анализом логической корректности понимается проверка протоколов lia наличие или отсутствие в них общих свойств таких квк тупики, непроизводительные цикли, невыполнимые команды и др. Для та,кого анализа достаточно использовать одноуровневую модель протокола, т.е. взять объект Е1 ~ (PEs/fl/fy] |j ME[í,rj ¡I РЕц[г/Рн}), который не имеет,точек доступа, т.е. есть является просто сетью Пгтрц, и исследовать полученную сеть на необходимые свойства. Следует- отметить, что большинство оО:цих свойств протоколов есте-ствешго выражаются в терминах сетей Петр». Так тупики в протоколах пряди соответствуют туникам н сетях Петри. Из живости сети следует много полезны:: свойств протоколов таких как отсутствие тупиков, невыполнимых команд, непроизводительных циклов и др. Из ограниченности следует отсутствие ситуаций переполнения буферов, конечность представления протокольных объектов.

Задача вернфикадии протоколов заключается-в доказательстве того, что нрогскол действительно предоставляет требуемый сервис. Для проведения зто-го доказательства- необходимо сравнить два объекта - следлфйкацию сервиса и его логическую реализацию с по пошью протокола и серикса ннзлежащего уров-нз. Пусть имеется спецификация N-сервиса в виде двухточечного сервисного обьекта S£n\S',S") в его логическая реализация SE§{S', S"), построеанм с помощью протокольного ойъекга PE ti и сервиса (К-1)-урсавя 1, си, (Э). Тогда N-протскол будет назыааться корректным по отношению, к сервисам S Es и S En- 1, если гыполкяется следующее равенство: SE» S-EjJ. Конгруэнтность эккпг&пенткости о&ъехткь оСесаечнвает возможность замену эталонного сервиса на его логическую реализацию и («оборот. Это гарантирует то, что при разработке (N-НУ-урозна можно использовать спецификацию эталонного N-сервиса, и попедедае (N+l)-cepsEca абсолютно не изменится при использовании реального N-ссрвиса.

Задач» иерархичедай койюзиаиа протоколов формулируется кок синтез из двух протоколов соседних уровьей общего протокола и анализ его свойсть. Исчисление объектов позволяет естсствгнным обраяогг решить эту задачу. Пусть PEn[S/4~\,Sk] и — протокольные объекты соответственно N'-

и (М+1)~урознеГ1. Их иерархическая комиочкция, обозкдчлетлач Как Р£лг,л'+1. образуется лак композиция объектов через соответствующие точки доступа:

РЕ= ГЕы)

Иерархическая композиция протоколов М- и (Н+1)-урсР-ч«й может Сыть представлена как замена о (Н+1)-уровае объекта Н-сергиса на его логическую реализацию, т.е. объекта 5Ец иа объект = см.(З). Эта подстановка оказывается корря^ттмй, о чём свидетельствует следующий факт.

Теорема. Пусть выполнены следующие условия:

1. (Л'+1)-протокол с объектом РЕ.н-ц корректен по отношению к сервисным объектам 41 и и

2. N-протокол с объектом РЕп корректен по огногт-шю а' сервисным объектам ¡1

Тогд л

1. (;ч'+ 1)-протокоп с объектом ал корректен по Отношению к сервисным объектая и ЯЕ^, гда

есть логическая реализация ^-сервиса.

2. (Н,Н+1)-протоюл с объектом РЕц,н-и ~ {РЕя§РЕ#+1) корректен по отношению к сервисным объектам 5 и

Г!

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

В Гласе 5 вводятся формальны»! ап>ират, пргдпмнгченный ял* вздлерж-ки объектного уровн* композидиоимьяоетв разработки логической структуры ИБС. Используя базовое исчисление сетей П^три с точками доступ з, вводятся понятие- протокольной процедуры, операции над протокольными процедурами, определение корректности протокольных процедур.

Протокольная процедура есть некая логический модуль, выполнявший одну или несколько функций протокола. Выполнение функции, я свою очередь, связано с приёмом / передачей прими п;®оа предостЕнляег-юго п потребляемого

сервисов, присном / передачей протокольных комшд, т.е. с этой точки зре-шгя, протоколы!ах процедура сов^шсино аналогична протокольному обьзкту и дэл»иа ииеть те же t-точки доступа, что и объект. С другой сторопц, функ-пионарозаппв кротохольных процедур ь составе объектов может иметь начало и Еониц, т.е. в процедурах должны быть явно специфицированы начальное и конечное состояли. Это позволяет определить иротолольную процедуру в виде сети 11стри с точками доступ.-. oScux »«дул.

Протокольной араг.сдурой будет нз.<й®атьсд сеть с точками доступа, т.е. набор /-" {(S, Т, F), Г, II), где {S, Т, F) есть сеть, называемая структурой процедуры; Г — {оз, ....а,} — мшшество t-точе:: доступа, с циделенвымн точками гвиа с перхцим п шшннм уроздями U, £ 6 Г, называемые оскоэ-ььиии точками; П » {Л, I,«} — множество s-то-аех доступа, соответствующих начальному, конечному а внутреннему сосюхшям процедуры.

Протокольная процедура, вьтплиалшш одну логически неделимую функцию протопопа, будет называться элементарной орочокольной процедурой. Эле-мелтгриьь: протокольные нроаесур*»' являются исходными элементами объектного уровня компознеиенапи&сти, и, а свею очередь, разрабатываются на более низком, процедурном уровне комаозптюнальностк.

При определении процедур, и отличии от протокольных объектов, множества примитивов взаимодействия Структурируются, где наделяются входящие к ьыхоншге лр5;.чцтнаы в iJCuoftHUx t-точк'ах доступа. Под входящими примитивам« и точках U или L будут пошшаться примитивы, инициатором которых хвлкютм удалённые объекты, т.е. прнгнтиьы, пришедшие как бы снизу, из се-тн. Выходящие нрнмятпгы, наоборот, инициируются сверху и предназначены Ляг посылки удглёвпому объеьту-. Пусть о — {Alph,tr) есть некоторая основная t- точка доступа процедуры. Тогд.г

Ahha ~ МрЬ\; и Ah'hi" n Alpha? = в,

где /Ир!»" есть кмека входящих примитивов, a Alpha*'' — выхеишцих.

Асклсгйч:;".« объектам, для графического нзображеаня вротакопьмей ороц':-,чуры лммдьзустс« даа вида лредстаашша — сетевой й схемйти'ший. В сетевом предп изл^ики процедуре изображаете* как сеть с помоченными перехока-ик и /юполнтхыы&Я информацией о s-тзчках доступа. Схематически, крото-гезыдо процедура будет нзоОрижатъся праиоуголышким с квадрахцхаич; (t-течкамя) и кружечками (в-точкпми}, расподокмнкдаи по периметру iinsi.io-у голь иска.

Гслокпах течка h п^оидауры Р иазиаастся czocraoC!, соли все еа места ио смеют юадпимх дуг. Хеостоизд точка I машзд&гся выгодна®, селя вся f c ьлст.л кс г,;-'.';;«'! r-uxonuux дуг. Процедура, у которой хвостовая точкл но ьыздав&к, i; ks ц «я*и «ейко й.

Пад крецецурши определяются правила комчозшми: - паследоъалтаы;,и и плр-лдсльяаз хо«ио5Biisii, pKipytuvH«'-, итермма и трансформация процедуры Е уСьСКТ. -

Лоследояатпелькая ко.ипсзпцул. Это красило композиции из двух драге дельных процедур 1\ л Яз строит новую процедуру Р = (Р\ ~> Ра). Нитуитшшил еммел операции последовательной композиции процедур заключается в том, что в конструкции (Р, >• Рг) сначала еыполижтсх процедура а затем процедура Рг, причём р3 может начать выполняться только строга поело успешного завершения Р\. Эта шерацна очень часто используется практически гю всех существующих протоколах, где есть фаза установления соединения, за которой следует фаза передачи дгцццзс.

Пусть Р\ ц Рг есть протокольные процедуры, гдд процедура Р\ имеет входную хвостовую в—точку доступ» 1\. Тогда последовательная хомйозвдия Р) и Р?, обозначаемая кал (Р1 .1» Ра), определяется как последовательная композиция со-ответст ву ющих ТД-сетей,

Параллельнаж камаозпчпж процедур* О крзтеколах часто встречаются ситуации, где некоторые функции выполняются полностью независимо друг от друга.-, т.е. соответствующие процедуры нэ ззаимодействуют друг с другом н пе пользуются общими данными. Примером таких конструкций сгляются зр> цедури передачи нормальных и срочиик блоков лонных, котортле-вьтолцяются пол?!ос7ъю независимо друг от яруга. Т*к;ге процедуры можно представлять как параллельные и для их обрхзэвнияя п предназначено правило параллся«--поЛ композиции.

Пусть Р\ и Р4 исть яротомхлздие Р.роиедури, тогда'юс параллельная композиция, обозначаемая как (Р\ ||'| Рз), определяется как "чистг-а4 парзллелым композиция соответствующих "Щ-сетвй.

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

Пусть даны дапы'дре процедуры г\ и Г;. Правило комвоэншп разрушение строятся в даз. этапа. Сначала Рг преобразуется в А(Р>.) так, что5ы 1'г(1\) могла принимать входящие команды и игнорировать ах. Затем Р( и Р» (Р1) объединяются правилом разрушения ТД-сетеа. Праобразоагнке Р3 необходимо потому, что с момента начала выполнения Рг в среде могут ешё существовать команды Рх, приём и игнорирование которых псабходомо дополнительно специфицировать.

Более строго, эта операция выглядит следующим образом. Для каждой ?:рр-кнровки в Рц М £ М™\ в которую можно попасть только нссмлох примят .кь:, добавляются переходи игнорирования пмедаяшх команд t ~ (М, а), а 6 /ИрЛ;", входные и выходные места которых соападйот а равны М, г.е. их дуги образуют петли. Переход ( = (I/, и) лз точки Ь вкдец пещ имегем а, а ¡;з то-ш» V -невиден, т.е. имеет т-пометку. Получение кримитнаа а С А!ркц процедуры Р\ специфицировано в Р?{Р\) а приводит к его игнорированию. Последнее сбссг.е-чивгется петлёй дуг (, что не приводят к изменению ссстоагшя Рг\Р\ )■ Такие

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

Далее, пусть Р\ в Яа есть протокольные процедуры и Р\ имеет простую головную точку. Тогда разрушением процедур называется процедура ( Р] о /'2) "=

№[> /:(Л)).

Лтсрацъя прмедур. Часто бывает необходимо построить циклическую Процедуру, т.е. сделать многократно цовторякнцкйс«. Для этого вводится правило терац-.ш процедур, полностью базирующееся на, соответствующей ТД-оперздги.

Пусть Р» есть Протокольная процедура с входной голозлой и выходной хвостовой" ь-точкамн доступа. Тогда итерацией Д называется процедура Р = »(Р]), определяемая кале итерация соответствующей 'ТД-сети.

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

Пусть Р = ({5',Т, Р),Г;П) есть протокольная процедура с головной точкой доступа Ь = {М1,...,М£). Тогда её трансформация в объект даёт множество объехтоз

. Если головназ точка процедуры Р простая, т.е. ¡Л| = 1 то трансформация в ебьгхт даёт один объект.

Корректность процедуры И-уроняя Р;у, использующей (Ь'-Ч^-сервлс вЕц-1, требует, чтобы есть Петри, полученная из двух копий объектов Ь/Е(Рц) и объекта сервиса 5'Ен~\ С:4Л г жиаа. для циклических процедур и достигала конечной лмркяровкя для иецнклпческой процедуры.

3 главе определяется понятие корректности протокольной процедуры. Пусть дана протокольная процедура Р>; и сервисный объект 5Ец-1- Пусть множество Е(Рлг) = - есть результат трансформации процедуры Р>; и объек-

ты. Еслл /V ппкнпчт, 'со она называется корректной, если каждая сеть

жим.. Здесь Е^Е'х С Е(Ры). '

Если Гц пепиклнчна, то она называется корректной, если б каждой сети вида 14)достижима ко;:е=л;ая маркировка А// — М* + {Л/йч_, )0+М}, где А/}, М/ € I, — начальная мг.ркнровкг, сети объекта вЕн-.

Теореме. Пусть протокольные г.роиелуры Р\ к Г\, использующие ссрвяс ЗЕу..I, корректны. Тогда корректны и процедуры: (Р| /я), {/'¡(НА), (/'1 0Рг) И*(Р|оРа). В

■Операция трансформации процедур в объект такке коррекгла, т.е. имеет место следующий факт: если процедура -рь '.'¡.кгйщгл простую головную точку доступа, корректна, то и оЯ-ьецт Е(Р) также корректен.

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

В глаге похазано, как существующие алгоритмы анализа сетей Петри могут быть использованы для построения хорректяых протокольных npoi—дур. ' Тях для анализа корректности процедур па наличие определенных логических свойств используется метод построения дереза покрытия сети Петри, что дает возможность аяалкза сети ил ограниченность. Еста сеть Петрн ограничена, то исследование дерева покрытая позэолягг проверять соотгетстнующугэ Процедуру на свойства живости - пзлпчиз / отсутствие туликся^кевмпо.гетаых операций, иеспецнфицпрокмп!!.« прими» и др.

Для верификащт процедур используется метод построчная откогаецця бя-спмулнгдга меяшу Mvaosecvj)»«! дзетяжямых жртгрса«« дг.ух сетей Петри, о ответствуюшлх протокольной цросетуре л соттветстзуюшему сервису. Этот метод можно непол^зежзть тогда, кет да обе сети Петра ограничеяы. В глазе приводятся примеру анализа ьеррск-таоста и керя^ккащга различиях протокольных процедур.

В Гляпе 7 списана автоматизированная система разрзботхи протоколов (далее по тексту Система), реализующая компззицпочальные метчяи проектирования яротоколоз. Сметена рмраСатана на персональном компьютере IBM PC в ранках графической системы MS V/indow* 3.1.

На шг.ккем ypcwœ рсалп^смл бпек,','! релг.ктор сетей Петри, позволгющкЗ рисовать и редактировать сети Петра в графическом режиме. Сдеаумншн уровень, предназначен для построения сетей Петри в алгебраическом ре;«г.ме с помощью набора операций. Д-агке, на следующем yposae, реализован архитек-. турной редактор спецификаций, г.озволяющнГг специфицировать' архитектуры, т.е. изображать объехты и конфигурация сбтдктоа на схематическом уровне. Пользователь имеет возможность! переключаться с одного редактора на другой в любой момент. Помимо редакторов в Систеиу в>.одпт подсистема анализа сетей Петря, т-тояякян«! аяаяизир&аать кгк на ейгцу.е cw?.cT?.n (иали-чие/отсутствне тупиков, ограниченность), так s! проверять пары сетей Петри на биспмугшптоинук» зкмвдлентяоеть.

Баюеый ркЗактоя сетей Петр» яоз&ояхет конструировать сети Петри в графической форме.путем рисования их элементов з окне. В частности, редактор позволяет выполнять следующие действия: помещение/удаление мест (кружочков) и переходов (прямоугольников) в лгсйую точку экрана; соединение мест и: перехопов ориентированными дугами; установка и изменение начальной маркировки сети помещением меток в места сети; изменение размеров мест (кружоч-

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

Lомами редактор шадаржпзает иерархическую структуру сетей. Согласно этой структуре, сеть Петри изображается на нескольких страницах. Каждый переход юн: место о сета та одпой стрьште мсает ¡шеть ссылку на другую страницу с другой сетью Истра. В редакторе имеются средства "путешествия'' по иерархии в обоих цап^аалмних..

Дополнительно базовы'й редактор сетей Петри имеет подсистему- визуализации функционирования сетей Петр::, предназначенной для наблюдения за сра-батиганкем переходов сетей и смену маркировок. Реализован ках ручной режим срабатызаниа, где пользователь явно указывает - какой из возбужденных переходов должен сработать, Так и автоматический, где Система сама произвольным образолг выбирает следующий нерекод. В процессе функционирования сети в специальном окна строится процесс - в виде развернутой ациклической сети -параллели:.'«! история сети (осснгапсе net). Эта подсистема может быть полезна для понимания динамически* свойств спецификаций, процессов, происходящих в моделируемых i: ¡шрзбатьшаемых системах.

ЛлгсСраичссхиИ рс^чктор сетаЯ Петри предназначен для построения сетей Петр:), используя набс-р сетевых операций, Ото позволяет конструировать сстк ь Солее композищюи&лыгам стиле, думал не в терминах условий и событий, а в терминах временных соотношений ы^жду соЗититн it квЩ-.игурличяип соСи-tv."Í.

Редактор позволяет строить сети Не»ри с поиошью следующих операций:

• злеиентарыы сеть. Эта операция помещает е ехгю элементарную сеть Л'„, т.е. сеть Петри, состоящую из одного перехода н двух мест, головного и хвостового.

о префикс. Эта операция присоединяет к ссти N, Находящейся а текущем окне, элемент арную сегь />« с помощью операции последовательней композиции : ( А'„; N).

в постфикс. Эта операция симмстричиз префиксу, но позаолгет присоединять элементарные сеть с хгдаета текущей сети: (Л'; //„);

о f;acjerfo6ame.iM¡oj? композиция- Эта операция соединяет два сети N% и Ni, расположенных в разных окнах, в одну (Л'г, Aj) посредством операции по-сп&созагельдой композиции и помещает результирующую сать в третье ск по.

« otiCajc (алътермапч-она! композиция). Эта операция объединяет две сети Л', и Л'г, расположенных в разных окнах, в одну операцией выбора: (A'i[]JVj) и поыещгет результат в третье окно.

• парсилсльиаг ксмяозичкя. Эта операция соединяет две сети N¡ и i\'¡ ь одну пграллслыгс& комяоэициеЯ (Aij^Vj), которая пмсщистся и третье окно.

• в итерация. Эта операция применяет и сети N, находящейся в окне, опера-

цию итерации: -»(Я), лягешад результат в другое окно.

Рсдактцор артигпект»}) дозволяет рисояать объекты и конфигурации из объектов в схематической форме, Он предоставляет следующие операции:

' • Понсщепие/удалелле в любую точку гхрги& прямоугольника, обозначающего объект в схематической форме. Объекту придаётся имя объекта, которое помещается ваутри прямоугольника,

в Помещение в любую точку периметра прямоугольника квадратика пли кружка, обозначающего 1- или я-тотку доступа, соответственно. Каждой точке доступа придаётся имя - яглнтафикатер точки, который располагается внутри соответственно квадратика дли кружка.

• Проважльчеотрезков ме:эду двумя томами доступа (1-тячка с (-точке», л я-точка с 8-точкоЯ), соотготстгующия кошгазяшш через эти точки доступа.

»' Изменение размеров и мсстопояожечая прямоугольника обмкта.

• Организация иерархической структуры оС/ьектез, установлением связей между объектами в стртаядгмя с другзмя ьонфлгурэднями объектов.

® Установление связей между объекте?.»« и страницами, содержащими описания сетей Петри, что позволяет определять мутреннкж» структуру объекта в сетевых терминах.

Подсистема анализа сетей Петри позволяет анализировать построенные редакторами сети Петри па логические свойства. Для этого в Системе реализован классический алгоритм построения дерева покрытия сетей Петри, что позволяет проверять сети Петри на ограниченность. В случае, если анализируемая сеть Петря оказалась ограняченпоя, <х;я кюжет &;ть дадее проверена па живость. Эти средства, позволяют гл&лязнров^ть протоколы на наличие / отсутствие логических ошибок типа дости/кямость тугспхоч, переполнений буферов, невыполнимых команд, ¡¡еснецифицировашшх приемов и др.

Подсистема гшализа содержит средства лроЬеркй двух сет? й на басимуля-циепнуто эквивалентность. Исходными данными для этого алгоритма являются построенные графы десгижимости обоих сетей (в случае, если сети ограничены). Далее алгоритм строит отношение басимулящш и в случае его удачного построения объявляет сети эквивалентными. Эти средства позволяют верифицировать протоколы, т.е. проверять их иа соо/ьетхтвн? предоставляемому сервису.

В Главе 8 описывается применение композияконапьпмх методов дл» проектирования логической структуры спещ5али}иротапногЬ коммуникационного модуля, работающего в сети передачи данных автоматизированной системы сбора, передачи и распределения гидрометеондфо^рмадик (АСПД). Этот коммуникацв-; онный модуль, названный подсистемой порёцачи данных' (ППЛ), разработан в лаборатории информационно - вычислительных систем Института гвтом&тики

и процессов управления ДВО РАН. В 18S2 - 1S93 г. в эксплуатацию вступила последняя версия ППД, учвдиьмаявя .Измгзгкив э аппаратном обеспечении АСПД.

ППД являетса мультиприггокольваи коммуникационным модулем, заполняющим промежуток между логическими каиалйьш системы обработка сообщений цсзтра ксммут&ш:и соейщиаяй (ИКС) а физнчесхамн каналами, работающими в соответствии с набором протоколов:

о Х.25/2 (HDLC) - для uotai;í¡¡o4>-;«a к сети хоихутаияв пакетов X.25;

» ВМО - протокол передача сообщений Всемирной метеорологической организации системами и ес'еснзчсаия влгзиого перехода к новой АСПД.

• ßSC-l - протЬчоя веразлчж ссоСшкый фирмы IBM для связи с ЭВМ и оборудование»! фирмы IBM каа серая ЕС .

• Асанхрояиый сбиен по интерфейсам СТЫК-2 (RS-232, ИПРС, "токовая петля")с асцедьзовйкиеи протокола упразлепна потоком XON/XOFF для гадхягачеиия; принтеров, терминалов, ПЭВМ и другой аппаратуры с последовательным интерфейсом.

» Протоколы телеграфных сетей передачи данных Минсвязи: АТ-50, ПС, ПД-200.

» Протокол работы по международной сети TELEX.

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

ЗАКЛЮЧЕНИЕ И ОСНОВНЫЕ ВЫВОДЫ

Основные выздды, результаты и pesoмгпдашш, полученные в диссертации;

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

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

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

2. Введена новая формальная модель, предназначенная для построения различных проблемно-ориентированных исчислений сетей Петри. Для этого, в частности, введено новое понятие точки доступа, формализующее информацию, характеризующую возможные способы композиции сети Петри. Выделено два типа точек доступа — 1-точки и з-точки доступа, задающие достуд к сети соответственно через переходы и через места. Использование сразу нескольких точек доступа позволяет явно спеикфиипровать яаправлацве^заимодействия, представлять одновременность логических событий как я различных точках доступа, так и внутри одной точки (муяьтинометка). 3-точка доступа является обобщением понятия маркировки сети и позволяет специфицировать несколько альтернативных событий (маркировок). Определена правила композиции через эти точки доступа и доказаны их стандартные свойства. На базе этих фундаментальных операций введено базовое исчисление сетей Петрй с тачками доступа, содержащее набор сетевых операций, необходимый для построения прикладных исчислений.

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

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

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

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

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

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

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

• Введены правила композиции протокольных процедур - последовательная и параллельная композиции, разрушение и итерация, позволяющие строить из »tease сложных процедур более сложные. Введено правило трансформации'протокольных процедур в протокольные объекты, завершающее процесс разработки протокольного объекта в связывающее системный н объектный уровни композицкоцальности.

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

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

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

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

6. РазраГютана и реализована вереи« автоматизированной системы разработки протоколов к логической структуры ИБС, реализованной на ПЭВМ типа IBM PC/AT с графической системой MS Windows 3.1. Версия включает трёхуровневый графический редактор сетей Петри, позволяющий специфицировать протоколы на процедурном, объектном к системном уровнях композици-оиалыюстк. Редактор снабжен средствами визуализация поведения сетей, позволяющих изучать динамику спецификация. Версия системы содержит средства анализа сетей Петри и проверки их на бисимуляциониую эквивалентность,

предназначенную для анализа логической корректности протоколов и верификация протокольных процедур.

7. Разработанные формальные модели в методы были использованы для проектирования логической структуры телекоммуникационного модуля - подсистемы передачи данных, функционирующего в соответствии с множеством протоколов (Х.25/3, HDLC, BSC-1, ВМО, и др.) и эксплуатирующийся в сети передачи данных, автоматизировав яой системы сбора, передачи и распределения гидрометеоипфорцацяи.

Список литературы

[1] Аниси»»в H.A. Алгебраический подход к формализации в верификации структуры протоколе» на ослоэе теории сетей Петря. // Вычислитель-вые сети коммутации пакетов: Тез. докл. IV Всесоозн. конф. КОМПАК'85 (Рига, 15-17 ит. 1985). - Рига: ИЭВТ АН ЛатвССР, 1ÜS5, ч.1, с.158-162.

J2] Ависвжэа H.A. Формализация сервиса вмчислатеяызой сета на ©слове алгебраического подхода ¡1 Одаваадд&тыЯ Всесоюзный семнкар по вычислительным сетям (Рига, екмбрь 5КЗ),-М: ВИНИТИ, 1S3Ö, ч.2, с.14-19.

[3] Аиисимоа H.A. Формальное описание траяспортиого протокола на основе теория сетей Петра // Системное программное обеспечение автоматизации научных исследований / Сборник каучпых труде®. Владивосток: ДВНЦ АН СССР, 1986, с.27-36. "

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

' [5j Анисямоа H.A. Рекурсивное определение протскояоз па основе теории сетей Петри // Автоматика и вычислительная техпзка, 1837, N 5, с.3-7.

. [6] Аиисимоа H.A. О формализации иерархии протоколов на основе теории • сетей Петри.// Вычислительные сети когшуганва пакетов: Тез. дохл. V Всеооюзн. копф. КОМПАК'87 {Рига, 27-® «т. 1987). - Рига: ИЭВТ АН ЛатвССР, 1987, ч.1, с.228-232.

[7) .Анисимсв H.A. О задаче веряфвмгцин протоколов, мдалных сетями Петри // Двенадцатый Всессягапый семинар гн> вычяеявтеяьпым сетям (Одесса, октябрь, Ш7), -М.: ВИНИТИ, 1567, ч.2, с.31-35.

¡8) Анисимоз H.A. Формальная модель для разработка а формального описания протоколов // Автоматика а вычислительная техника, 1988, N 6, с.З-10.

(9] Аннсшлов H.A. Формальное опксавие транспортного сервиса информационно - вычислительных сетей // Проблемы информационных систем / MQ-НТИ, 1988, бьш.4, С.12-23.

[10] Анискмов H.A. Формальнаямодель языка LOTOS на основе теории сетей Петр к Ц Тринадцатая Всесоюзная школа-семинар по вычислительным сетям (Алма-Ата, 1988), -М-; ВИНИТИ, 1988, ч.2, с.34-39.

[11] Анисимов H.A. Сети Петри Пах формальная модель языков Estelle и LOTOS // Лекальные вычислительные сети: Тез. докл. 3 Всесоюзной конф., (Рига, 25-27 окт. 1888). - Рига: ИЭВТ АН ЛатвССР, 1988, ч.1,

. с.б-10.

[12] Анисимов H.A. Теоретические основы автоматизированной разработки протоколов f / Территориальные неоднородные вычислительные системы: Тез. докл. Всесоюзц. коцф. (Новосибирск, 2-4 ноября, 1988), - Новосибирск: ВЦ СО АН СССР, 4.2, с.110-112.

(13} Auiicumod H.A. О задаче анализа корректвостн протоколов, заданных с 'помощью сетей Петри /} Системное программирование и автоматизация научных исследований / Сб. научн. тр., Владивосток: ПВО АН СССР, 1938, с.5-12.

[14] Анисимов H.A. Алгебра регулярных ыакросетей для формального описания протоколов сетей ЭВМ //„Формальные м одела параллельных вычислений / Сб. научн. трудов. Псд ред. Котова В.Е. Новосибирск: ВЦ СО АН СССР, 1988, с.62-€8.

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

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

[17] Анисимов H.A. Иерархическая композиция протоколов // Автоматика и вычислительная техника, 1990, N 1, с.3-10.

[18] Анисимов H.A. Об использовании оператора состояния a-языке спецификации протоколов LOTOS // Локальные вычислительные сети: Тез. докл. IV Межд. конф. ЛОКСЕТЬ'ЙО, (Рига, 9-11 окт. 1890). - Рига: ИЭВТ АН ЛатвССР, 1690, с.287-291.

[19] Анисимов H.A. Определение семантики языка спецификации LOTOS с помощью сетей Петри // Шестнадцатая Всесоюзная школа - семинар по вычислительным сетям, - М.: ВИНИТИ, 1991, ч.2, с.119-124.

{ЗЯ} Лииснмов 'ГГ.А., (Блоыроэ В.К., Герасимов B.D., Голенков Е.А. Якяейгшй протокол взаимсяейстпия коммутаднониой ЭВМ с главкой ЭВМ // всесоюзная школа - семинар по вычислительным сетям (Владивосток, 1980), -М.: ВИНИТИ, 1980, ч.Ш, с.8-10.

|[21] Аннсимов H.A., Герасимов В.В., Гоягнко» Е.Л. Средства синхронизации процессов пользователеЗ п транспортной станции в сети ЭВМ // Пятая Всесоюзны школа - семинар по ьичислятельным сетям (Владивосток, )980), -М.: ВИНИТИ, 1980, ч.Ш, с.11-13.

{22] Аннсимов H.A., Герасимов В.В., Голеикоз Е.А. Архитектура в вопросы реализация транспортного уровня сета ЭВМ // Шестая Всесоюзны шхо-ла - семинар по вычислительным сетям (Вкнннца, 1981), -М.: ВИНИТИ, 1981, ч.Ш, с.78-81.

{23] Аш;смисв {i.A., Бломроз S.K., Герасимов S.S., Норозенко A.B. Об эхспе-рнмеитаямсм участке сетя // Шестая всесоюзная школа - семинар по ёычислительным сетям (Вняипги, М), -М.: ВИНИТИ, Î5SI, 4.IV, с.72-75.

(21) Аииашоя H.A.,ГерасимовЭ.В., ГояеяконЕ.А.Обмен соо&типями между з«дачами ОС ЕС // Прнхладаняа информатика. Зиц.2, -М.: Фнлаясм я • статистика, 1982, с.78-82.

{25} Аяисимса H.A., Голенкон Е.А. Об одной реализация транспортного урчали для вычислительно.? сети // Прняладакая и.тферматяка. Вип.2, -М.: Фкнаксы я статистика, 1933, с. 184-194.

(26] Аннсимов H.A., Голенкоа Е.А. Использование сетей Петри для формального описания транспортного сервиса // Вычислительные сета коммутация пакетов: Тез. докл. Ш Всесоюзн. конф. КОМПАК'83. - Рига: ИЭВТ АН ЛатвССР, 1983, ч.1, с.76-80.

{27) Аниснмо» H.A., Перчук В.Л. Представление протоколов обмена секвенциальными автоматаия и сетями Петря // Язв. АН СССР. Техн. кибернетика, 1086, N 1, с.74-80.

(28) Аннсимов H.A., Голенкоа Е.А. О технология разработки сетевого программного обеспечения Ц Технология программирования: Тез. докл. 11 Всесоюзн. конф. (Киев, 18-21 ноября 1986г.) -Киев: ПК АН УССР, 1986, с.92-94.

[29] Аннсимов H.A., Виноградов В.В., Голенков Е.А. Организация транспортной службы на ЕС ЭВМ // Системное программное обеспечение автоматизации научных исследований / Сборник научных трудов. Владивосток: ДВНЦ АН СССР, 1985, с.22-27.'

£301 Анисиыов П.А., Бузив A.M., Голекков Е. А. 05 автоматизации проектирования сетевого программного обеспечения * // Двенадцатый Всесоюзный семинар со вычислительным сетям (Одесса, октябрь, 1987), -М.: ВИНИТИ, 1937, ч.2, с.Зб-41.

[31] Аняашоз Н.А., Бузин A.M., Голеннов Б.А. Технологические принципы разработай программного обесцочсяаа информационно - вычислительных сетей // Управляющее системы и машзпы, 19S8, N 4, с.88-91.

[32] Aeucumod Н.А., Новицкий А.Ю. 0 верификации протоколов на основе биснмуляциоавой эквивалентности сетей Петри // Вычислительные сети коммутации пакетов: Тез.докл.У! Всейяози. копф. КОМПАК'89, Рига: ИЭВТ АН Л&твССР, 1989, с.222-226.

[33] Ациашов Н.А., Голекков Е.Л., Ккыццсккй К.П., Коваленко А.А. Графически.^ LOTOS на Сазе сетей Петри и средства его обработки // Технология программирования SO-x / Тез. докл. ыежд. конф. (Ккгз, 14-17 мая, 1S91), - Киев: ПК АН УССР, 1S31, 97-23.

[34] Аянсамо» II.А.,Коваленко А.А., Иостуналъсаий П.А., Симанчук А.С. Гра-ф,[чес1а:й редактор йротокояов сетей ЭВМ на базе сетей Петри // Семнадцатая Международная школа - семинар по вычислительным сетям (Алма-Ата, 1902), -М.: ВИИКТЙ, 1992, ч.2,.с.З-8.

[35] Анксимоо Н.А., Кйз&лсг.ко Л.А. „Посту па-искна П.А., Симанчук А.С. Автоматизированная система СЕагефпкакия протоколов на базе сетей Петри // Тез. докл. V совещания по раепр^неяейным вычислительным системам и сетям (SDS-92), (7-11 септ. 13S2, Калининград), -М: ШШИ РАН., 1892.

[36] Aniaimov N.A. A Petri Net Mode! of LOTOS, A Protocol Specification Language. In: Ccmputers'SS: Pros, intern. Csnfcrcr.cc, Bratislava, Czechoslovakia, (1SS9) 182-16".

[37] Anisimov N. A. A Petri Net Entity cs a Formal Model for LOTOS, a Specification Language for Distributed and Concurrent Systems, ia: Parallel Computing Technologies, Ы. N. N. Miraikov (World Scientific, 1S91), 440450.

[33] Aniaimov N.A. An Algebra of Regular M&croncts for Formal Specification of Communication Protocols. Computers and Artificial Intelligence, 10 (19Э1), 541-5GO.

[39] Arisimov N.A. A Notion cf Entity Based on Petri Nets, in: Proceedings of i!it 1901 IFAC Workshop on Dkcrcle Evctit System Theory and Applications in Manufacturing and Social Phenomena, ed. Yu-Chi Ho, Ymg-Ping Zheng, Slieuyaag, P. It. China, (International Academic Publisher, 1991) 142-147.

[40] Anisimov N.A., Kovalento A.A., Pcstupalski P.A.,8imancuk A.S. A Graphical Petri Net Based Editor for Visualization of Distributed and Parallel Systems. Lecture Notes in Computer Science, 031 (Springer-Ver'.ag, 1992) S47-843.

¡41} Anisimov N.A. A Dbablinj of Event Structures, in: PARLE'DS, Parallel Ar- chilectures and Language Europe, cd. A. Bodem M. Reeve, G. Wo!f, Lecture Notes in Computer Science, SSI (Sjrinser-Vcriag, 1SS3) 721-723.

(42) Anisimov N.A., Kovalaako A.A., PostupaVJa P.A. Two-Levels Formal Model for Protocol Specification Based on Petri Nets, in Network Information Processing Systems. Proc. of tiie IFIP TC6 int. Symp.ed. K. Boyanov, (Bulgarian Academy of Sciences, 1093) 143-154.

[43] Anisimov N.A., KovaJeako A.A., Postupalski P.A. Compositional Petri Net Environment, in: Proc. of the 1094 IEEE Symposium on Emerging Technologies & Factory Automation: ETFA '94, November 6-10, 1S91, Tokyo, .Japan, 420-427.