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

Российская Академия Наук Институт Системного Программирования

УДК 519.683

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

Пакулин Николай Витальевич

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

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

Автореферат

диссертации на соискание ученой степени кандидата физико-математических наук

Москва, 2006

Работа выполнена в Институте системного программирования РАН.

Научный руководитель: доктор физико-математических наук

Петренко Александр Константинович

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

Позин Борис Аронович

кандидат физико-математических наук, Соколов Валерий Анатольевич

Ведущая организация: Факультет Вычислительной математики

и кибернетики

Московского Государственного Университета им. М.В. Ломоносова

Защита диссертации состоится «08» _сентября_ 2006 г. в _15_ часов на заседании диссертационного совета Д.002,087.01 при Институте системного программирования РАН по адресу:

109004, Москва, Б. Коммунистическая 25, Институт системного программирования РАН, конференц-зал.

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

Автореферат разослан «28» _июля _ 2006 г.

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

/Прохоров С.П./

Общая характеристика работы

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

Тестирование соответствия стандартам Интернета является одним из основных средств обеспечения совместимости реализаций протоколов Интернета. Подходы к тестированию реализаций этих протоколов, использующиеся на практике, основаны на ручной разработке тестовых наборов, состоящих из отдельных элементарных испытаний (test cases). Элементарные испытания представляют собой программы на специализированных языках спецификации тестов, таких как TTCN-2 и TTCN-3, или на обычных языках программирования — Perl, Java, Си. В каждом элементарном испытании реализуется последовательность тестовых воздействий на целевую систему и вынесение вердикта о корректности наблюдаемого поведения целевой системы. Для каждого элементарного испытания явно или неявно задаётся цель тестирования (test purpose), которая неформально определяет группу функциональных требований к реализации протокола. Успешное или неуспешное завершение элементарного испытания трактуется следующим образом: реализация протокола корректно или некорректно реализует требования, соответствующие цели тестирования.

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

• Высокая трудоёмкость разработки из-за низкого уровня автоматизации разработки тестовых наборов.

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

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

• Элементарные испытания, как правило, реализуют только ограниченное число сценариев для проверки соответствующей цели тестирования. Нет подхода, который позволяет существенно повысить «глубину» тестирования и обеспечить всестороннюю проверку требований цели тестирования.

В последнее десятилетие определённый прогресс в решении указанных проблем достигнут в исследованиях в области тестирования с использованием моделей (model-based testing). Центральная идея этого направления заключается в том, что в процесс разработки тестовых наборов включаются формальные модели (спецификации) целевой системы и тестов, которые используются для автоматической генерации тестовых последовательностей, автоматической проверки корректности поведения реализации, оценки полноты тестирования и т.д.

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

До последнего времени в исследованиях по формализации протоколов и их тестированию незаслуженно мало внимания уделялось контрактным спецификациям, которые развивают известный метод проектирования программ Design-by-Contract (Проектирование на основе контрактов), разработанный Б.Майером. По сути контрактные спецификации являются продолжением идей Т.Хора о спецификации при помощи пред- и постусловий. При описании внешне наблюдаемого поведения системы контрактными спецификациями взаимодействие системы с окружением представляется как набор операций в некотором формальном интерфейсе. С

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

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

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

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

1. Разработать метод формализации стандартов протоколов, функционирующих в стеке протоколов Интернета.

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

3. Провести апробацию и оценку эффективности предложенных методов на наборе протоколов Интернета, составляющих сетевой и транспортный уровни стека протоколов 1Р\'6.

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

Практическая значимость работы. Разработанные методы спецификации протоколов Интернета и тестирования их соответствия требованиям стандартов расширяют область использования контрактных спецификаций на сложные сетевые протоколы с ограниченным временем реакции на внешние воздействия. С использованием разработанных методов и пакета программ CTesK, реализующего технологию автоматизированного тестирования UniTESK для программного обеспечения на языке Си, были проведены исследовательские проекты по грантам Microsoft Research, РФФИ, Президиума РАН по тестированию реализаций современных сетевых протоколов. Были разработаны тестовые наборы для тестирования соответствия следующим базовым стандартам протоколов сетевого и транспортного уровней стека Интернет-протокола нового поколения IPv6:

• протокол IPv6, базовые функции оконечного узла (IETF RFC 2460, 2461, 2462, 2463,2464,2710, 3513);

• протокол ГОР в сетях IPv6 (IETF RFC 768,2460);

• протоколы динамической смены подключения к сетям IPv6, Mobile IPv6 (IETF RFC 3775);

• протоколы безопасности сетевого уровня IPsec (IETF RFC 1851, 2401, 2402,2403,2404,2405, 2406,2410);

• программный интерфейс стека протоколов (IETF RFC 2292, 2553). Эти проекты показали результативность и приемлемую сложность

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

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

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

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

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

Апробация работы н публикации. Результаты работы докладывались на международных конференциях «Интернет нового поколения» (Ярославль, 2002 г., там же, 2003 г., Москва, 2004 г.), Всероссийской научной конференции «Научный сервис в сети Интернет» (Новороссийск, 2003 г., 2004 г., 2005 г.), пятой международной конференции «Перспективы систем информатики» (Новосибирск, 2003 г.), на втором Международном симпозиуме по обеспечению готовности сервисов ISAS (Берлин, Германия, 2005 г.), девятой всемирной конференции по системике, кибернетике и информатике WMSCI2005 (Орландо, США, 2005), на рабочем совещании Европейского проекта G04IT (Sophia Antipolis, Франция, 2005 г.), на семинаре по теоретической информатике Ярославского Государственного Университета (Ярославль, 2006 г.).

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

Структура и объем работы. Диссертация состоит из введения, четырёх глав, заключения, списка литературы и четырёх приложений. Список литературы включает 126 названий. Основной текст диссертации (без приложений) занимает 130 страниц.

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

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

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

тестовый набор состоит из абстрактных элементарных испытаний (abstract test cases); которые записаны в нотации, не зависящей от конкретной реализации. В заключении параграфа отмечаются недостатки этой методологии, существенные для тестирования реализаций протоколов Интернета.

В параграфе 1,3 рассмотрены традиционные для телекоммуникационных приложений методы формального описания протоколов и основанные на них подходы к автоматизированной генерации тестовых последовательностей. Современные нотации, которые используются для описания поведения протоколов, представляют протоколы как взаимодействующие расширенные конечные автоматы (нотация SDL) или как взаимодействующие процессы (нотация LOTOS). Представлены несколько наиболее известных подходов к тестированию соответствия таким спецификациям протоколов - инструменты TGV, TCBeans-Gotcha/AGEDIS, ТогХ, работы У.Уяра (Uyar), - обсуждаются ограничения этих подходов, препятствующие их использованию для тестирования реализаций протоколов Интернета.

В параграфе 1.4 содержится введение в протоколы Интернета, проанализированы характерные особенности протоколов, принадлежащих стеку Интернет-протокола нового поколения IPv6. В таблице 1 приведены основные характеристики базовых протоколов стека IPv6. Из таблицы видно, что протоколы в стеке IPv6 обладают следующими особенностями: (1) большой размер сообщений (сотни бит), сложная структура сообщений, включающих списки и поля переменного размера; (2) сложное устройство состояния протоколов — наличие в состоянии таблиц, множеств, кэшей, буферов; (3) недетерминизм данных — поля сообщений протоколов содержат случайные или трудно предсказуемые значения, недетерминизм времени -случайные задержки времени перед отправкой сообщений; (4) спецификации протоколов содержат необязательные и недоопределённые функции.

