Введение к работе
Актуальность темы.
На современном этапе развития информационных технологий и средств передачи информации особую значимость имеют сети связи, соединяющие в единое целое совокупность разнородных вычислительных мощностей . Сети такого типа, получившие название информационно-вычислительных сетей ( распределенных систем ), с момента возникновения и до сегодняшнего дня являются" предметом самого пристального изучения как отдельных исследователей, так и крупных национальных и международных научно-технических ассоциаций, таких как Международный консультативный комитет по телефонии и телеграфии ( МККТТ ), Международная организация по стандартизации ( МОС ), Европейская ассоциация производителей вычислительных машин и др.
Этими организациями было положено начало создания единых стандартов, позволяющих организовать обработку информации в подобных распределенных системах и воплощенных в виде системы протоколов управления информационным обменом, реализуемых в программно-технических комплексах сети.
Среди исследователей проблем стандартизации можно назвать Кларка, Сипсера, Флинта; Дэвиса. в нашей стране этими проблемами занимались Сакойленко С.И., Рякин О.м., Зайцев с.С., Пра-нявичус Г.Й., Жигулин Л.Ф., Горностаев Ю.м..
Процесс эволюции информационно-вычислительных сетей показал, что первоначальные неформальные описания протоколов не подходят для проведения анализа и разработки подобного рода систем. Выход из создавшегося положения может быть найден только путем применения методов формального описания ( МФО ) протоколов и сервисов, полно и однозначно определяющих все аспекты взаимодействия.Причинами отсутствия общепризнанного МФО являются:
сложность, которая вызвана громоздкой структурой самих протокольных объектов и комбинаторной сложностью задач анализа взаимодействий, о
большое разнообразие протоколов,
ряд аспектов протокола, трудно поддающихся описанию, противоречия между требованиями к описаниям всеобщих стандартов и описаниям для реализации в конкретном программно-аппаратном окружении.
Таким образом, от выбора МФО зависит, насколько эффективно можно разрешить любую из вышеперечисленных проблем, в том числе и задачу верификации описаний протоколов и сервисов распределенных систем.
В данной работе используется метод формализации ЯСМОД ( Язык Сетевых моделей ) , относящийся к пограничным методам формализации протоколов и сервисов, с которым могут работать любые методы верификации, поскольку ЯСМОД обьединяет достоинства описательных возможностей обеих групп моделей формализации протоколов и сервисов. Описательная мощность ЯСМОД позволяет создавать формализации, ориентированные как на реализацию ( описания протокольных объектов ) , так и на проведение комплексного анализа всей системы; вцелом ( описание сервиса . ). Среди различных областей применения ЯСМОД наиболее актуальной оказывается область верификации протоколов и сервисов в распределенных системах. :
Цель работы
Целью работы является исследование задачи верификации протоколов и сервисов распределенных систем и- разработка методов ее решения. В процессе достижения цели ставились и решались следующие задачи:
проведение сравнительного анализа методов формализации и верификации протоколов и сервисов распределенных систем,
постановка задачи верификации для выбранного метода формализации и верификации протоколов и сервисов,
формализация процесса верификации на основе семантического эквивалентирования иэ общей теории систем,
разработка алгоритма редукции для решения задачи верификации протокольных объектов,
проектирование программного комплекса для анализа пос-
ледователыюстей взаимодействий двух протокольных объектов ( протокольный анализатор ),
- реализация протокольного анализатора в виде пакета
прикладных программ администратора сети и сетевых раз
работчиков.
Методы исследования
Для решения задачи верификации протоколов и сервисов используется метод семантического эквиоалентирования, предложенный академиком Горбатовым В.А.. Работа протокольного анализа-тора основывается на синтаксическом анализе автоматной грамматики и разработанном алгоритме редукции ациклических графов специального вида.
Научная новизна
В качестве результатов проведенного исследования можно представить следующие положения:
постановка задачи верификации протоколов и сервисов с точки зрения запрещенных фигур семантического эквива-лентирования,
разработка алгоритма редукции сетевой модели для решения задачи верификации протокольных объектов,
обоснование использования разработанного эвристического алгоритма анализа контекстов свернутой сетевой модели для решения задачи верификации в условиях повышенной размерности,
разработка метода анализа взаимодействия двух протокольных объектов на основе модели локального сервиса.
Практическая значимость
Результаты диссертационной работы нашли следующее применение:
- разработанные алгоритмы верификации локального сервиса
и протокольного объекта были положены в основу реализа
ции программного комплекса протокольного анализатора,
протокольный анализатор был внедрен в виде пакета прикладных программ администратора сети и сетевого разработчика, о чем имеется соответствующие акты о внедрении,
результаты работы протокольного анализатора для протоколов Х.25, V.42 и V.42bis говорят о возможности анализа задач большей размерности по сравнению со стандартным тестирующим оборудованием.
На защиту выносятся:
метод решения задачи верификации на основе семантического эквивалентирования,
алгоритм редукции сетевой модели к канонической модели на шести вершинах с эвристическим подходом к анализу контекстов модели,
программный комплекс протокольного анализатора в виде пакета прикладных программ для администратора сети и сетевого разработчика,
результаты работы протокольного анализатора для протоколов Х.25, V.42 и V.42bis.
Апробация работы
Результаты работы представлены в докладах на 15 и 17 Международных симпозиумах " Логическое управление.. Интеллектуальные информационные технологии и стратегии " в-1992 и 1994 г.
Раскрытие результатов
Материалы диссертационной работы полностью опубликованы в трех статьях в сборниках Международной академии информатизации.
Достоверность результатов
Достоверность разработанных методов, алгоритмов и программных средств подтверждена результатами внедрения, о чем имеются соответствующие акты, а также апробацией работы на на-
.-7-
учных симпозиумах.
Структура и объем работы
Диссертация содержит 4 главы, введение, заключение, 3 приложения, 22 рисунка, 4 таблицы. Общий объем - 190 страниц. Список использованных источников содержит 50 наименований.
