Содержание к диссертации
Введение
Глава 1. Анализ современного состояния методов формализации в тестировании телекоммуникационных протоколов 24
1.1 Краткий обзор истории формализации спецификаций и тестов для телекоммуникационных протоколов 24
1.2 Методы формальной спецификации тестов 27
1.3 Методы формального описания протоколов и автоматической генерации тестовых последовательностей 30
1.4 Введение в протоколы Интернета 33
1.5 Постановка задачи 37
Глава 2. Метод формализации стандартов протоколов Интернета 39
2.1 Введение в контрактные спецификации 39
2.2 Описание разработанного метода формализации стандартов протоколов Интернета 45
2.3 Анализ спецификации протокола и извлечение требований 52
2.4 Разработка и анализ концептуальной модели требований 61
2.5 Определение формального интерфейса протокола 73
2.6 Разработка пред- и постусловий для формального интерфейса протокола Интернета 79
2.7 Разработка критериев покрытия 87
2.8 Разработка функций реконструкции состояния 88
Выводы по главе 2 89
Глава 3. Метод формального задания тестов для тестирования соответствия контрактным спецификациям протоколов Интернета 91
3.1 Тестирование соответствия контрактным спецификациям 92
3.2 Обзор разработанного метода формального задания тестов 97
3.3 Определение целей тестирования 100
3.4 Разработка проекта тестового сценария 102
3.5 Разработка итераторов тестовых воздействий и конструкторов конкретных тестовых воздействий 104
3.6 Разработка функции определения текущего состояния сценария... 108
3.7 Разработка настроек тестового сценария 113
3.8 Прогон тестового сценария и анализ результатов тестирования 117
Выводы по главе 3 118
Глава 4. Практические применения 119
4.1 Проекты по тестированию IPv6 в ИСП РАН 119
4.2 Тестирование MSR IPv6 119
4.3 Сравнение с другими тестовыми наборами для IPv6 121
4.4 Применение разработанных методов к другим видам систем 126
Выводы по главе 4 127
Заключение 129
Список литературы
- Методы формального описания протоколов и автоматической генерации тестовых последовательностей
- Описание разработанного метода формализации стандартов протоколов Интернета
- Обзор разработанного метода формального задания тестов
- Тестирование MSR IPv6
Введение к работе
Актуальность работы. Современная сеть Интернет представляет собой гетерогенную сетевую среду - в ней функционируют узлы с сетевыми подсистемами от десятков независимых производителей. Надёжность сети Интернет в значительной степени определяется совместимостью различных реализаций протоколов Интернета между собой.
Тестирование соответствия стандартам Интернета является одним из основных средств обеспечения совместимости реализаций протоколов Интернета. Подходы к тестированию реализаций этих протоколов, использующиеся на практике, основаны на ручной разработке тестовых наборов, состоящих из отдельных элементарных испытаний (test cases). Элементарные испытания представляют собой программы на специализированных языках спецификации тестов, таких как TTCN-2[54] и TTCN-3[55], или на обычных языках программирования - Perl, Java, Си. В каждом элементарном испытании реализуется последовательность тестовых воздействий на целевую систему и вынесение вердикта о корректности наблюдаемого поведения целевой системы. Для каждого элементарного испытания явно или неявно задаётся цель тестирования (test purpose)[38], которая неформально определяет группу функциональных требований к реализации протокола. Успешное или неуспешное завершение элементарного испытания трактуется следующим образом: реализация протокола корректно или некорректно реализует требования, соответствующие цели тестирования.
Для современных сетевых протоколов тестовый набор должен содержать сотни или тысячи элементарных испытаний, что вызывает в практическом тестировании соответствия стандартам Интернета следующие проблемы:
Высокая трудоёмкость разработки из-за низкого уровня автоматизации разработки тестовых наборов.
Низкая доля повторно используемых компонентов тестового набора, прежде всего процедур проверки корректности поведения и генераторов тестовых данных.
Нет формально заданной меры определения полноты тестирования и достоверной процедуры оценки полноты тестирования.
Элементарные испытания, как правило, реализуют только ограниченное число сценариев для проверки соответствующей цели тестирования. Нет подхода, который позволяет существенно повысить «глубину» тестирования и обеспечить всестороннюю проверку требований цели тестирования.
В последнее десятилетие определённый прогресс в решении указанных проблем достигнут в исследованиях в области тестирования с использованием моделей (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 страниц.
Содержание работы
Во введении обосновываются цели и задачи данной работы, её актуальность, научная новизна и практическая значимость. Приводится краткий обзор работы.
Методы формального описания протоколов и автоматической генерации тестовых последовательностей
Согласно определению в RFC3935[73], «Интернет - это большой разнородный комплекс взаимосвязанных систем; любые участники, подключённые к Интернету, могут использовать его для различных видов взаимодействия. Это понятие охватывает как «ядро Интернета» (сети провайдеров), так и «границу Интернета» (корпоративные и частные сети, зачастую подключённые через сетевые экраны, трансляторы адресов, шлюзы прикладного уровня и т.п.)».
Сети провайдеров, частные и корпоративные сети, взаимодействие между сетями и отдельными узлами сетей - всё это осуществляется посредством специализированных телекоммуникационных протоколов, которые в рамках данной работы будут называться протоколами Интернета.
Протоколы Интернета разрабатываются под эгидой Комитета по разработке стандартов Интернета (IETF, Internet Engineering Task Force). Комитет состоит из нескольких отделов (Technology Areas), которые в свою очередь делятся на подкомитеты, отвечающие за разработку регламентирующих документов для отдельных относительно узких областей Интернета. По историческим причинам документы, публикуемые IETF, называются Request For Comments или сокращённо RFC. Большинство спецификаций протоколов Интернета публикуются как Internet standard, поэтому в тексте диссертации будет использоваться термин стандарт Интернета как синоним спецификации протоколов Интернета.
В настоящее время большинство сообщений в сети Интернет передаются в пакетах Интернет-протокола IPv4. Этот протокол был разработан в конце 1970-х годов по заказу Министерства обороны США, стандарт IETF протокола был принят в 1981 году. Помимо гибкого протокола сетевого уровня стек IPv4 включает эффективные протоколы транспортного уровня UDP и TCP, что в конечном итоге привело к абсолютному доминированию IPv4 в современных сетях. Однако уже в середине 1990-х годов стало ясно, что следующие особенности стека IPv4 могут стать фактором, сдерживающим дальнейший рост сети Интернет: 1. Недостаточный размер адресного пространства приведёт к исчерпанию адресов, и будет препятствовать дальнейшему расширению глобальной сети. 2. 32-х битная адресация не позволяет строить эффективные схемы иерархической маршрутизации, что вызовет быстрый (экспоненциальный по времени) рост таблиц маршрутизации. 3. неразвитость средств автоматической конфигурации узлов IPv4 требует ручной настройки всех узлов в сети администраторами, что затрудняет развёртывание новых сетей, поддержание и обновление существующих сетей. 4. Отсутствие встроенной поддержки безопасности передачи данных. 5. Нерасширяемая структура пакета протокола IPv4 не позволяет добавлять новые опции и служебные протоколы непосредственно на сетевом уровне.
С середины 1990-х годов ведутся работы над Интернет-протоколом следующего поколения, который получил название IPv6. Фактически, разработан не один протокол IPv6, а стек служебных протоколов, которые призваны заменить существующий протокол сетевого уровня IPv4. Стек IPv6 содержит ряд усовершенствований по сравнению с IPv4 и разрешает проблемы, которые ограничивают дальнейшее развитие сетей на IPv4. Нет сомнений в том, что со временем протокол IPv6 заменит IPv4 в сети
Интернет, поэтому в данной работе рассматриваются вопросы тестирования протоколов Интернета на примере именно протоколов из стека IPv6.
Стек протоколов IPv6 находится в развитии, в него добавляются новые протоколы и расширяются функции уже стандартизованных, поэтому затруднительно определить рамки IPv6. Тем не менее, можно выделить несколько зафиксированных протоколов, которые обеспечивают базовые функции узлов сети IPv6: отправку и получение пакетов IPv6, механизмы автономной конфигурации узлов, обеспечение безопасности передачи данных на сетевом уровне, мобильность (динамическая смена подключения) в сетях IPv6. К числу таких протоколов относятся собственно протокол IPv6[74], транспортные протоколы ТСР[75] и UDP[76], служебный протокол ICMPv6[77], протоколы Neighbor Discovery[78], функцию автономной конфигурации адресов и протокол проверки уникальности адреса (Duplicate Address Detection, DAD)[79], протоколы безопасности сетевого уровня IPsec[80-87] и Internet Key Exchange (1КЕ)[88-90]. Таблица 1 в краткой форме представляет характеристики этих протоколов, а также одного вспомогательного служебного протокола Multicast Listener Discovery (MLD)[91]. Описание столбцов таблицы и более подробный обзор протоколов Интернета приведён в приложении А.
Из данных, приведённых в Таблице 1 можно сделать следующие выводы об особенностях протоколов Интернета, влияющих на применение средств автоматизации тестирования:
протоколы характеризуются большим числом параметров состояния, наличием в состоянии списков переменной длины и множеств, недетерминированным поведением;
сообщения многих протоколов отличаются сложным устройством: большим числом параметров, наличием списков переменной длины, наличием связей между значениями различных параметров;
Описание разработанного метода формализации стандартов протоколов Интернета
Цель разработанного метода - предоставить процедуру формализации спецификации протокола, в результате выполнения которой получится спецификация протокола, которая удовлетворяет следующим свойствам: 1. однозначность: эксперты в данной предметной области одинаковым образом трактуют спецификацию; 2. проверяемость: для каждого требования в спецификации эксперты в предметной области могут предложить процедуру проверки; 3. адекватность исходным текстовым спецификациям: требования в разработанной спецификации соответствуют требованиям, представленным в исходной спецификации; 4. полнота представления исходной спецификации: все требования исходной текстовой спецификации представлены в разработанной спецификации; 5. прослеживаемость исходной спецификации: есть строго определённая процедура, при помощи которой можно для каждого требования из исходной спецификации определить, как оно представлено в разработанной спецификации и наоборот - для каждого логического или исполнимого выражения модели найти исходные требования, представленные им; 6. пригодность для тестирования соответствия: спецификацию можно использовать для автоматизации тестирования соответствия. Это, в свою очередь, подразумевает: a. возможность генерировать оракулы из спецификации; b. возможность генерировать тестовые данные из спецификации; c. наличие инструментальной поддержки генерации оракулов и тестовых данных из спецификации.
Контрактные спецификации являются однозначными, так как записываются средствами формально определённой нотации. Пригодность контрактных спецификаций для тестирования определяется тем, что из контрактных спецификаций можно построить оракул для проверки корректности внешне наблюдаемого поведения, и есть инструментальная поддержка UniTESK для тестирования на основе контрактных спецификаций (см. Приложение Б).
Рассмотрим достоинства контрактных спецификаций в контексте анализа и формализации требований и проверки соответствия.
1. Контрактные спецификации позволяют сравнительно легко описывать различные виды недетерминированного поведения, в том числе вызванные неполнотой исходной спецификации или особенностями реализации.
2. Существуют эффективные способы автоматического построения тестовых оракулов из контрактных спецификаций [92]. Это позволяет автоматизировать процесс проверки соответствия реализации требованиям.
3. Разработка контрактных спецификаций требует от разработчика мышления в стиле требований к результату, что отличается от характерных стилей мышления разработчиков программных систем. Это позволяет выявить особенности требований, которые остались бы незамеченными при анализе требований средствами прототипирования или разработки экспериментальных реализаций. В частности, мы считаем, что контрактная спецификация позволяет лучше анализировать требования к недетерминированному поведению, чем явные исполнимые спецификации или прототипы.
Разработанный метод призван решить следующую задачу:как построить формальный объект - контрактную спецификацию - М = (S,F,Inv) на основании текстовых спецификации протокола. Метод формализации стандартов Интернета состоит из нескольких шагов. В этом параграфе представлен краткий обзор каждого шага метода. Подробное описание каждого шага метода приводится в последующих параграфах этой главы.
В ходе разработки контрактной спецификации протокола необходимо решить несколько задач: Чётко выделить набор функциональных требований к реализации протокола. В текстах спецификации протоколов такие требования, как правило, перемежаются пояснениями, обоснованиями и подобными высказываниями, которые не несут смысловой нагрузки и призваны облегчить понимание требований читателям спецификации, поэтому перед началом разработки формальной модели протокола необходимо отделить требования от всего остального текста.
Составить формального интерфейса протокола, а именно определить множества входных, выходных и внутренних событий протокола и разработать их представление в виде сигнатур элементов формального интерфейса.
Разработать формальную запись требований к реализации протокола в виде логических формул в пред- и постусловиях элементов формального интерфейса.
Обзор разработанного метода формального задания тестов
В большинстве формальных языков, поддерживающих контрактные спецификации, включая используемое в работе расширение языка Си, нет встроенной поддержки темпоральных спецификаций, то есть спецификаций свойств цепочки событий, упорядоченных во времени. Поэтому в этих формализмах требования к ожидаемой реакции формулируются в постусловии спецификационной функции, соответствующей реакции. Постусловие выносит вердикт на основании истории взаимодействий, которая хранится в модельном состоянии.
Рассмотрим виды выходных событий, которые возникают в протоколах Интернета:
1. Реакции на стимулы. Это реакции, которые, согласно спецификации протокола, должны быть выданы в ответ на определённое входное событие.
2. Реакции на внутренние события. К этой группе относятся внешне наблюдаемые действия, связанные с ненаблюдаемыми извне событиями. Наиболее распространённый вид внутренних событий для протоколов Интернета - истечения таймеров.
На представление реакции в формальной спецификации влияет также и то, через сколько каналов демонстрируются реакции на стимул или внутреннее событие. Обычно одному входному или внутреннему событию соответствуют не более одной реакции, но в отдельных случаях число реакций может быть больше, и доставляться они будут по нескольким независимым каналам. Например, если узел IPv6 получит на групповой (multicast) адрес пакет IPv6 с сообщением UDP в качестве полезной нагрузки, то все сокеты, которые присоединены к этому адресу, получат сообщение UDP.
Предложенные выше методы позволяют проверять корректность наблюдаемых реакций. Тем не менее, этих приёмов недостаточно для решения следующей задачи: проверить, что реализация действительно демонстрирует некоторую реакцию.
В данной работе для решения этой задачи используется следующая методика. Предполагается, что тестируемая система после приёма любого стимула за некоторое ограниченное время переходит в стационарное состояние, в котором тестируемая система ожидает прибытие стимула, и выдача реакций без предшествующего им стимула невозможна. После выдачи тестового воздействия тестовая система собирает в течение некоторого времени реакции. Наблюдаемое поведение тестируемой системы считается корректным, если корректны все реакции и конечное состояние является стационарным. В противном случае поведение реализации считается некорректным.
В формальную спецификацию вводится функция проверки стационарности состояния, которая возвращает определённые значения в зависимости от того, является ли текущее состояние спецификации стационарным или нет.
Требования к обязательности реакций формализуются в функции проверки стационарности. Функция определяет состояние как нестационарное, когда в истории взаимодействия есть стимулы, для которых не наблюдались обязательные реакции, или активные таймеры. Благодаря этому тестовая система вынесет вердикт о некорректности поведения реализации, если реализация не выдала обязательную реакцию.
Рассмотрим, как представляются требования к реакции на входное событие в том случае, когда на него выдаётся не более одной реакции.
Информация о полученных стимулах сохраняется в состоянии формальной спецификации. Модельное состояние может хранить историю стимулов различными способами: в виде списка объектов, набора (мультимножество, multiset), отображения, множества.
Требования, устанавливающие связь между стимулом и реакцией, формализуются в функциях со следующей сигнатурой: bool matchReaction(Object s, ReactionType r);
Первый аргумент соответствует входному событию, второй -реакции. Функция возвращает true, если реакция соответствует стимулу. Для каждой реакции необходимо разработать такую функцию.
Тестирование MSR IPv6
В разработанном методе задания тестов тесты определяются как неизбыточные задания конечных автоматов, из обхода которых и строятся тестовые последовательности посредством генерации тестовых воздействий при обходе неизбыточно заданного конечного автомата. Обходчик автомата стремится подать все тестовые воздействия во всех состояниях автомата, достижимых из начального.
Метод формального задания тестов заключается в проектировании и разработке неизбыточного задания конечного автомата. Такое задание автомата теста, записанное средствами формальной нотации далее будет назваться тестовым сценарием. Проектировщикам и разработчикам тестовых сценариев необходимо решить следующие задачи: определить алфавит входных символов автомата теста: задать множество обобщённых тестовых воздействий; определить состояние автомата теста: разработать факторизацию модельного состояния; разработать итераторы тестовых воздействий и конструкторы конкретных тестовых воздействий; разработать средства настройки теста - параметры теста и механизм передачи параметров в тест при его запуске.
Для решения перечисленных задач разработанных метод формального задания тестов включает следующие шаги: определение целей тестирования; разработка проекта тестового сценария для конкретной цели тестирования; разработка итераторов тестовых воздействий конструкторов конкретных тестовых воздействий; разработка функций определения текущего состояния сценария по модельному состоянию контрактной спецификации стека протоколов; проектирование настроечной информации тестового сценария и разработка формата для представления опций; прогон тестового сценария и анализ результатов тестирования.
На первом шаге метода определяются цели тестирования - аспекты протокола, корректность реализации которых будут проверять разрабатываемые тестовые сценарии. В качестве цели тестирования может выступать набор функций протокола, присутствие определённых полей в сообщениях протокола, выполнение определённых ветвей функциональности в алгоритмах обработки данных, определённые цепочки переходов. Цель тестирования формально задаётся как множество элементов покрытия, которые должны быть покрыты в ходе выполнения сценария.
Второй шаг метода - проектирование неизбыточно заданного автомата теста. В ходе проектировании определяется алфавит обобщённых тестовых воздействий, задаются отношение эквивалентности для факторизации модельного состояния и разрабатываются структуры данных для представления классов эквивалентности. В диссертации разработаны алфавиты тестовых воздействий и факторизации модельного состояния для нескольких часто встречающихся целей тестирования.
На третьем шаге метода разрабатывается формальное описание неизбыточно заданного автомата средствами используемого формализма описания тестовых сценариев, прежде всего итераторы параметров тестовых воздействий и генераторы конкретных сообщений, соответствующих обобщённым тестовым воздействиям. Для часто встречающихся целей тестирования разработаны схемы построения итераторов тестовых воздействий и конструкторов конкретных тестовых воздействий.
На четвёртом шаге метода разрабатываются функции определения текущего состояния автомата тестового сценария, которые строят класс эквивалентности для текущего модельного состояния. Функции определения текущего состояния тестового сценария являются конструктивным представлением отношения эквивалентности, определённого на втором шаге метода.
В диссертации разработаны отношения эквивалентности и итераторы тестовых воздействий для нескольких видов часто встречающихся при тестировании протоколов Интернета целей тестирования. Для них сформулированы и доказаны теоремы о том, что при определённых ограничениях на протоколы предложенные итераторы порождают конечные автоматы, удовлетворяющие требованиям алгоритмов обхода неизбыточно заданных автоматов тестов.