Таблица 1. Характеристики базовых протоколов стека 1Ру6

Функционирует в стеке Есть программный интерфейс Свойства сообщений Свойства состояния Недетерминизм Содержит необязательные функции 1 а> ! il ч S Размер спецификации, страницы

Переносит данные других Мин. размер заголовка, бит Маке, размер заголовка, бит Содержит списки Содержит поля переменного Размер состояния Содержит кэши Включает буферизацию Содержит таблицы Содержит множества Содержит таймеры Данные 1 а m

IPv6 + С + 320 320 + + * — + — — — + — + + 39

Передача IPv6 в Ethernet + — + 116 116 7

UDP + С + 64 62 — — — — Р/3 — + — — — — + 3

TCP + с + 192 480 + + # — + + + + + + + 84

lCMPvô + H + 64 64 + + 18

Neighbor Discovery + — - 128 2" + + # + — + + + + + + + 93

Address Autoconf. + — — 128 2" + — N•192 + — — + + — — + + 20

DAD + ■ — — 192 224 — — — — — — — + — + + + 5

MLD + H 192 192 — — N•160 — — — + + — + + + 22

MIPv6 + H — 64 576 + + . # + — + + + + + + 165

IPsec + сд + 48 2" + + № — + + + + , — + + 110

IKE + H — 2" + + # — — + + — + — + + 182

С - есть стандартизованный программный интерфейс; Н - программный интерфейс предполагается, но не стандартизован,Р/3 - зависит от реализации. >1*М означает, что состояние включает N объектов, размер каждого М бит; # - размер состояния зависит от многих параметров

В главе 2 рассматривается разработанный метод формального описания функционирования сетевых протоколов посредством контрактных спецификаций. В параграфе 2.1 приведено краткое введение в контрактные спецификации. Контрактная спецификация М = (S,F,Inv) состоит из

модельного состояния S, формального интерфейса F, и инварианта Inv. Модельное состояние представляет собой набор переменных, £ = 7] х Г2 х • • • х Г„, где Ti - тип (множество значений) переменной с

