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

г Г Б ОД 2 9 ДПР 1396

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

КОЛЬЦОВ ДМИТРИЙ ВЛАДИМИРОВИЧ

ВЕРИФИКАЦИЯ ОБЪЕКТОВ И СЕРВИСОВ В РАСПРЕДЕЛЕННЫХ СИСТЕМАХ

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

Автореферат диссертации на соискание ученой степени кандидата технических наук

' ' У : :

Автор .<,'• • ' Научный руководитель:

кандидат технических наук, доцент Гусева Анна Ивановна

Москва 1996

- г -

Работа выполнена в Московском государственном инженерно-фи-зическои институте ( техническом университете ).

Научный руководитель - кандидат технических наук, доцент

А.И. Гусева

Официальные оппоненты - доктор технических наук, профессор

В.А. Горбатов

кандидат технических наук О.В. Перевицкий

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

Защита состоится ЧИ^' 199бг- в ^ час. на

заседании диссертационного совета Д053.03.04 в Московском государственном инженерно-физическом Институте (техническом университете) по адресу: 115409, г.Москва, Каширское И., Д.31., г. 324-84-58; 324-91-67.

С диссертацией можно ознакомиться в библиотеке МИФИ

Реферат разослан 1996Г.

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

Ученый секретарь диссертационного совета доктор технических наук,

профессор _УВ.Э. Вольфенгаген

/ * ,. I

Подписано к печати "- С" I 1996г. Заказ > Тираж 80 экз.

Типография МИФИ, Каширское ш., д.31

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ Актуальность темы.

На современном этапе развития информационных технологий и средств передачи информации особую значимость имеют сети связи, соединяющие в единое целое совокупность разнородных вычислительных мощностей. Сети такого типа, получившие название информационно-вычислительных сетей ( распределенных систем ), с момента возникновения и до сегодняшнего дня являются' предметом самого пристального изучения как отдельных исследователей, так и крупных национальных и международных научно-технических ассоциаций, таких как Международный консультативный комитет по телефонии и телеграфии ( МККТТ ), Международная организация по стандартизации ( МОС ), Европейская ассоциация производителей вычислительных машин и др.

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

Среди исследователей проблем стандартизации можно назвать Кларка, Сипсера, Флинта, Дэвиса. В нашей стране этими проблемами занимались Сакойленко С.И., Рякин О.м., Зайцев с.С., Пра-нявичус Г.Й., Жигулин Л.Ф., Горностаев Ю.м..

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

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

о

большое разнообразие протоколов,

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

Таким образом, от выбора МФО зависит, насколько эффективно можно разрешить любую из вышеперечисленных проблем, в том числе и задачу верификации описаний протоколов и сервисов распределенных систем.

В данной работе используется метод формализации ЯСМОД ( Язык Сетевых моделей ) , относящийся к пограничным методам формализации протоколов и сервисов, с которым могут работать любые методы верификации, поскольку ЯСМОД объединяет достоинства описательных возможностей обеих групп моделей формализации протоколов и сервисов. Описательная мощность ЯСМОД позволяет создавать формализации, ориентированные как на реализацию ( описания протокольных объектов ) , так и на проведение комплексного анализа всей системы;вцелом ( описание сервиса . ). Среди различных областей применения ЯСМОД наиболее актуальной оказывается область верификации протоколов и сервисов в распределенных системах. :

Цель работы

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

- проведение сравнительного анализа методов формализации и верификации протоколов и сервисов распределенных систем,

- постановка задачи верификации для выбранного метода формализации и верификации протоколов и сервисов,

- формализация процесса верификации на основе семантического эквивалентирования из общей теории систем,

- разработка алгоритма редукции для решения задачи верификации протокольных объектов,

- проектирование программного комплекса для анализа пос-

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

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

Методы исследования

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

Научная новизна

В качестве результатов проведенного исследования можно представить следующие положения:

- постановка задачи верификации протоколов и сервисов с точки зрения запрещенных фигур семантического эквива-лентирования,

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

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

- разработка метода анализа взаимодействия двух протокольных объектов на основе модели локального сервиса.

Практическая значимость

Результаты диссертационной работы нашли следующее применение :

- разработанные алгоритмы верификацйи локального сервиса и протокольного объекта были положены в основу реализации программного комплекса протокольного анализатора,

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

- результаты работы протокольного анализатора для протоколов Х.25, У.42 и \Z.42bis говорят о вбзможности анализа задач большей размерности по сравнению со стандартным тестирующим оборудованием.

На защиту выносятся:,■■■■■

- метод решения задачи верификации на основе семантического эквивалентирования,

- алгоритм редукции сетевой модели к канонической модели на шести вершинах с эвристическим подходом к анализу контекстов модели,

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

- результаты работы протокольного анализатора для протоколов Х.25, V.42 и У.42Ьхз.

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

Результаты работы представлены в докладах на 15 и 17 Международных симпозиумах " Логическое управление.. Интеллектуальные информационные технологии и стратегии " в-1992 и 1994 г.

Раскрытие результатов

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