номером i. На множестве состояний задан одноместный предикат Inv, который ограничивает множество допустимых состояний модели, выражаемой контрактной спецификацией, = {i eS|//jv(.s)}. Формальный

интерфейс F - {fiсодержит конечный набор элементов формального

интерфейса. Каждый элемент формального интерфейса представляет собой пятёрку ft = (ln,,Outi,prel,posti,Ci). Множества /я,- и ОиЦ определяют

сигнатуру элемента формального интерфейса, Int задаёт пространство входных значений элемента^: /я, =Tt' х• • • х7"/, где Tj есть тип (множество

значений) j-того входного параметра. Outt аналогично определяет пространство выходных значений элемента формального интерфейса: Outi = Т[у.---хТ'',, где T'j есть тип (множество значений)/-того выходного

параметра. Если у элемента формального интерфейса нет входных или выходных параметров, то /я, или Outf соответственно равны выделенному множеству Void, состоящему из единственного элемента и не пересекающегося ни с одним из типов, входящих в сигнатуры элементов формального интерфейса или модельное состояние. Двухместный предикат pret с /и, х S, является предусловием и определяет допустимость вектора in

входных значений элемента формального интерфейса / в состоянии s, что выражается формулой prej{in,s). Четырёхместный предикат post, с. 1п1 х SI х Outi х S, является постусловием; он определяет допустимость вектора выходных значений out элемента формального интерфейса и конечного состояния s' после приёма вектора in входных значений в состоянии у, что выражается формулой post ¡(in, s, out, s'). С,- есть конечное множество критериев покрытия С, - {eqtJ , где каждый элемент eq,j является отношением эквивалентности на множестве 1щ х Sl. Классы эквивалентности по отношениям eq,j называются элементами покрытия элемента формального интерфейса /¡. К отношениям эквивалентности eqj

предъявляется требование, чтобы каждое отношение задавало конечное число классов эквивалентности.

В параграфе 2.2 разработан метод построения контрактной спецификации М = по текстовым спецификациям протоколов

Интернета. Метод заключается в том, что функциональные требования к реализациям протоколов представляются как логические формулы, составляющие постусловия элементов формального интерфейса контрактной спецификации, состоящего из операций обработки входящих и отправки исходящих сообщений протоколов. Разработка контрактной спецификаций разбита на этапы, которые подробно рассматриваются в последующих параграфах 2.3-2.8. На первых двух этапах проводится анализ стандартов Интернета, составление каталога функциональных требований к реализациям протоколов (2.3), анализ полноты набора извлечённых требований (2.4). Собственно контрактная спецификация разрабатывается на последующих этапах: определения состава формального интерфейса протокола (2.5), разработки пред- и постусловий (2.6), задания структуры покрытия контрактной спецификации (2.7). На заключительном этапе разрабатываются введённые в данной работе функции реконструкции состояния (2.8), которые позволяют упростить тестирование недетерминированных и недоопределённых протоколов.

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

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

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

Этапы метода формализации стандартов Интернета, представленные в параграфах 2.3 и 2.4 являются подготовительными - разработчики формальных спецификаций изучают регламентирующие документы, выделяют и анализируют функциональные требования к реализации протокола. Этапы разработки собственно контрактной спецификации рассмотрены в параграфах 2.5-2.7. В параграфе 2.5 описан новый метод составления формального интерфейса, отличающийся тем, что в его состав вводятся элементы, соответствующие получению и отправке сообщений протокола. Разработан метод задания сигнатур элементов формального интерфейса на основании набора параметров сообщения. В параграфе 2.6 рассмотрены вопросы представления функциональных требований в постусловиях и инвариантах состояния. Разработаны методики формализации различных категорий требований, основанных на

классификации требований, введённой в параграфе 2.3. В частности, предложена методика аннотирования утверждений постусловия ссылками на функциональные требования из каталога требований. В параграфе 2.7 введено представление критериев покрытия элемента формального интерфейса как функций, принимающих вектор значений входных параметров этого элемента и возвращающих идентификатор класса эквивалентности. В параграфе 2.8 введено понятие функции реконструкции состояния R для элемента формального интерфейса f с сигнатурой (in,Out): R-.InxS/X. Out p(S), где p(S) обозначает множество конечных

подмножеств множества S. Результат вызова функции реконструкции состояния R(in,s,out) есть множество состояний, в которые может перейти

реализация, вернув вектор значений выходных параметров out в ответ на вектор входных параметров in в состоянии s. Функции реконструкции состояния используются при тестировании «чёрным ящиком», когда у тестовой системы нет доступа к состоянию реализации. Введение функций реконструкции состояний призвано упростить тестирование реализаций недетерминированных и недоопределённых протоколов.

В главе 3 рассматривается разработанный метод задания тестов для проверки соответствия реализаций протоколов Интернета контрактным спецификациям этих протоколов. В этом методе тест рассматривается как конечный автомат t = (S,, sl0,1,, {pass, fail], T,}, где S, - конечное множество

состояний автомата, s,o - начальное состояние, I, — алфавит входных символов автомата, которые в контексте тестирования служат для обозначения обобщённых тестовых воздействий, {pass, fail} — множество

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

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

Важная особенность разработанного метода тестирования заключается в том, что автомат теста для контрактной спецификации = задаётся в особой форме как пятёрка (,?м0,Здесь

$м> — начальное состояние модели, Е, — отношение эквивалентности на множестве 57 допустимых состояний контрактной спецификации, I, -множество обобщённых тестовых воздействий, г, — итератор тестовых воздействий - функция, которая для заданного состояния тестового сценария строит конечный список тестовых воздействий, 1Т : —> I* (здесь 7/ обозначает множество непустых конечных списков из элементов множества /,), А, — конструктор конкретных тестовых воздействий, который по обобщённому тестовому воздействию строит последовательность конкретных тестовых воздействий как список обращений к элементам формального интерфейса с определёнными значениями входных параметров. Результат вызова функции А, для обобщённого тестового воздействия ае1, в модельном состоянии я е 51 есть список конечной длины А,,(я,а) = ((£,,/„щ,оы/;)|5, ей,/, еГ,щ е/,,1п,оЫ1 е/,.Ош), где I -номер конкретного тестового воздействия в последовательности, <5, -задержка перед выдачей /-го конкретного воздействия, и т-, — конкретное тестовое воздействие, заданное как вызов элемента формального интерфейса / с вектором значений входных значений ш„ оиЬ — зарегистрированный ответ тестируемой реализации (/¡.1п и /¡.Ош используются для обозначения пространств входных и выходных значений элемента/; соответственно).

Параллельно с выдачей воздействий тестовая система регистрирует наблюдаемое поведение системы, например, исходящие сообщения протокола или обратные вызовы программного интерфейса, как частично упорядоченное множество вызовов элементов формального интерфейса <9 = {(1,(!Г,,/),ш,.,он^)}, где / - порядковый номер регистрации события, 8, -отметка времени регистрации события, /, <= /¡1п,оШ1 е /¡.Ом -

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

порядок -< определяет предшествование зарегастрированных событий: е, -<е2 означает, что событие в\ гарантированно произошло до события ег.

Несравнимость событий в\ и е2 означает, что взаимный порядок событий неизвестен.

Конечное состояние перехода и вердикт вычисляются следующим образом. Из дизъюнктивного объединения множества конкретных тестовых воздействий At[s,a) и зарегистрированных реакций О целевой системы строится изоморфное ему полностью упорядоченное множество событий Е = {(у,/у,irtj,outj) , такое, что порядок на Е удовлетворяет частичному

порядку на О и полному порядку A£s,a), и существует такая последовательность модельных состояний s0=s,st.....s„, что

V/ е 1, п fj .preiirij ,s) л s; е fj , Sj_x, outj^fj.postimj^j^outj,*;),

где fj.pre,fjA,fj.post означают предусловие, функцию реконструкции

состояния и постусловие элемента формального интерфейса fj соответственно. Если такая последовательность существует, то переход автомата теста из состояния [г]1 по обобщённому тестовому воздействию a el, завершается в состоянии [s„ ] и сопровождается выдачей символа pass. При этом покрытие спецификации, достигнутое на переходе, есть

и и

j=leqefj.C

где fj.C обозначает множество критериев покрытия fj, а [[ш^,sj обозначает класс эквивалентности пары [irij, j по отношению eq, то есть

элемент покрытия элемента формального интерфейсаf. В случае, если такая последовательность не найдена, то переход завершается в состоянии [s] и выдаётся символ fail.

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

Такое задание автомата теста называется неизбыточным, так как в задании автомата теста не указывается явно конечные состояния и выходные

1 Класс эквивалентности модельного состояния s по отношению эквивалентности Е,

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

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

В параграфах 3.2-3.7 представлены этапы метода разработки тестов для протоколов Интернета в виде неизбыточно заданных автоматов. В параграфе 3.2 рассматривается новый метод задания целей тестирования, заключающийся в том, что цель тестирования представляется как множество элементов покрытия, которые должны ■ принадлежать покрытию спецификации, достигнутого тестом. Такое формальное задание целей тестирования позволяет автоматизировать проверку достижения целей тестирования тестами и обеспечить корректность декомпозиции протокола: объединение целей тестирования всех тестов для протокола, чьи сообщения и программный интерфейс в контрактной спецификации М = (5,/г,/«у) моделируются множеством элементов формального интерфейса Р сР,

должно покрывать всю спецификацию протокола, то есть совпадать с множеством сол/(ед), где соу(ед) означает множество классов

У^, «7 «/с

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

В параграфе 3.3 приведено научное обоснование методики составления множества обобщённых тестовых воздействий и состояний

автоматов тестирования, то есть отношений факторизации модельных состояний. В параграфах 3.4 и 3.5 рассматриваются вопросы, связанные с разработкой алфавита тестовых воздействий и отношения эквивалентности модельных состояний. Для часто встречающихся целей тестирования протоколов Интернета, выделенных в параграфе 3.2, разработаны обобщённые тестовые воздействия, отношения эквивалентности и конструкторы конкретных тестовых воздействий. Сформулированы и доказаны теоремы о корректности разработанных неизбыточных заданий автоматов тестов для типичных функций протоколов Интернета.

В параграфах 3.6 и 3.7 рассмотрены практические вопросы реализации тестов: параметризация контрактной спецификации и автоматов тестов, передача значений параметров при прогоне тестов (параграф 3.6) и отладка тестов (параграф 3.7).

В главе 4 рассматривается опыт практического применения разработанных в диссертации методов. В параграфе 4.1 перечислены проекты по тестированию сетевых протоколов, проведённых с использованием разработанных в данной диссертации методов. В параграфе 4.2 представлен тестовый набор для тестирования соответствия базовым функциям стека протоколов IPv6, который применялся при тестировании реализации IPv6 от Microsoft Research. Рассмотрены вопросы состава формального интерфейса, формализации различных функций протоколов, недетерминированного поведения.

В параграфе 4.3 приведены результаты сравнения тестовых наборов, разработанных в ИСП РАН с использованием представленных в диссертации методов, с известными тестовыми наборами IPv6 — тестовым набором ТАШ2, старейшим и наиболее разработанным тестовым набором для IPv6, и тестовым набором для IPv6, развиваемом в ETSI3, который разрабатывается средствами языка TTNC-3, наиболее современной на настоящий момент реализацией подхода элементарных тестов. В таблице 2 приведены данные для двух тестовых наборов, разработанных автором в ИСП РАН: для

2 Проект по разработке тестового набора для IPv6 TAHI. [HTTP] http://www.tahi.org/.

3 European Telecommunications Standards Institute. Methods for Testing and Specification (MTS); Internet Protocol Testing (IPT); IPv6 Testing: Methodology and Framework. ETSI TS 102 351, August 2005.

реализации IPv6 от Microsoft Research (MSR IPv6) и расширенный тестовый набор для реализации IPv6 для Windows XP/Windows СЕ (MS Mobile IPv6).

Таблица 2. Сравнительные характеристики тестовых наборов для IPv6

Название тестового набора Спецификация протокола, в тысячах строк ^ Спецификация тестов, J в тысячах строк Медиаторы и вспомогательные подсистемы, в тысячах строк Число тестовых испытаний Затраты на одно тестовое испытание, без учёта медиаторов, строки4 Затраты на одно тестовое испытание, с учётом медиаторов, строки Доля повторно используемых компонентов тестового набора

TAHI - 116 22 750 157 188 16%

ETSI - 22 5 400 55 - 50%

ИСП РАН для MSR IPv6 8,5 2,5 6 500 22 34 80%

ИСП РАН для MS Mobile IPv6 12 4,5 9 700 23 35 80%

Данные, приведённые в таблице 2 показывают, что использование методов, разработанных в данной диссертации, позволяет сократить в 2-5 раз затраты на разработку тестов и в 1,5-5 раз повысить в тестовом наборе долю повторно используемых компонентов. Кроме того, необходимо отметить, что с использованием тестового набора для MSR IPv6 в реализации были обнаружены 4 дефекта и 2 критические ошибки, приводящие к перезагрузке операционной системы, не выявленные при тестировании другими тестовыми наборами.

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

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

5 тестовый набор ETSI использует адаптеры, кодеры и декодеры, разработанные компанией Testing Tech, информация об их размерах отсутствует.

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

Основные выводы и результаты

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

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

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

3. Разработаны неизбыточные задания автоматов тестов для типичных задач тестирования, которые встречаются при тестировании протоколов

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

4. С использованием представленных в диссертации методов разработан пакет прикладных программ - тестовый набор — для тестирования соответствия реализаций стека протоколов IPvö набору базовых стандартов IPv6.

5. Проведенное в работе сравнение эффективности разработанного пакета прикладных программ с известными реализациями показало, что:

• Использование разработанных методов позволяет сократить объём тестового набора 2—5 раз по сравнению с созданием тестовых наборов из элементарных испытаний.

• Доля повторно используемых компонентов составляет 80% тестового набора, что в 1,5—5 раз превосходит аналогичный показатель тестовых наборов TAHI и ETSI.

• Разработанные тестовые наборы демонстрируют большую «глубину» . тестирования, чем тестовые наборы, составленные из элементарных

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

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

Публикации

По теме диссертации опубликованы следующие работы:

1. АгамирзянИ., Грошев С.Г., Хорошилов A.B., Ключников Г.В., Косачев A.C., Омельченко В.А., Пакулин Н.В., Петренко А.К., Шнитман В.З. Применение формальных методов для тестирования MSR IPv6. // Интернет нового поколения. Сборник тезисов международной конференции. Ярославль, 2002. С. 29-33.

2. Ключников Г.В., КосачевА.С., Пакулин Н.В., Петренко Л.К., Шнитман В.З. Применение формальных методов для тестирования Mobile IPv6. // Интернет нового поколения. Сборник тезисов II международной конференции. Ярославль, 2003. С. 20-25.

3. Ключников Г.В., КосачевА.К., Пакулин Н.В., Петренко А.К., Шнитман В.З. Применение формальных методов для тестирования реализации IPv6. // Труды ИСП РАН, Том 4. М., 2003. С. 121-140.

4. Косачев А.С., Пакулин Н.В., Петренко А.К., Шнитман В.З. Формализация требований Интернет-стандартов для тестирования реализаций коммуникационных протоколов. П Научный сервис в сети Интернет. Труды Всероссийской научной конференции. М.: Изд-во МГУ, 2003. С. 318-321.

5. Victor V. Kuliamin, Alexander К. Petrenko, Nick V. Pakoulin, Alexander S. Kossatchev, Igor B. Bourdonov. Integration of Functional and Timed Testing of Real-time and Concurrent Systems. // Perspectives of System Informatics. Proceedings of Andrei Ershov Fifth International Conference. LNCS 2980. Springer-Verlag, 2003. P. 450-462.

6. Пакулин H.B. Формальная спецификация IPsec. // Интернет нового поколения. Сборник тезисов III международной конференции. М., 2004. С. 14-23.

7. Nickolay Pakoulin, Vitaly Omelchenko, Alexander Koptelov, Alexander Petrenko, Alexander Kossatchev, Chunyen Cheng. MPEG-2 IPMP Conformance Test Suite Development. AVS Ml 263, 2004. [PDF] (http://www.avs.org.cn/FileList.asp?meetingid=15&filetype=proposal)

8. V. Kuliamin, A. Petrenko, N. Pakoulin. Practical Approach to Specification and Conformance Testing of Distributed Network Applications. // M. Malek, E. Nett, N. Suri, eds. Service Availability. Proc. of 2-nd ISAS 2005. LNCS 3694. Springer-Verlag, 2005. P. 68-83.

9. V. Kuliamin, A. Petrenko, N. Pakoulin. Extended Design-by-Contract Approach to Specification and Conformance Testing of Distributed Software. // Model Based Development and Testing, v. VII. Proc. of 9-th WMSCI, Orlando, USA, 2005. P. 65-70.

Ю.Ключников Г.В., Пакулин Н.В., Шнитман В.З. Автоматизированное тестирование сетевых сервисов Интернет-протокола. // Научный сервис в сети ИНТЕРНЕТ. Труды Всероссийской научной конференции, М.: Изд-во МГУ, 2005. С. 168-170.

11.В. В.Кулямин, Н. В. Пакулин, О.Л.Петренко, А. А. Сортов, А. В. Хорошилов. Формализация требований на практике. Препринт. М.: ИСП РАН, 2006. 50 с.

12.Пакулин Н.В., Хорошилов A.B. Разработка формальных моделей и тестирование соответствия для систем с асинхронными интерфейсами и телекоммуникационных протоколов. II Программирование. 2006. В печати.

Напечатано с готового оригинал-макета

Издательство ООО "МАКС Пресс" Лицензия ИД N 00510 от 01.12.99 г. Подписано к печати 28.07.2006 г. Формат 60x90 1/16. Усл.печ.л. 1,25. Тираж 100 экз. Заказ 571.

119992, ГСП-2, Москва, Ленинские горы, МГУ им. М.В. Ломоносова, 2-й учебный корпус, 627 к. Тел. 939-3890,939-3891. Тел./факс 939-3891.

Введение.

Глава 1. Анализ современного состояния методов формализации в тестировании телекоммуникационных протоколов.

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

1.2 Методы формальной спецификации тестов.

1.3 Методы формального описания протоколов и автоматической генерации тестовых последовательностей.

1.4 Введение в протоколы Интернета.

1.5 Постановка задачи.

Глава 2. Метод формализации стандартов протоколов Интернета.

2.1 Введение в контрактные спецификации.

2.2 Описание разработанного метода формализации стандартов протоколов Интернета.

2.3 Анализ спецификации протокола и извлечение требований.

2.4 Разработка и анализ концептуальной модели требований.

2.5 Определение формального интерфейса протокола.

2.6 Разработка пред- и постусловий для формального интерфейса протокола Интернета.

2.7 Разработка критериев покрытия.

2.8 Разработка функций реконструкции состояния.

Выводы по главе 2.

Глава 3. Метод формального задания тестов для тестирования соответствия контрактным спецификациям протоколов Интернета.

3.1 Тестирование соответствия контрактным спецификациям.

3.2 Обзор разработанного метода формального задания тестов.

3.3 Определение целей тестирования.

3.4 Разработка проекта тестового сценария.

3.5 Разработка итераторов тестовых воздействий и конструкторов конкретных тестовых воздействий.

3.6 Разработка функции определения текущего состояния сценария.

3.7 Разработка настроек тестового сценария.

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

Выводы по главе 3.

Глава 4. Практические применения.

4.1 Проекты по тестированию IPv6 в ИСП РАН.

4.2 Тестирование MSR IPv6.

4.3 Сравнение с другими тестовыми наборами для IPv6.

4.4 Применение разработанных методов к другим видам систем.

Выводы по главе 4.

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

Тестирование соответствия стандартам Интернета является одним из основных средств обеспечения совместимости реализаций протоколов Интернета. Подходы к тестированию реализаций этих протоколов, использующиеся на практике, основаны на ручной разработке тестовых наборов, состоящих из отдельных элементарных испытаний (test cases). Элементарные испытания представляют собой программы на специализированных языках спецификации тестов, таких как TTCN-2[54] и TTCN-3[55], или на обычных языках программирования - Perl, Java, Си. В каждом элементарном испытании реализуется последовательность тестовых воздействий на целевую систему и вынесение вердикта о корректности наблюдаемого поведения целевой системы. Для каждого элементарного испытания явно или неявно задаётся цель тестирования (test purpose)[38], которая неформально определяет группу функциональных требований к реализации протокола. Успешное или неуспешное завершение элементарного испытания трактуется следующим образом: реализация протокола корректно или некорректно реализует требования, соответствующие цели тестирования.

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

1. Высокая трудоёмкость разработки из-за низкого уровня автоматизации разработки тестовых наборов.

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

3. Нет формально заданной меры определения полноты тестирования и достоверной процедуры оценки полноты тестирования.

4. Элементарные испытания, как правило, реализуют только ограниченное число сценариев для проверки соответствующей цели тестирования. Нет подхода, который позволяет существенно повысить «глубину» тестирования и обеспечить всестороннюю проверку требований цели тестирования.

В последнее десятилетие определённый прогресс в решении указанных проблем достигнут в исследованиях в области тестирования с использованием моделей (model-based testing). Центральная идея этого направления заключается в том, что в процесс разработки тестовых наборов включаются формальные модели (спецификации) целевой системы и тестов, которые используются для автоматической генерации тестовых последовательностей, автоматической проверки корректности поведения реализации, оценки полноты тестирования и т.д.

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

До последнего времени в исследованиях по формализации протоколов и их тестированию незаслуженно мало внимания уделялось контрактным спецификациям, которые развивают известный метод проектирования программ Design-by-Contract (Проектирование на основе контрактов), разработанный Б.Майером.[120] По сути контрактные спецификации являются продолжением идей Т.Хора[121] о спецификации при помощи пред- и постусловий. При описании внешне наблюдаемого поведения системы контрактными спецификациями взаимодействие системы с окружением представляется как набор операций в некотором формальном интерфейсе. С каждой операцией формального интерфейса связаны предусловие и постусловие. Предусловие операции накладывает ограничения на ситуации, в которых эта операция может быть вызвана, постусловие операции накладывает ограничение на результаты операции и изменение состояния системы после выполнения операции.

Контрактные спецификации успешно использовались в проектах индустриального масштаба по тестированию программных интерфейсов компонентов ядра операционной системы [122,123]. Представляется перспективным расширить подход контрактных спецификаций на сетевые протоколы и применить их для формализации стандартов протоколов Интернета и разработать метод тестирования реализаций протоколов Интернета на основе формальных спецификаций протоколов.

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

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

• Разработать метод формализации стандартов протоколов, функционирующих в стеке протоколов Интернета.

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

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

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

Практическая значимость работы. Разработанные методы спецификации протоколов Интернета и тестирования их соответствия требованиям стандартов расширяют область использования контрактных спецификаций на сложные сетевые протоколы с ограниченным временем реакции на внешние воздействия. С использованием разработанных методов и пакета программ CTesK[100], реализующего технологию автоматизированного тестирования UniTESK[124] для программного обеспечения на языке Си, были проведены исследовательские проекты по грантам Microsoft Research, РФФИ, Президиума РАН по тестированию реализаций современных сетевых протоколов. Были разработаны тестовые наборы для тестирования соответствия следующим базовым стандартам протоколов сетевого и транспортного уровней стека Интернет-протокола нового поколения IPv6:

• протокол IPv6, базовые функции оконечного узла (IETF RFC 2460, 2461,2462,2463, 2464,2710,3513)[74,78,79,77,116,91,125];

• протокол UDP в сетях IPv6 (IETF RFC 768,2460)[76,74]

• протоколы динамической смены подключения к сетям IPv6, Mobile IPv6 (IETF RFC 3775)[99];

• протоколы безопасности сетевого уровня IPsec (IETF RFC 1851, 2401,2402,2403,2404,2405,2406,2410)[80-87];

• программный интерфейс стека протоколов (IETF RFC 2292, 2553)[97,98].

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

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

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

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

Апробация работы и публикации. Результаты работы докладывались на международных конференциях «Интернет нового поколения» (Ярославль, 2002 г., там же, 2003 г., Москва, 2004 г.), Всероссийской научной конференции «Научный сервис в сети Интернет» (Новороссийск, 2003 г., 2004 г., 2005 г.), пятой международной конференции «Перспективы систем информатики» (Новосибирск, 2003 г.), на втором Международном симпозиуме по обеспечению готовности сервисов ISAS (Берлин, Германия, 2005 г.), девятой всемирной конференции по системике, кибернетике и информатике WMSCI2005 (Орландо, США, 2005), на рабочем совещании Европейского проекта G04IT (Sophia Antipolis, Франция, 2005 г.), на семинаре по теоретической информатике Ярославского Государственного Университета (Ярославль, 2006 г.).

По теме диссертации опубликованы 12 работ [1-12], раскрывающих все основные научные результаты диссертации.

Структура и объем работы. Диссертация состоит из введения, четырёх глав, заключения, списка литературы и четырёх приложений. Список литературы включает 126 названий. Основной текст диссертации (без приложений и списка литературы) занимает 130 страниц.

Выводы по главе 4

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

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

1. Использование разработанных методов позволяет сократить объём тестового набора 2—5 раз по сравнению с созданием тестовых наборов из элементарных испытаний.

2. Доля повторно используемых компонентов составляет 80% тестового набора, что в 1,5—5 раз превосходит аналогичный показатель тестовых наборов TAHI и ETSI.

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

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

Заключение

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

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

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

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

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

5. Проведенное в работе сравнение эффективности разработанного пакета прикладных программ с известными реализациями показало, что:

• Использование разработанных методов позволяет сократить объём тестового набора 2—5 раз по сравнению с созданием тестовых наборов из элементарных испытаний.

• Доля повторно используемых компонентов составляет 80% тестового набора, что в 1,5—5 раз превосходит аналогичный показатель тестовых наборов TAHI и ETSI.

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

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

1. Агамирзян И., Грошев С.Г., Хорошилов А.В., Ключников Г.В., Косачев

2. A.С., Омельченко В.А., Пакулин Н.В., Петренко А.К., Шнитман В.З. Применение формальных методов для тестирования MSR IPv6. // Интернет нового поколения. Сборник тезисов международной конференции. Ярославль, 2002. С. 29-33.

3. Ключников Г.В., Косачев А.С., Пакулин Н.В., Петренко А.К., Шнитман

4. B.З. Применение формальных методов для тестирования Mobile IPv6. // Интернет нового поколения. Сборник тезисов II международной конференции. Ярославль, 2003. С. 20-25.

5. Ключников Г.В., Косачев А.К., Пакулин Н.В., Петренко А.К., Шнитман В.З. Применение формальных методов для тестирования реализации IPv6. // Труды ИСП РАН, Том 4. М., 2003. С. 121-140.

6. Пакулин H.B. Формальная спецификация IPsec. // Интернет нового поколения. Сборник тезисов III международной конференции. М., 2004. С. 14-23.

7. Nickolay Pakoulin, Vitaly Omelchenko, Alexander Koptelov, Alexander Petrenko, Alexander Kossatchev, Chunyen Cheng. MPEG-2 IPMP Conformance Test Suite Development. AVS M1263, 2004. PDF. (http://www.avs.org.cn/FileList.asp?meetingid=15&filetype=proposal)

8. V. Kuliamin, A. Petrenko, N. Pakoulin. Extended Design-by-Contract Approach to Specification and Conformance Testing of Distributed Software. // Model Based Development and Testing, v. VII. Proc. of 9-th WMSCI, Orlando, USA, 2005. P. 65-70.

9. Ю.Ключников Г.В., Пакулин H.B., Шнитман В.З. Автоматизированное тестирование сетевых сервисов Интернет-протокола. // Научный сервис в сети ИНТЕРНЕТ. Труды Всероссийской научной конференции, М.: Изд-во МГУ, 2005. С. 168-170.

10. В. В. Кулямин, Н. В. Пакулин, О. JI. Петренко, А. А. Сортов, А. В. Хороши лов. Формализация требований на практике. Препринт. М.: ИСП РАН, 2006. 50 с.

11. Пакулин Н.В., Хорошилов А.В. Разработка формальных моделей и тестирование соответствия для систем с асинхронными интерфейсами и телекоммуникационных протоколов. // Программирование. 2006. В печати.

12. F. С. Hennie. Fault detecting experiments for sequential circuits. // Proc. 5th Ann. Symp. Switching Circuit Theory and Logical Design, 1964. C. 95110,.

13. M. П. Василевский. Диагностика ошибок в автоматах. // Кибернетика и системный анализ, т. 9, № 4, 1973. С. 98-108.

14. Т. S. Chow. Testing software design modeled by finite-state machines. // IEEE Trans, on Software Engineering, vol. 4, no. 3,1978. C. 178-187.

15. J. A. Bergstra, J. W. Klop. Algebra of Communicating Processes with Absraction. Theoretical Computer Science, 37(1), 1985. C. 77-121.

16. C. A. R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985; электронное издание, 2004. 260 с. PDF. (http://www.usingcsp.com/cspbook.pdf).

17. R. Milner. Communication and Concurrency. Prentice-Hall, 1989. 260 c.

18. N.A. Lynch, M.R. Tuttle, "An Introduction to Input/Output Automata" // CWI-Quaterly 3, 1989, P. 219-246. PDF. http://www.markrtuttle.com/papers/lt89-cwi.pdf.

19. F. Maraninchi. Operational and compositional semantics of synchronous automaton compositions. // CONCUR'92 Proceedings, LNCS 630. Springer-Verlag, 1992. PS. http://www-verimag.imag.fr/~maraninx/ArgosCONCUR92.ps.gz

20. ISO/IEC 7498. Information technology Open Systems Interconnection -Basic Reference Model. Geneva, Switzerland: ISO, 1994.

21. CCITT Recommendation Z.100. Specification and Description Language (SDL). Geneve, Switzerland: ITU, 1993. 245 c.

22. ISO/IEC 9074. Information Processing Systems — Open Systems Interconnection. Estelle — A Formal Description Technique based on an Extended State Transition Model. Geneve, Switzerland: ISO, 1989 1 я редакция,1997 2-я редакция. Отозван 06.05.1999.

23. ISO/IEC 8807. Information Processing Systems — Open Systems Interconnection. LOTOS — A Formal Description Technique Based on the Temporal Ordering of Observational Behaviour. Geneve, Switzerland: ISO, 1989. 142 c.

24. Е. Brinksma. A theory for the derivation of tests. Proc. IFIP WG6.1 8th Intl. Symp. on Protocol Specification, Testing, and Verification, North-Holland, S. Aggarwal and K. Sabnani Ed. pp. 63-74,1988.

25. К. K. Sabnani and A. T. Dahbura. A protocol test generation procedure. Computer Networks and ISDN Systems, vol. 15, no. 4, pp. 285-297, 1988.

26. S. Fujiwara, G. v. Bochmann, F. Khendek, M. Amalou, and A. Ghedamsi. Test selection based on finite state models. IEEE Trans, on Software Eng., vol. 17, pp. 591-603, 1991.

27. G. Luo, A. Petrenko, and G. v. Bochmann. Selecting test sequences for partially specified nondeterministic finite state machines, Proceedings of the IFIP Seventh International Workshop on Protocol Test Systems, Japan, 1994, pp. 95-110.

28. H. В. Евтушенко, А. В. Лебедев, А. Ф. Петренко. Построение проверяющего множества для компоненты последовательной автоматной сети. Автоматика и телемеханика, № 8. стр. 145-153,1994.

29. J. Tretmans. A Formal Approach to Conformance Testing. PhD thesis, University of Twente, Enschede, The Netherlands, 1992.

30. J. C. Fernandez, C. Jard, T. Jeron, C. Viho. Using on-the-Fly Verification Techniques for the Generation of Test Suites // Proceedings of the 8th International Conference on Computer Aided Verification, LNCS 1102, Springer-Verlag, 1996, P. 348-359.

31. J. Tretmans. Test Generation with Inputs, Outputs, and Repetitive Quiescence. Software — Concepts and Tools, 17(3):103-120,1996.

32. D. P. Sidhu and T.-K. Leung. Formal methods for protocol testing: a detailed study. IEEE Trans. Soft. Eng., vol. 15, no. 4, pp. 413-426,1989.

33. D. Lee, M. Yannakakis. Principles and methods of testing finite state machines — a survey. Proc. IEEE, 84(8): 1090-1123,1996.

34. G. v. Bochmann, A. Petrenko. Protocol Testing: Review of Methods and Relevance for Software Testing. Proc. of ACM SIGSOFT ISSTA'1994, Software Engineering Notes, Special Issue, pp. 109—124.

35. G. Bernot. Testing against Formal Specifications: A Theoretical View. In Proc. of TAPSOFT'91, vol. 2. S. Abramsky and T. S. E. Maibaum, eds. LNCS 494, pp. 99-119, Springer-Verlag, 1991.

36. ISO/IEC 9646. Information technology Open Systems Interconnection - Conformance testing methodology and framework - Part 1: General concepts. Geneva: ISO, 1994. 46 c.

37. ITU-T Recommendation Z.500. Framework on formal methods in conformance testing. Geneve, Switzerland: ITU, 1997. 49 c.

38. S. Sadeghipour, H. Singh. Test strategies on the basis of extended finite state machines, 1998. Report FT3/SM-98-04, Daimler-Benz AG.

39. C. Bourhfir, R. Dssouli, El M. Aboulhamid and N. Rico. Automatic Executable Test Case Generation for Extended Finite State Machine Protocols. IFIP International Workshop on Testing Communicating Systems, IFIP IWTCS'97, Korea, 1997.

40. A. Duale, U. Uyar. Generation of Feasible Test Sequences for EFSM Models. Proc. IFIP Intl. Conf. Testing of Communicating Systems, pp. 91109, Sept. 2000.

41. M. Ben-Ari, A. Pnueli, Z. Manna: The Temporal Logic of Branching Time. // Acta Informatica, Volume 20, Springer Verlag, 1989, pp. 207-226.

42. A. Pnueli. The temporal semantics of concurrent programs. // Theoretical Computer Science, Vol. 13 № 1, Elsevier, 1981, pp. 45-60.

43. E.M. Clarke, E.A. Emerson: Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic. // Logic of Programs, LNCS 131, Springer-Verlag, 1981, pp. 52-71.

44. A. Church. A formulation of the simple theory of types. // J Symbolic Logic, vol.5,1940. C. 56-68.48.muCalc. D. Kozen. Results on the propositional mu-calculus. // Theoretical Computer Science, vol. 27. Netherlands: Elsevier, 1983. C. 333—354.

45. M. Gordon. HOL: A Machine Oriented Formulation of Higher Order Logic. Technical Report 68, University of Cambridge, Computer Laboratory, 1985.

46. S. Owre, J. M. Rushby, N. Shankar. PVS: A Prototype Verification System. // Proc. of 11th Int. Conf. on Automated Deduction (CADE), LNAI 607. Springer-Verlag, 1992. C. 748-752.

47. Кларк Э.М. (мл.), Грамберг О., Пелед Д. Верификация моделей программ: Model checking. Пер. с англ. Под ред. Р. Смелянского. М.: МЦНМО, 2002.416 с.

48. IS09646-2. ISO/IEC 9646. Information technology Open Systems Interconnection - Conformance testing methodology and framework - Part 2: Abstract Test Suite specification. Geneva: ISO, 1994. 33 c.

49. ISO/IEC 9646-3. Information technology Open systems interconnection -Conformance testing methodology and framework - Part 3: The Tree and

50. Tabular Combined Notation (TTCN). 1-е издание. Geneva, Switzerland: ISO, 1992.

51. ISO/IEC 9646-3. Information technology Open systems interconnection -Conformance testing methodology and framework - Part 3: The Tree and Tabular Combined Notation (TTCN). 2-е издание. Geneva, Switzerland: ISO, 1998.

52. ETSI ES 201 873-1 V3.1.1. Methods for Testing and Specification (MTS); The Testing and Test Control Notation version 3; Part 1: TTCN-3 Core Language. Sophia-Antipolis, France: ETSI, 2005. 210 c.

53. OMG formal/05-07-07. UML Testing Profile. Version 1.0. Needham, USA: Open Management Group, 2005. PDF, PostScript. (http://www.omg.org/cgi-bin/doc7formal/05-07-07).

54. L. Ebrecht, M. Schacher, C. Buhler. Test Specification in XML the most important Element for Test Automation. // ARTiSAN Benutzerforum D.A.CH, 2005.

55. Программный комплекс для разработки unit-тестов. URL. http://www.junit.org.

56. Проект TAHI по разработке тестового набора для стека протоколов IPv6. HTML. (http://www.tahi.org/).

57. CCITT Recommendation Z.120. Message Sequence Chart (MSC). Geneve, Switzerland: ITU-T General Secretariat, 1996. 77 c.

58. OMG formal/05-07-04. Unified Modeling Language: Superstructure. Version 2.0. Needham, USA: Open Management Group, 2005. 710 c.

59. ITU-T Rec. X.680 (2002) | ISO/IEC 8824-1:2002. Abstract Syntax Notation One (ASN.l): Specification of Basic Notation. Geneva, Switzerland: ITU-T, 2002; ISO, 2002. 133 c.

60. ITU-T Rec. X.681 (2002) | ISO/IEC 8824-2:2002. Abstract Syntax Notation One (ASN.l): Information Object Specification. Geneva, Switzerland: ITU-T, 2002; ISO, 2002.31 c.

61. ITU-T Rec. X.682 (2002) | ISO/IEC 8824-3:2002. Abstract Syntax Notation One (ASN.l): Constraint Specification. Geneva, Switzerland: ITU-T, 2002; ISO, 2002.10 c.

62. ITU-T Rec. X.683 (2002) | ISO/IEC 8824-4:2002. Abstract Syntax Notation One (ASN.l): Parameterization of ASN.l Specifications. Geneva, Switzerland: ITU-T, 2002; ISO, 2002. 14 c.

63. MIL-STD-188-220. Interoperability Standard for Digital Message Transfer Device Subsystems. 1993.

64. C. Jard, T. Jeron. TGV: Theory, principles and algorithms. // International Journal on Software Tools for Technology Transfer (STTT), vol. 7(4). Berlin: Springer, 2005. C. 297 315. PDF. (http://www.irisa.fr/triskell/publis/2002/Jard02c.pdf).

65. IETF RFC 2462. S. Thomson, T. Narten. IPv6 Stateless Address Autoconfiguration. December 1998. 25 c. TXT. (http://www.ietf.org/rfc/rfc2462.txt).

66. IETF RFC 1851. P. Karn, P. Metzger, W. Simpson. The ESP Triple DES Transform. September 1995. 11 c. TXT. (http://www.ietf.org/rfc/rfc 1851 .txt)

67. IETF RFC 2401. S. Kent, R. Atkinson. Security Architecture for the Internet Protocol. November 1998. 66 c. TXT. (http://www.ietf.org/rfc/rfc2401 .txt)

68. IETF RFC 2402. S. Kent, R. Atkinson. IP Authentication Header. November 1998. 22 c. TXT. (http://www.ietf.org/rfc/rfc2402.txt)

69. IETF RFC 2403. C. Madson, R. Glenn. The Use of HMAC-MD5-96 within ESP and AH. November 1998. 7 c. TXT. (http://www.ietf.org/rfc/rfc2403.txt)

70. IETF RFC 2404. C. Madson, R. Glenn. The Use of HMAC-SHA-1-96 within ESP and AH. November 1998. 7 c. TXT. (http://www.ietf.org/rfc/rfc2404.txt)

71. IETF RFC 2405. C. Madson, N. Doraswamy. The ESP DES-CBC Cipher Algorithm With Explicit IV. November 1998. 10 c. TXT. (http://www.ietf.org/rfc/rfc2405.txt)

72. IETF RFC 2406. S. Kent, R. Atkinson. IP Encapsulating Security Payload (ESP). November 1998. 22 c. TXT. (http://www.ietf.org/rfc/rfc2406.txt)

73. IETF RFC 2410. R. Glenn, S. Kent. The NULL Encryption Algorithm and Its Use With IPsec. November 1998. 6 c. TXT. (http://www.ietf.org/rfc/rfc2410.txt).

74. IETF RFC 2407. D. Piper. The Internet IP Security Domain of Interpretation for ISAKMP. IETF, 1998. 32 c. TXT. (http://www.ietf.org/rfc/rfc2407.txt)

75. IETF RFC 2408. D. Maughan, M. Schertler, M. Schneider, J. Turner. Internet Security Association and Key Management Protocol (ISAKMP). IETF, 1998. 86 c. TXT. (http://www.ietf.org/rfc/rfc2408.txt)

76. IETF RFC 2409. D. Harkins, D. Carrel. The Internet Key Exchange (IKE). IETF, 1998.41 c. TXT. (http://www.ietf.org/rfc/rfc2409.txt)

77. IETF RFC 2710. S. Deering, W. Fenner, B. Haberman. Multicast Listener Discovery (MLD) for IPv6. October 1999. 22 c. TXT. (http://www.ietf.org/rfc/rfc2710.txt).

78. Bourdonov, I., Kossatchev, A., Kuliamin, V., Petrenko, A. UniTesK Test Suite Architecture // Proceedings of FME, LNCS 2391. Springer-Verlag, 2002. P. 77-88.

79. IETF RFC 2223. J. Postel, J. Reynolds. Instructions to RFC Authors. IETF, 1997. 20 c. TXT. (http://www.ietf.org/rfc/rfc2223.txt).

80. Редактор и издатель IETF RFC. URL. http://www.rfc-editor.org/.

81. Центр назначения числовых идентификаторов для Интернета. URL. http://www.iana.org/.

82. IETF ВСР 14 | IETF RFC 2119. S. Bradner. Key words for use in RFCs to Indicate Requirement Levels. IETF, 1997. 3 c. TXT. (http://www.ietf.org/rfc/rfc2119.txt).

83. IETF RFC 2292. W. Stevens, M. Thomas. Advanced Sockets API for IPv6. February 1998.67 c. TXT. (http://www.ietf.org/rfc/rfc2292.txt).

84. IETF RFC 2553. R. Gilligan, S. Thomson, J. Bound, W. Stevens. Basic Socket Interface Extensions for IPv6. March 1999. 41 c. TXT. (http://www.ietf.org/rfc/rfc25 53 .txt).

85. IETF RFC 3775. D. Johnson, C. Perkins, J. Arkko. Mobility Support in IPv6. June 2004. TXT. (http://www.ietf.org/rfc/rfc3775 .txt).

86. CTesK 2.1: SeC Language Reference. M.: ИСП PAH, 2005. 167 c. PDF.http://vvww.unitesk.com/download/papers/ctesk/CTesK2.lLanguageRefere nce.eng.pdf).

87. IETF RFC 2579. K. McCloghrie, D. Perkins, J. Schoenwaelder. Textual Conventions for SMIv2. April 1999. TXT. (http://www.ietf.org/rfc/rfc2579.txt).

88. IETF RFC 1213. K. McCloghrie, M. T. Rose. Management Information Base for Network Management of TCP/IP-based internets: MIB-II. March 1991. TXT. (http://www.ietf.org/rfc/rfcl213.txt).

89. IETF RFC 2011 K. McCloghrie, Ed. SNMPv2 Management Information Base for the Internet Protocol using SMIv2. November 1996. TXT. (http://www.ietf.org/rfc/rfc201 l.txt).

90. IETF RFC 2465. D. Haskin, S. Onishi. Management Information Base for IP Version 6: Textual Conventions and General Group. December 1998. TXT. (http://www.ietf.org/rfc/rfc2465.txt).

91. IETF RFC 2665. J. Flick, J. Johnson. Definitions of Managed Objects for the Ethernet-like Interface Types. August 1999. TXT. (http://www.ietf.org/rfc/rfc2665.txt).

92. IETF RFC 2863. K. McCloghrie, F. Kastenholz. The Interfaces Group MIB. June 2000. TXT. (http://www.ietf.org/rfc/rfc2863.txt).

93. IETF RFC 3635. J. Flick. Definitions of Managed Objects for the Ethernet-like Interface Types. September 2003. TXT. (http://www.ietf.org/rfc/rfc3635.txt).

94. IETF RFC 4293. S. Routhier, Ed. Management Information Base for the Internet Protocol (IP). April 2006. TXT. (http://www.ietf.org/rfc/rfc4293.txt).

95. IETF RFC 4295. G. Keeni, K. Koide, K. Nagami, S. Gundavelli. Mobile IPv6 Management Information Base. April 2006. TXT. (http://www.ietf.org/rfc/rfc4295.txt).

96. И.Б. Бурдонов, A.C. Косачев, B.B. Кулямин. Неизбыточные алгоритмы обхода ориентированных графов. Детерминированный случай. // Программирование, 2003, №5.

97. И.Б. Бурдонов, А.С. Косачев, В.В. Кулямин. Неизбыточные алгоритмы обхода ориентированных графов. Недетерминированный случай. // Программирование, 2004, №1.

98. И.Б.Бурдонов, А.С.Косачев, В.В.Кулямин. Асинхронные автоматы: классификация и тестирование. // Труды ИСП РАН, том 4. М.: ИСП РАН, 1999.

99. IETF RFC 792. J. Postel. Internet Control Message Protocol. IETF, 1981. TXT. (http://www.ietf.org/rfc/rfc0792.txt).

100. IETF RFC 791. J. Postel. Internet Protocol. IETF, 1981. TXT. (http://www.ietf.org/rfc/rfc0791 .txt).

101. IETF RFC 2464. M. Crawford. Transmission of IPv6 Packets over Ethernet Networks. December 1998. 7 c. TXT. (http://www.ietf.org/rfc/rfc2464.txt).

102. ISO/IEC 13818-11. Information technology Generic coding of moving pictures and associated audio information - Part 11: IPMP on MPEG-2 systems. Geneva, Switzerland: ISO, 2004. 74 c.

103. P. Levis, S. Madden, J. Polastre, R. Szewczyk, K. Whitehouse, A. Woo, D. Gay, J. Hill, M. Welsh, E. Brewer, D. Culler. TinyOS: An operating system for wireless sensor networks. // Ambient Intelligence. Springer-Verlag, 2005. ISBN: 3-540-23867-0.

104. B. Meyer. Applying "Design by Contract". // IEEE Computer, vol. 25 №10. USA, 1992. P. 40-51.

105. C. A. R. Hoare. An axiomatic basis for computer programming. // Communications of the ACM, volume 12 №10, 1969. C. 576-580.

106. I. Bourdonov, A. Kossatchev, A. Petrenko, D. Gaiter. KVEST: Automated Generation of Test Suites from Formal Specifications. // Formal Methods 99, LNCS 1708, Springer-Verlag, 1999. C. 608-621.

107. И. Б. Бурдонов, А. В. Демаков, А. С. Косачев, А. В. Максимов, A. К. Петренко. Формальные спецификации в технологиях обратной инженерии и верификации программ. // Труды ИСП РАН, том 1. М.: ИСП РАН, 1999. С. 35-47.

108. IETF RFC 3513. R. Hinden, S. Deering. Internet Protocol Version 6 (IPv6) Addressing Architecture. April 2003. 26 c. TXT. (http://www.ietf.org/rfc/rfc3513 .txt).

109. ETSI TS 102 351. Methods for Testing and Specification (MTS); IP Testing; TTCN-3 IPv6 Test Specification Toolkit VI. 1.1. Sophia-Antipolis, France: ETSI, 2004. 29 c.