Достоверность результатов

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

прог-о чем на на-

учных симпозиумах.

Структура и объем работы

Диссертация содержит 4 главы, введение, заключение, 3 приложения, 22 рисунка, 4 таблицы. Общий объем - 190 страниц, список использованных источников содержит 50 наименований.

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

Во введении обоснована актуальность исследуемой темы и приведена общая характеристика работы.

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

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

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

Всю совокупность известных методов формализации можно разбить на две части : автоматные методы и методы допустимых последовательностей. '

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

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

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

Модели, принадлежащие х группе моделей допустимых последовательностей, рассматривают- обьект спецификации в виде " черного ящика " , т.е. с точки зрения наблюдаемых событий по взаимодействию с этим обьектом. Формальные описания, построенные на основе таких моделей, довольно кратки и не подвержены такому росту размерности, как те описания, о которых говорилось выше, поскольку они строятся, используя различные ' формульные представления свойств описываемых обьектов, однако у них тоже есть свои недостатки. Громоздкость преобразований и сложность формализации новых свойств описываемых обьектов существенно затрудняет анализ таких спецификаций, а ■ абстрактность описаний не способствует их реализации. Методй верификации, применяемые для анализа этих описаний относятся к методам анализа допустимых последовательностей.

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

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

На основании такого анализа методов формализации и верификации протоколов и сервисов был выбран язык сетевых моделей

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

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

Суть семантического эквивалентирования сострит в том, что при переходе от системы S с моделью Ч1,, =< ¥а ^i, ,Р0 > к системе S" с моделью Ч'с~=< ^а" »^ь->р0~ > предикат Р0~ сохраняет свою истинность в случае, если ни одна из моделей и Ч^" не содержит в виде собственной подмодели запрещенные фигуры 3 ~ и 3~ такие, что Ч,аз<<Ч,аз"' и Ч^з«"Рцз" • Запрещенной фигурой преобразования Ч'ь называется подмодель Ч^., « Ч*а такая,

что Р0 ( 4*3 3 ,Vb )=0, и при удалении или расщеплении хотя бы одного элемента из Ч^з Р0 ( ^аз »^Ь )=1-

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

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

не находит отражения в последовательности событий локального сервиса.

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

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

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

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

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

вершин 1000 дуг ). Сложность такого перебора оценивается как 0( и" ). Для того, чтобы избежать полного перебора вводится следующее допущение: при проведении любых построений считать, что среди элементов вектора контекста свернутой модели на 6 вершинах существуют функционально независимые элементы, изменение значений которых не связано с изменением значений других элементов. Сложность такого перебора оценивается как 0( тп ).

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

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

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

Разработанные и исследованные алгоритмы были использованы при проектировании и реализации программного комплекса протокольного анализатора.

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

Протокольный анализатор состоит из четырех частей •

- подсистемы формирования последовательности Запрос-Ответ,

- подсистемы верификации, включающей в себя анализатор,

- подсистемы тестирования,

- программы-монитора.

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

Протокольный анализатор был апробирован на данных из совокупности передач, прошедших за сутки по одному логическому соединению протокола Х.25. . 5

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

Возможности адаптации протокольного анализатора к но-

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

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

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

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

ОСНОВНЫЕ РЕЗУЛЬТАТЫ

В процессе проводимых исследований были получены следующие результаты:

1. В результате проведенного сравнительного анализа методов формального описания и верификации протоколов и сервисов был обоснован выбор метода формализации ЯСМОД ( Язык Сетевых моделей ) , относящегося к пограничным методам формализации протоколов и сервисов, с которым могут работать любые методы верификации.

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

3. Безошибочность и адекватность описаний сервисов и протоколов впервые были доказаны на основании формализации запре-

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

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

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

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

7. Практическим результатом решения'задачи анализа трафика протокольных взаимодействий в распределенных системах стал программный комплекс протокольного анализатора. Объем программного комплекса составляет 328К.

8. Результаты использования протокольного анализатора для сетей, работающих с протоколом Х.25 говорят о значительных преимуществах анализатора по сравнению с остальными протокольными тестерами с точки зрения объемности обработки обнаруженных ошибок в работе сети.

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

Публикации по теме диссертации

1. Гусева А.И., Кольцов Д.В. Характеризационное управление при верификации протоколов и сервисов в распределенных системах. В кн. Материалы 15 Международного симпозиума " Логическое управление. Интеллектуальные информационные технологии и стратегии. '", Москва, Международная академия информатизации, 1992г., с. 76-78

2. Кольцов Д.В. Алгоритм редукции при верификации объектов в распределенных системах. В кн. Материалы 15 Международного симпозиума " Логическое управление. Интеллектуальные информационные технологии и стратегии. Москва, Международная академия информатизации, 1992г., с. 209 - 211

3. Гусева А.И., Кольцов Д.В. Распределенные системы: декомпозиция и синтез. В кн. Материалы 17 Международного симпозиума " Логическое управление. Интеллектуальные информационные технологии и стратегии. 'V Москва, Международная академия информатизации, 1994г., с. 75 - 80