Содержание к диссертации
Введение
1. Основные понятия, постановка задачи и обзор литературы 20
1.1. Модели дискретных систем 20
1.2. Представление сетевых протоколов при помощи конечных автоматов 25
1.3. Особенности проверки взаимодействия дискретных систем 27
1.4. Модели неисправности и проверяющие тесты 28
1.5. Описание задач, решаемых в работе 30
1.6. Обзор существующих методов 31
1.6.1. Известные операции композиций дискретных систем, решение языковых и автоматных уравнений 31
1.6.2. Обзор методов построения тестов для проверки взаимодействия дискретных систем 34
1.7. Выводы по главе 41
2. Композиция языков, полуавтоматов и автоматов 42
2.1. Обобщенная композиция элементов, поведение которых описано формальными языками 43
2.1.1. Элементы и системы взаимодействующих элементов 43
2.1.2. Построение языка, описывающего поведение системы взаимодействующих элементов 46
2.1.3. Построение языка, описывающего поведение неизвестного элемента в системе 49
2.2. Обобщенная композиция полуавтоматов 51
2.2.1. Описание системы взаимодействующих полуавтоматов 51
2.2.2. Нахождение неизвестного полуавтомата в системе взаимодействующих полуавтоматов 54
2.3. Обсуждение ограничений на структуру и режим работы для композиции конечных автоматов 55
2.4. Частные случаи композиции автоматов 57
2.4.1. Синхронная композиция автоматов 57
2.4.2. Параллельная композиция автоматов 59
2.4.3. Бинарная композиция с кратным стимулированием 64
2.4.4. Некоторые свойства бинарной композиции с кратным стимулированием 71
2.4.5. Нахождение неизвестного автомата в системе взаимодействующих автоматов 75
2.5. Выводы по главе 76
3. Тестирование относительно осцилляции 77
3.1. Модель неисправности для тестирования относительно осцилляции.. 80
3.2. Выбор класса неисправностей на основе частичного задания компонент композиции 81
3.3. Особенности тестирования относительно осцилляции 86
3.4. Метод построения проверяющих тестов на отсутствие осцилляции по мутационному автомату 87
3.4.1. Построение полного проверяющего теста на основе безусловного тестирования 87
3.4.2. Построение полного проверяющего теста на основе условного тестирования 92
3.5. Экспериментальные результаты 98
3.6. Выводы по главе 102
4. Модели неисправности и синтез тестов для проверки функционирования взаимодействующих автоматов при кратном стимулировании 104
4.1. Синтез тестов для композиции 107
4.2. Синтез тестов для композиции 111
4.2.1. Полный проверяющий тест при использовании мутационного автомата 112
4.2.2. Модель неисправности при тестировании композиции 113
4.2.3. Алгоритм построения полного проверяющего теста 114
4.2.4. Построение тестов для компонент сети на основе решения автоматных уравнений 119
4.3. Синтез тестов для удаленной компоненты 120
4.3.1. Построение тестов для композиций А1 0+iA2(Al 0+2А2) 120
4.3.2. Исследование отношения неразделимости 121
4.4. Выводы по главе 127
5. Тестирование программных реализаций протоколов в лабораторном практикуме 129
5.1. Краткое описание предлагаемых лабораторных работ 130
5.2. Ошибки, типичные при реализации любого протокола прикладного уровня 131
5.3. Возможные ошибки при реализации конкретного протокола прикладного уровня 132
5.3.1. Возможные ошибки при реализации протокола РОРЗ 132
5.3.2. Возможные ошибки при реализации протокола SMTP 133
5.3.3. Возможные ошибки при реализации протокола TFTP 134
5.3.4. Возможные ошибки при реализации протокола TIME 135
5.3.5. Возможные ошибки при реализации протокола HTTP 136
5.4. Автоматизация тестирования студенческих реализаций протоколов 136
5.4.1. Постановка задачи автоматизации тестирования 136
5.4.2. Архитектура тестера 138
5.4.3. Пример тестирования РОРЗ-сервера 140
5.5. Выводы по главе 142
Заключение 144
Список литературы 146
- Известные операции композиций дискретных систем, решение языковых и автоматных уравнений
- Элементы и системы взаимодействующих элементов
- Выбор класса неисправностей на основе частичного задания компонент композиции
- Синтез тестов для композиции
Введение к работе
Общая характеристика Актуальность проблемы. Под дискретной системой в работе понимается система, поведение которой описывается последовательностями действий в некотором алфавите. Поведение управляющих дискретных систем описывается при помощи формальных языков, а также таких моделей, как полуавтоматы (источники), сети Петри, автоматы и т. д. [1-11]. Примерами взаимодействующих дискретных систем являются интегральные схемы [5], аппаратные и программные реализации сетевых протоколов [8, 11], мультиагентные системы [13]. При этом системы могут быть соединены между собой различными способами, и режимы их совместного функционирования также могут быть различными. Совместная работа дискретных систем проверяется путем подачи на вход системы проверяющих тестов - последовательностей входных воздействий, и наблюдения выходных реакций системы с последующим их анализом [1, 3, 6]. Моделью дискретной системы, относительно которой достаточно хорошо развиты методы построения проверяющих тестов, является модель с конечным числом переходов, которая в русскоязычной литературе называется конечным автоматом. Тестирование дискретных управляющих систем автоматными методами активно развивалось в работах Г. Бокмана, М.П. Василевского, И.С. Грунского, Н.В. Евтушенко, А. Кавалли, М. Кима, В.В. Кулямина, Д. Ли, Б.Д. Лукьянова, А.Ю. Матросовой, А.Ф. Петренко, М. Янакакиса и других авторов.
Взаимодействующие дискретные управляющие системы могут быть соединены между собой различными способами, и режимы их совместного функционирования также могут быть разными. Методы построения тестов существенно зависят от режима взаимодействия дискретных систем. Известных формальных операций композиции автоматов [2, 40-42], вообще говоря, недостаточно для описания реальных систем, например, для описания поведения дискретных систем при кратном стимулировании, когда входные сигналы могут поступать на
компоненты композиции как одновременно, так и поочередно [36]. Поэтому актуальной остается задача обобщения известных операций композиции для более сложных случаев.
Большинство публикаций по тестированию взаимодействующих конечных автоматов посвящено синтезу тестов для проверки функционирования некоторых видов автоматных композиций, особенно для бинарной параллельной или синхронной композиции [15,17-20, 22, 63]. Авторы предполагают, что взаимодействующие автоматы согласованы, т. е. предполагается соответствие внешних алфавитов взаимодействующих систем, отсутствие несовместимостей при задании их параметров, отсутствие осцилляции при совместной работе и т. п. [15]. Однако, такое предположение не соответствует действительности, т. к. проверка на тупики и осцилляции на этапе валидации [21], т. е. на этапе проверки корректности спецификации, например, таких дискретных управляющих систем, как протоколы, не всегда гарантирует, что при взаимодействии реализаций этих систем от разных производителей осцилляции не возникнет. Поэтому в последнее время появились работы [16], в которых предлагаются методы синтеза тестов только для проверки, могут ли системы функционировать совместно. Тестьг для двух этапов строятся независимо друг от друга, т. к. неизвестна связь между этими тестами. В известных нам работах тесты для проверки совместимости систем строятся эвристически без математической модели [15-20]. Таким образом, актуальной является задача разработки технологии тестирования взаимодействующих автоматов, включающей в себя тестирование на возможность совместного функционирования, для более сложных режимов совместного функционирования, в частности для режима кратного стимулирования.
Цель работы. Разработка методов тестирования композиций дискретных управляющих систем, поведение которых описано конечными автоматами, и которые взаимодействуют в режиме кратного стимулирования.
7 Для достижения поставленной цели решаются следующие задачи.
Обобщение известных операций композиции для описания взаимодействия дискретных систем в режиме кратного стимулирования, и исследование свойств такой композиции.
Разработка модели неисправности и метода синтеза полных проверяющих тестов для проверки дискретных систем на совместимость (отсутствие осцилляции при взаимодействии).
Исследование применимости известных методов построения проверяющих тестов для проверки взаимодействующих дискретных систем на соответствие спецификации при кратном стимулировании, и разработка новых методов для случаев, когда известные методы не применимы.
Методы исследования. Для достижения поставленной цели применяется аппарат дискретной математики, в частности, аппарат теории автоматов, теории формальных языков и математической логики.
ІІаучная новизна работы состоит в следующем: 1) Введена обобщенная операция композиции дискретных систем, которая позволяет формально описать взаимодействие дискретных систем, в том числе в режиме кратного стимулирования. На основе введенной формулы предложена формула для нахождения максимально допустимого поведения неизвестной компоненты дискретной системы, если известен язык композиции и известны языки остальных компонент. Показано, что с применением предложенной формулы может быть построена бинарная композиция автоматов при кратном стимулировании, а также параллельная и синхронная композиции автоматов для произвольного количества компонент и структуры композиции. Введенная формула для нахождения максимально допустимого поведения адаптирована для нахождения максимально допустимого поведения компоненты автоматной композиции.
Введена модель неисправности и предложен метод построения полных проверяющих тестов для проверки дискретных управляющих систем на совместимость (отсутствие осцилляции при взаимодействии).
Предложены алгоритмы построения полных проверяющих тестов для проверки автоматной композиции с кратным стимулированием на соответствие спецификации при различных условиях доступа к каналам композиции.
Показано, что синтез полного проверяющего теста относительно неразделимости нельзя свести к синтезу теста относительно отношений эквивалентности и редукции, для которых известны методы построения полных проверяющих тестов. Предложен алгоритм построения полного проверяющего теста для недетерминированных автоматов относительно неразделимости, который может быть использован при удаленном тестировании.
Практическая ценность. Предложенные в работе методы синтеза тестов для проверки взаимодействия дискретных систем могут быть использованы, в частности, при проверке взаимодействия аппаратных и программных реализаций телекоммуникационных протоколов, а также при тестировании распределенных мультиагентных систем.
Реализация полученных результатов. Исследования, результаты которых изложены в диссертации, проводились в рамках работ по программе «Университеты России» (2002-2003 г.), НИР «Алгебра конечных автоматов и полуавтоматов: отношения, операции, решение уравнений», а также в рамках международного проекта по исследованию и обучению методам тестирования TAROT (Training and Research on Testing, с 2004 г.) и по программе МОН РФ «Развитие научного потенциала высшей школы» (2005 г.), НИР «Разработка методологии тестирования совместного функционирования телекоммуникационных протоколов на основе теории автоматов». Кроме того, результаты исследований по тестированию сетевых протоколов нашли применение при выполнении НИР «Лабораторные работы по курсу «Интернет-программирование» при поддержке
9 ИДО ТГУ в рамках программы информатизации ТГУ. Разработанная система автоматизированного тестирования студенческих реализаций протоколов прикладного уровня внедрена в учебный процесс на радиофизическом факультете ТГУ.
Документы, подтверждающие участие автора в работе по грантам, можно найти в приложении к настоящей диссертации.
Апробация работы. Научные результаты [67-79], составившие основу данной работы, обсуждались на заседаниях объединенного семинара кафедры информационных технологий в исследовании дискретных структур радиофизического факультета, кафедры защиты информации и криптографии и кафедры программирования факультета прикладной математики и кибернетики ТГУ. Кроме того, они докладывались на конференциях различного уровня, в том числе международных, в гг. Саратове, Берлине, Оксфорде, Москве и Томске, что подтверждается соответствующими публикациями докладов и тезисов докладов [67, 68, 70, 71, 73, 74, 76, 77, 79].
Структура и объем диссертации. Диссертация состоит из введения, 5 глав, заключения и списка используемой литературы. Объем диссертации составляет 158 страниц текста, набранного в редакторе Microsoft Word 2000 (Шрифт -Times New Roman, размер шрифта - 14 pt, межстрочный интервал - 1,5 строки), в том числе: титульный лист - 1 стр., оглавление - 3 стр., основной текст, включающий 53 рисунка и 3 таблицы, - 141 стр., библиография из 79 наименований - 8 стр., приложение - 5 стр. Основное содержание работы
Первая глава диссертации содержит необходимые понятия из теории дискретных систем, формальных языков и теории автоматов, обзор публикаций, посвященных тестированию конечно автоматными методами взаимодействующих дискретных систем, и формулировку задач, которые решаются в диссертационной работе.
Для синтеза качественных проверяющих тестов необходима математическая модель неисправности, которая включает формальное описание композиции взаимодействующих систем, и отношение соответствия (конформности) между системами. Известен ряд операций композиции дискретных систем [2, 14,40-42]. Например, известно, как построить параллельную композицию дискретных систем, описанных языками [14], конечными автоматами [41], а также как построить синхронную композицию конечных автоматов [2, 41]. Результатом этих операций является конечный автомат, причем, если исходные автоматы детерминированные, то и композиция будет детерминированным автоматом. Известны методы построения тестов для проверки функционирования таких композиций автоматов [46, 56, 62, 63] (методы синтеза тестов на соответствие спецификации).
В работе [14] вводится формула для описания операции параллельной композиции двух дискретных систем, которая ранее описывалась в теории процессов только алгоритмически (см., например, [43]). В параллельной композиции в каждый такт взаимодействия возможно наличие сигнала только на одном из полюсов композиции. В работе [14] операция определяется как композиция языков компонент, причем в определении операции отсутствует структура композиции. В работе [2] рассматривается задача построения синхронной композиции из п структурных автоматов. Синхронность подразумевает одновременную работу всех дискретных систем, т. е. в каждый такт взаимодействия на каждом полюсе композиции есть сигнал. Структура композиции задается при помощи разбиения множества полюсов. В работе рассматриваются условия корректности построения схемы, т. е. условия, при соблюдении которых построенная схема будет являться автоматом. В работах [40-42] вводится формула для описания параллельной и синхронной композиции дискретных систем определенной структуры.
На практике часто используются более сложные режимы взаимодействия
дискретных систем, чем синхронное и поочередное (как при параллельной ком
позиции) взаимодействие. Например, при верификации TCP-протокола в режи
ме параллельной композиции не накрывается переход
Syn_sent—SYN,SYN-ACK )Syn_rcvd. Для проверки этого перехода необходимо исполь
зовать так называемое кратное стимулирование, при котором на внешние полю
сы взаимодействующих компонент сигналы могут поступать как по отдельно
сти, так и одновременно [36]. В известной нам литературе нет формальной опе
рации композиции, позволяющей описать такого рода взаимодействие.
В известных нам работах при тестировании дискретных систем используется модель неисправности <А,&, Ш> [46], где А описывает поведение эталонной дискретной системы (спецификации), 9Ї задает класс неисправности, « - отношение соответствия, в котором должны находиться эталонная и проверяемая системы. При этом предполагается, что в любой проверяемой системе компоненты согласованы, т. е. предполагается соответствие внешних алфавитов взаимодействующих систем, отсутствие несовместимостей при задании их параметров, отсутствие осцилляции при совместной работе и т. п. [15]. Однако этап тестирования совместимости компонент не рассматривается. Исследования, посвященные проверке совместимости компонент системы, проводились независимо. Ниже мы кратко представляем известные в этой области результаты.
Одной из основных проблем, возникающих при взаимодействии дискретных систем, являются осцилляции, т. е. бесконечные циклы, когда композиции не достигает устойчивого состояния после некоторого воздействия.
В известных нам работах тесты для выявления осцилляции строятся эвристически без математической модели [16], или этот этап тестирования вообще не рассматривается [15, 17-20]. Проверка на тупики и осцилляции на этапе ва-лидации [21], т. е. на этапе проверки корректности спецификации таких дискретных систем, как протоколы, не всегда гарантирует, что при взаимодействии
12 реализаций этих систем от разных производителей осцилляции не возникнет. Это связано с тем, что спецификации бывают частичными, и в реализациях неопределенные части спецификаций могут быть определены по-разному. Если в проверяемой системе осцилляции отсутствуют и поведение системы описывается параллельной или синхронной композицией автоматов, то для проверки правильности работы композиции можно воспользоваться известными формальными моделями неисправности. В этих моделях, как правило, предполагается, что неисправности возможны в любой, но только в одной компоненте сети. Подобное предположение достаточно реалистично, поскольку вероятность неисправности нескольких компонент значительно меньше. Известно, что тесты, построенные для одиночных неисправностей, обнаруживают большое количество других неисправностей, в частности, такие тесты обнаруживают константные неисправности на связях между компонентами [8]. Если предполагать, что неисправности возможны только в одной компоненте сети, можно говорить о тестировании компоненты сети в контексте другого автомата [46]. Проверяющие тесты могут быть построены на основе автомата сети или на основе тестируемой компоненты сети.
Автомат сети строится посредством композиции эталонной компоненты и контекста. Известно несколько подходов к построению тестов на основе автомата сети, а именно: перечисление всевозможных неисправностей в компоненте, синтез тестов на основе верхней оценки числа состояний композиции методами, предложенными в [24-31], представление класса неисправностей при помощи мутационного автомата [35]. Перечисление всех неисправностей позволяет строить безызбыточные тесты, однако обычно не применимо на практике; тесты, основанные на верхней оценке числа состояний композиции, избыточны, т. к. не учитывается исправность контекста; мутационный автомат позволяет учесть исправность контекста, однако, также содержит «лишние» подавтоматы, которые не описывают поведение ни одной из тестируемых композиций.
При построении тестов на основе тестируемой компоненты сети, использу-ется максимально допустимое поведение компоненты, которое может быть описано специальным недетерминированным автоматом, называемым сетевым эквивалентом [54, 55]. Сетевой эквивалент обычно находится решением соответствующего автоматного уравнения. Задача трансляции внутренних тестов на внешние полюсы сети может решаться для всех последовательностей теста одновременно на основе решения автоматных уравнений [56].
Нам известна единственная работа [22], в которой проверяющие тесты для композиции автоматов при кратном стимулировании строятся на основе формальной модели неисправности, а именно для выходных неисправностей в компонентах сети.
Следует также отметить, что модели неисправности, применяемые при построении тестов для синхронной и параллельной композиций, не могут быть напрямую применены для композиции с кратным стимулированием, по следующим причинам. Известно, что при кратном стимулировании результатом композиции детерминированных автоматов может быть недетерминированный автомат. Поэтому необходимы модели неисправности, в которых и спецификация, и реализация могут быть недетерминированными автоматами. Отсутствует формула, позволяющая найти максимально допустимое поведение компоненты для композиции с кратным стимулированием, в результате чего подход с использованием сетевого эквивалента не может быть применен. На основании вышесказанного, сделаны следующие выводы:
Известных формальных операций композиции автоматов недостаточно для описания поведения взаимодействующих систем, в частности для описания поведения композиции автоматов при кратном стимулировании.
Отсутствует формальная модель неисправности и методы построения проверяющих тестов с гарантированной полнотой для проверки композиции автоматов на осцилляции.
3. При синтезе тестов для композиции автоматов при кратном стимулировании рассматривалась только модель выходных неисправностей компонент, причем не учитывались различные возможности управления и наблюдения для компонент композиции.
Данная работа посвящена заполнению описанных выше пробелов для взаимодействующих дискретных систем, которые можно описать как композицию автоматов с кратным стимулированием.
В первой главе также описаны такие модели дискретных управляющих систем, как формальные языки, полуавтоматы, автоматы. Известно [1-11], что все эти модели используются для описания поведения различных дискретных систем, в частности для описания сетевых протоколов [8, 11]. В качестве примера рассмотрено описание конкретного сетевого протокола РОРЗ при помощи конечного автомата. Отмечается необходимость разработки технологии тестирования взаимодействующих автоматов при кратном стимулировании, включающей два этапа: тестирование на возможность совместного функционирования и проверку функционирования. Необходимо отметить, что второй этап -проверка функционирования, для которого методы построения тестов более развиты, не обязательно включает проверку на совместимость, например, проверку на отсутствие осцилляции. Поэтому, на первом этапе композиция взаимодействующих систем проверяется на возможность возникновения осцилляции, на втором этапе композиция проверяется на соответствие спецификации.
Вторая глава диссертации посвящена операции композиции для языков, полуавтоматов и автоматов. Как было отмечено выше, известные операции композиции не позволяют описать некоторые виды взаимодействия, которые встречаются на практике. Дискретные системы взаимодействуют, обмениваясь последовательностями действий, т. е. словами в некотором заданном языке. Каким будет язык, описывающий взаимодействующие дискретные системы, зависит от структуры композиции, которая может быть формально задана при по-
15 мощи разбиения, в котором отождествленные полюсы объединены в классы (среди которых выделены классы, содержащие внешние полюсы), и режима взаимодействия, который может быть задан при помощи матрицы несовместимости, определяющей, на каких полюсах сигналы не могут возникнуть одновременно. В параграфе 2.1 вводится обобщенная операция композиции, позволяющая описать совместное поведение взаимодействующих дискретных систем при заданных структуре и матрице несовместимости для случая, когда поведение дискретных систем задано формальными языками; на основе введенной операции предлагается формула для нахождения наибольшего допустимого языка, описывающего поведение неизвестного элемента композиции. В параграфе 2.2 предлагается эффективный алгоритм построения композиции в случае, если языки взаимодействующих дискретных систем регулярные, т. е. поведение таких дискретных систем может быть описано конечным способом посредством полуавтоматов. Результатом композиции полуавтоматов будет полуавтомат, т. к. класс регулярных языков замкнут относительно операций, используемых при построении композиции. Также предлагается эффективный алгоритм нахождения наибольшего решения полуавтоматного уравнения.
В параграфе 2.3 обсуждаются ограничения на структуру и режим работы для композиции конечных автоматов. Распространить введенную операцию композиции на конечные автоматы так, чтобы результатом композиции был автомат, в общем случае не удается. В параграфе 2.4 бинарные операции параллельной и синхронной композиции автоматов, описанные формально в [40-42], обобщаются с использованием введенной операции на произвольное число компонент и произвольную структуру композиции. Кроме того, введенная формула используется для описания бинарной композиции с кратным стимулированием, которая ранее описывалась только алгоритмически. Установлен ряд свойств для бинарной композиции с кратным стимулированием; например, показано, что если автоматы А1 и А2 детерминированные, то композиция с крат-
ным стимулированием в общем случае будет наблюдаемым недетерминированным автоматом с детерминированной функцией переходов. При этом, если нас не интересует порядок появления выходных последовательностей на различных внешних полюсах, то автомат композиции будет детерминированным автоматом. Если же для наблюдения доступны внешние входной и выходной каналы только одной компоненты (но при этом внешнее воздействие может быть подано и на другую компоненту), то недетерминированный автомат композиции с кратным стимулированием может иметь недетерминированную функцию переходов при детерминированных автоматах А\ и А2.
Алгоритм нахождения наибольшего решения полуавтоматного уравнения адаптирован к решению уравнений для конечных автоматов.
Третья глава посвящена проверке взаимодействующих дискретных систем на отсутствие осцилляции. В параграфе 3.1 вводится модель неисправности
17 таты компьютерных экспериментов, которые показывают, что хотя условные тесты обычно значительно короче безусловных, в некоторых случаях длина условного теста может даже превосходить длину безусловного теста.
Четвертая глава посвящена тестированию бинарной композиции автоматов с кратным стимулированием на соответствие спецификации. Обсуждаются модели неисправности и методы построения проверяющих тестов при различных точках доступа к каналам взаимодействующих автоматов. В параграфе 4.1 рассматривается общий случай композиции двух детерминированных автоматов с кратным стимулированием, когда автомат композиции является недетерминированным автоматом с детерминированной функцией переходов. В этом случае проверяющие тесты должны строиться для недетерминированных автоматов относительно отношения эквивалентности.
В параграфе 4.2 рассматривается частный случай бинарной композиции с кратным стимулированием, когда нас интересуют внешние выходы каждой из компонент независимо друг от друга, т. е. нас не интересует порядок выдаваемых системой символов в разных выходных каналах. Согласно утверждению 2.5, в этом случае поведение автоматной сети с кратным стимулированием из детерминированных автоматов описывается детерминированным автоматом. В связи с этим можно использовать те же модели неисправности, что и при построении проверяющих тестов для параллельной и синхронной композиции автоматов. В разделе 4.2.3 предлагается усовершенствованный метод синтеза проверяющих тестов для автоматной сети на основе мутационного автомата, согласно которому, используется не один, а несколько мутационных автоматов. После построения тестов для одного мутационного автомата остальные мутационные автоматы сокращаются. Из них удаляются подавтоматы, соответствующие неисправностям, которые обнаружимы уже построенным тестом [77]. Подобно разделу 3.2, метод иллюстрируется для случая, когда неисправности воз-
18 можны только в переходах компонент, которые «жестко» не зафиксированы в спецификации.
В параграфе 4.2.4 задача синтеза проверяющего теста для компоненты автоматной сети решается на основе решения автоматных уравнений. В частности, показывается, что при кратном стимулировании, так же как и в случае параллельной и синхронной композиции, можно построить недетерминированный автомат, описывающий допустимое поведение тестируемой компоненты, на основе решения автоматного уравнения. В данном разделе также отмечается, что задача трансляции внутренних тестов на внешние полюсы сети может решаться для всех последовательностей теста одновременно на основе решения автоматных уравнений [56, 78].
В параграфе 4.3 рассматривается ситуация, когда отсутствует доступ ко входам и выходам одной из компонент (т. е. удаленное тестирование). В этом случае, недетерминированный автомат композиции может иметь недетерминированную функцию переходов при детерминированных автоматах А\ и А2. Показывается, что проверяющие тесты должны строиться для модели неисправности, в которой эталонный и проверяемый автоматы являются недетерминированными, и отношением соответствия между проверяемым и эталонным автоматами является отношение неразделимости. Отмечается, что синтез полного проверяющего теста относительно такой модели неисправности нельзя свести к синтезу теста относительно известных отношений эквивалентности и редукции. Предлагается алгоритм построения разделяющей последовательности для заданных наблюдаемых автоматов А и В (если существует). Данный алгоритм дает возможность строить полные проверяющие тесты относительно неразделимости путем перебора автоматов из области неисправности.
В пятой главе описывается система автоматизированного тестирования студенческих реализаций протоколов прикладного уровня. В разделе 5.1 приводится краткое описание лабораторных работ, предлагаемых для выполнения по
19 курсу «Интернет-программирование». В разделах 5.2 и 5.3 вводится классификация наиболее вероятных ошибок, которые могут быть свойственны либо реализации только данного протокола, либо реализации любого протокола прикладного уровня, предлагаются тестовые последовательности, гарантирующие обнаружение и/или локализацию таких ошибок. В разделе 5.4 описывается подход к автоматизации процесса тестирования студенческих реализаций протокола, который был реализован при выполнении проекта «Лабораторные работы по курсу «Интернет-программирование» при поддержке ИДО ТГУ в рамках программы информатизации ТГУ.
В заключении подводится итог результатам, полученным в диссертации, и формулируются основные положения, выносимые на защиту.
Известные операции композиций дискретных систем, решение языковых и автоматных уравнений
В различных работах [2, 14,40-42] вводятся различные операции композиции конечных полуавтоматов и автоматов. Наиболее хорошо известны так называемые синхронная и параллельная композиции. При синхронной композиции предполагается, что у системы (автомата) нет задержки между входным и выходным сигналом. Все взаимодействие происходит мгновенно в один такт при поступлении синхросигнала. На внешние входы компонент поступают внешние входные воздействия, компоненты генерируют соответствующие внутренние и внешние выходные воздействия; последние и наблюдаются на внешних выходах композиции. При параллельной композиции предполагается, что каждая компонента может обрабатывать входное воздействие достаточно долго, потом взаимодействовать с другой компонентой посредством внутреннего выходного символа или с внешней средой посредством внешнего выходного сигнала. Поэтому в каждый такт в композиции находится всего один сигнал; следующее входное воздействие поступает только после того, как композиция произвела выходной символ на предыдущий входной сигнал. Свойства такой композиции наиболее активно изучались в алгебре процессов; полученные результаты использовались, в частности, при синтезе тестов для протоколов телекоммуникационных систем.
Одной из первых работ, где рассматривается задача построения синхронной композиции из п структурных автоматов, является книга В. М. Глушкова [2]. Структура схемы (сети) автоматов задается при помощи разбиения множества полюсов на множества попарно непересекающихся отождествленных полюсов. В работе рассматриваются условия корректности построения схемы, т. е. условия, при соблюдении которых построенная схема будет являться автоматом. В частности, к таким условиям относится, что всякая петля (линия обратной связи) в схеме должна содержать хотя бы один автомат Мура, т. е. такой автомат, выходной символ которого определяется только состоянием, т. е. в каждом состоянии выходной символ не зависит от входного сигнала (во избежание возникновения неоднозначностей на полюсах петли). В работе [40] формулируются более «тонкие» условия, позволяющие избежать неоднозначностей - а именно, для всякой пары состояний st автомата композиции достаточно, чтобы лишь из одного состояния из этой пары внутренний выход не зависел бы от внутреннего входа.
В работе [14] вводится операция параллельной композиции на языках для двух дискретных систем. По сути, эта операция представляет собой расширение языков компонент на алфавиты системы, и затем пересечение этих языков. При этом в работе не фигурирует структура системы. На практике часто используются более сложные режимы взаимодействия дискретных систем, чем синхронное и поочередное (как при параллельной ком позиции) взаимодействие. Например, при верификации TCP-протокола в режи ме параллельной композиции не накрывается переход Syn_sent—swlsm-ACK Syn_rcvd. Для проверки этого перехода необходимо исполь зовать так называемое кратное стимулирование, при котором на внешние полю сы взаимодействующих компонент сигналы могут поступать как по отдельно сти, так и одновременно [36]. В известной нам литературе нет формальной опе рации композиции, позволяющей описать такого рода взаимодействие. Для параллельной и синхронной композиции в литературе активно обсуждались возможности построения неизвестной компоненты композиции автоматов [41-45]. Описание максимально допустимого поведения компоненты используется при синтезе тестов для автоматных композиций [46]. Задача сводится к решению автоматных уравнений. Известен ряд результатов по решению данной задачи для синхронной композиции. Обзор этих результатов можно найти в [47, 48]. В работе [43] получены Необходимые и достаточные условия решения полуавтоматного уравнения для префиксзамкнутых регулярных языков, т. е. регулярных языков, в которых начальный отрезок любого слова также принадлежит языку. В работе [44] авторы разработали алгоритм для описания максимально допустимого поведения компоненты в композиции полуавтоматов. Для этой цели в работе вводится понятие безразличного состояния (don t care).
В работе [41] вводятся операции бинарной параллельной и синхронной композиции для языков, полуавтоматов и автоматов, а также формулы для описания максимально допустимого поведения компоненты синхронной и параллельной композиции языков, полуавтоматов и автоматов. Операции вводятся только для композиции определенной структуры. Формулы для операций параллельной и синхронной композиций включают в себя известные теоретико-множественные операции дополнения, пересечения, проекции и подстановки, относительно которых множество регулярных языков замкнуто. В работе также показывается, каким образом множество решений полуавтоматного уравнения можно ограничить для получения решения в классе конечных автоматов. Таким образом, предлагается формула для максимально допустимого поведения компоненты в виде конечного автомата для бинарной синхронной и параллельной композиции автоматов определенной структуры.
В работах [49-52] предлагается строить композицию автоматов при помощи так называемого графа достижимости, в котором вершинам сопоставлены пары состояний композируемых автоматов, ребра помечаются парами «входной символ / выходной символ», и смежные вершины с соединяющим их ребром соответствуют переходу в одном из композируемых автоматов. Построение графа достижимости начинается с пары начальных состояний автоматов, заканчивается когда достигнуты все достижимые состояния. Граф достижимости также можно использовать при описании композиции из п автоматов [49, 50]. Однако формулы для описания такой композиции отсутствуют, что не позволяет, в частности, формально описать максимально допустимое поведение компоненты композиции на основе графа достижимости.
Элементы и системы взаимодействующих элементов
Для разработки методов синтеза тестов для взаимодействующих дискретных управляющих систем с гарантированной полнотой необходимо формально определить операцию композиции, т. е. описать поведение взаимодействующих систем с помощью математической модели, которая используется для описания поведения отдельной системы. Иными словами, композиция полуавтоматов должна быть описана полуавтоматом, композиция автоматов - автоматом и т. п. Общим в поведении дискретных управляющих систем является то, что их поведение можно описать последовательностями допустимых действий в заданном алфавите, т. е. формальным языком. Системы могут взаимодействовать по различным правилам. Например, в каждый такт может быть разрешено взаимодействие только по одному каналу - такой режим взаимодействия называется параллельным [14, 43-45], или в каждый такт задействованы все каналы - такой режим взаимодействия называется синхронным [2, 10, 40, 41]. Однако на практике возможно более сложное совместное функционирование (например, режим, при котором разрешены совместные входные воздействия (кратное стимулирование), асинхронное взаимодействие). В данной работе мы обобщаем операции параллельной и синхронной композиции и предлагаем формулу для описания языка композиции. В каждый такт в композиции могут быть активными несколько каналов, но не обязательно все каналы. Операция композиции вводится для элементов, поведение которых описано формальными языками, и показывается, как с использованием этой операции можно получить язык, описывающий поведение неизвестного элемента в системе взаимодействующих элементов, а именно, предлагается формула для наибольшего решения языкового уравнения относительно введенной операции композиции (раздел 2.1).
В разделе 2.2 предложен эффективный способ построения композиции и решения языкового уравнения в случае, если языки элементов являются регулярными. Регулярные языки реализуются полуавтоматами, или источниками [4, 58], поэтому построение композиции и нахождение решения языкового уравнения сводятся к известным операциям над конечными полуавтоматами.
Распространить введенную операцию композиции на конечные автоматы так, чтобы результатом композиции был автомат, в общем случае не удается (раздел 2.3). Поэтому для автоматов обсуждаются необходимые ограничения на операцию композиции. В частности, при композиции автоматов не разрешается отождествлять выходные полюсы различных автоматов. Кроме того, для того, чтобы остаться в классе автоматных языков, между автоматами - элементами композиции в некоторых случаях приходится вводить буферы, в которых «запасаются» поступившие входные символы. Таким образом, для описания взаимодействия двух автоматов, на самом деле рассматривается композиция из четырех элементов, два из которых являются входными буферами. Дополнительным ограничением обычно является так называемая «медленная» внешняя среда, когда следующий входной сигнал на композицию автоматов может быть подан только после того, как все внутренние каналы становятся пустыми. Такая композиция подробно рассматривается в разделе 2.4, где также показывается, что введенная операция адекватно описывает композицию автоматов с кратным стимулированием, которая, в частности, используется для описания взаимодействия протокольных объектов.
В данном разделе речь идет об элементах. Элемент С характеризуется множеством полюсов. Каждому полюсу соответствует некоторый алфавит. Пусть для определенности алфавит Aj соответствует у -му полюсу элемента С, т. е. на этом полюсе возможны последовательности сигналов только из алфави Формально структура композиции (отождествление полюсов) может быть задана при помощи разбиения щ в котором отождествленные полюсы объединены в классы {блоки, узлы [2], цепи [5]), \л\ = к. Для системы взаимодействующих элементов на рис.2.2 п= {1; 2,4,6 ; 3 ; 5,7 ; 8 }. Каждому классу bt разбиения 7Г поставим в соответствие алфавит Bt, который получается при пересечении всех алфавитов полюсов класса 6,-. Таким образом, только символы из алфавита В, могут появиться на полюсах класса Ъ, разбиения х Среди множества полюсов выделяют внешние полюсы, т. е. полюсы, сигналы на которых появляются из внешней среды. На рис.2.2 можно видеть, что с внешней средой связаны полюсы с номерами 1, 3 и 8. Обозначим через в множество всех блоков из ж, которые содержат внешние полюсы системы, Ocz к. Последовательности сигналов на полюсах из множества в описывают внешнее поведение системы. Для системы взаимодействующих элементов на рис.2.2 в = {1; 3 ; 8 }. Существуют режимы работы композиции, при которых некоторые узлы композиции не могут быть активными одновременно. Например, при параллельной композиции в каждый такт работы композиции активным является только один узел.
Выбор класса неисправностей на основе частичного задания компонент композиции
Проверяющие тесты для автоматов обычно строят на основе так называемых умозрительных экспериментов с автоматами, которые бывают безусловными и условными [3]. При безусловном тестировании множество тестовых последовательностей формируется заранее. Входные последовательности затем подаются на тестируемую систему; если проверяемая система на каждую тестовую последовательность реагирует конечной выходной последовательностью, то мы заключаем, что в проверяемой системе отсутствуют осцилляции первого и второго рода. Более того, если ни одна наблюдаемая выходная последовательность не совпадает с теми, при которых возможна осцилляция третьего рода, то мы заключаем, что в проверяемой системе отсутствуют осцилляции.
При условном эксперименте каждая следующая тестовая последовательность определяется в зависимости от реакции проверяемой системы на предыдущие тестовые последовательности. Условные тесты [57] обычно короче безусловных, но требуют более сложного оборудования для организации процесса тестирования.
В разделе 3.4.1 предлагается алгоритм построения безусловного проверяющего теста, который является полным относительно модели неисправности Sub(MM), отсутствие осцилляции . В разделе 3.4.2 предлагается алгоритм построения полного проверяющего теста при условном тестировании проверяемой системы.
Построение полного проверяющего теста на основе безусловного тестирования При синтезе проверяющего теста, который строится заранее, и обнаруживает любую проверяемую систему, в которой есть осцилляция (или может быть осцилляция третьего рода), основным является накрытие определенных переходов в любом подавтомате мутационного автомата, а именно, переходов в состояние ОСЦИЛЛЯЦИЯ.
Напомним, что состояние s автомата A = (S, X, Y, h, s0) называется детерминировано достижимым, если существует последовательность, детерминировано переводящая автомате в состояние s , т. е. накрывающая только переходы, в которых однозначно определен переход в следующее состояние при данном входном воздействии. d-Покрыеающим множеством автомата А называется множество входных последовательностей автомата , по которым достигаются все детерминировано достижимые состояния.
Поскольку гарантировано накрываются только детерминировано достижимые переходы (которые есть в каждой реализации), то естественный подход при построении такого теста накрыть в каждой реализации переход в состояние ОСЦИЛЛЯЦИЯ из каждого состояния. Построим автомат ММшигт, удалив из автомата ММ состояние ОСЦИЛЛЯЦИЯ, и все переходы в это состояние. Пусть в автомате MMNoLTr и состояний, из них m детерминировано достижимы.
Построение теста основано на следующем наблюдении: длина последовательности, по которой в любой реализации из детерминировано достижимых состояний достижимо любое состояние, будет не больше, чем n-m. Поэтому, чтобы из детерминировано достижимого состояния накрыть переход в состояние ОСЦИЛЛЯЦИЯ, достаточно последовательности длины n-m+1. Как обычно, мы предполагаем, что каждый автомат обладает исправным сигналом сброса г, который переводит систему в начальное состояние.
Частный случай. Все состояния автомата ММц0ип из которых в автомате ММ есть переходы в состояние ОСЦИЛЛЯЦИЯ, достижимы детерминировано. В этом случае, для каждого перехода из такого состояния st автомата ММ под действием входного символа х добавим в проверяющий тест последовательность г.ах, где г - символ сброса, а, а- входная последовательность, детерминировано переводящая автомат -MMNoLTr из начального состояния в состояние st. Общий случай. В общем случае, не все состояния автомата MM OLTT, ИЗ которых в автомате ММ есть переходы в состояние ОСПДЛЛЯЦИЯ, достижимы детерминировано. Для построения полного проверяющего теста без явного перечисления всех возможных реализаций предлагается использовать следующий алгоритм [74, 77].
Синтез тестов для композиции
В данной главе рассматривается тестирование автоматной сети из двух компонент. Задача такого тестирования может быть формально поставлена на основе модели неисправности в виде тройки: 1) автомата-эталона, описывающего поведение исправной дискретной системы; 2) множества автоматов, описывающих поведение системы при возможных неисправностях; 3) отношения, в котором должны находиться проверяемый и эталонный автоматы [46]. Обычно считается, что неисправности возможны только в компонентах автоматной сети. Таким образом, мы полагаем, что неисправная система получается из эталонной при замене одной из ее компонент некоторым другим (возможно, неисправным) детерминированным автоматом. Подобное предположение достаточно реалистично, поскольку тесты для компонент сети обнаруживают и большое количество других неисправностей, в частности, такие тесты обнаруживают константные неисправности на связях между компонентами [7].
Модели неисправности и методы синтеза проверяющих тестов для параллельной композиции автоматов рассмотрены в работах [46, 56, 62], для синхронной композиции - в работе [63]. В обоих случаях поведение автоматной сети описывается детерминированным автоматом. При кратном стимулировании автомат, описывающий поведение сети, в общем случае является недетерминированным. В данной главе мы предлагаем модели неисправности для композиции с кратным стимулированием при различном доступе к компонентам сети. Кроме того, в отличие от предыдущих исследований мы полагаем, что неисправными могут быть обе компоненты сети.
В данной главе мы рассматриваем систему, состоящую из двух автоматов-компонент, структура которой представлена на рис. 1.2. Компоненты А\ и А2 являются детерминированными автоматами. В каждый момент времени внешний входной сигнал поступает либо на одну из компонент, либо одновременно на обе компоненты. Как обычно, мы полагаем, что следующий внешний входной сигнал поступает только тогда, когда все очереди пусты, т. е. после полной обработки системой предыдущего входного сигнала (раздел 2.3). Кроме того, композиция автоматов А\ и А2 не содержит осцилляции, т. е. предполагается, что поведение системы уже проверено с помощью тестов, методы построения которых были предложены в главе 3.
В разделе 4.1 рассматривается общий случай композиции с кратным стимулированием двух детерминированных автоматов А\ иА2. Автомат композиции А\0ХА2, согласно утверждению 2.4, является наблюдаемым недетерминированным автоматом с детерминированной функцией переходов. Таким образом, эталонный и проверяемый автоматы являются недетерминированными, и про-веряющие тесты должны строиться для недетерминированных автоматов отно-сительно отношения эквивалентности. Однако, в разделе 4.1 показывается (утверждение 4.1), что можно перейти от эталонного недетерминированного автомата с детерминированной функцией переходов А к детерминированному автомату Ал, при этом полный проверяющий тест, построенный для автомата Ал в классе неисправностей с ограничением на число состояний, будет являться полным и для автомата А. Это утверждение позволяет при построении проверяющего теста для композиций с кратным стимулированием А\ ХА2 использовать хорошо известные методы синтеза проверяющих тестов для детерминированных автоматов, например, метод Василевского (W метод) [24, 25] и его модификации [26-28].
В разделе 4.2 рассматривается композиция А\ 0 А2 - частный случай композиции с кратным стимулированием двух детерминированных автоматов А1 и А2, когда нас интересуют внешние выходы каждой из компонент независимо друг от друга, т. е. нас не интересует порядок выдаваемых системой символов в разных выходных каналах. Согласно утверждению 2.5, в этом случае поведение автоматной сети с кратным стимулированием из детерминированных автоматов описывается детерминированным автоматом. В связи с этим можно использовать те же модели неисправности, что и при построении проверяющих тестов для параллельной и синхронной композиции автоматов. В разделе 4.2.3 предлагается усовершенствованный метод синтеза проверяющих тестов для автоматной сети на основе мутационного автомата. Поскольку длина теста при использовании мутационного автомата существенно зависит от числа детерминированных переходов в этом автомате, то, в отличие от [35, 61], при синтезе тестов для автоматной сети используется не один, а несколько мутационных автоматов. После построения тестов для одного мутационного автомата остальные мутационные автоматы сокращаются. Из них удаляются подавтоматы, соответствующие неисправностям, которые обнаружимы уже построенным тестом. Подобно разделу 3.2, метод иллюстрируется для случая, когда неисправности возможны только в переходах компонент, которые «жестко» не зафиксированы в спецификации.
В разделе 4.2.4 задача синтеза проверяющего теста для компоненты автоматной сети решается на основе решения автоматных уравнений. В частности, отмечается, что при кратном стимулировании, так же как и в случае параллельной и синхронной композиции, можно построить недетерминированный автомат, описывающий допустимое поведение тестируемой компоненты [55]. Этот автомат называется сетевым эквивалентом тестируемой компоненты, и может быть построен на основе решения автоматного уравнения. В данном разделе также отмечается, что задача трансляции внутренних тестов на внешние полюсы сети может решаться для всех последовательностей теста одновременно на основе решения автоматных уравнений.
В разделе 4.3 рассматривается синтез тестов для композиции А10+\А2 (А\ 042 42), т. е. композиции с кратным стимулированием при отсутствии доступа ко входам и выходам компоненты А2 (А1). Согласно утверждению 2.6, автомат А10 \А2 (/41 0 2 А2) может быть наблюдаемым недетерминированным автоматом при детерминированных автоматах А1 и А2, и, поскольку отсутствует доступ ко входам второй компоненты, единственным отношением между проверяемой и эталонной композицией, которое можно гарантировать в процессе тестирования, является отношение неразделимости. Показывается (утверждение 4.3), что синтез полного проверяющего теста относительно такой модели неисправности нельзя свести к синтезу теста относительно отношений эквивалентности и редукции. Предлагается алгоритм построения разделяющей последовательности для заданных наблюдаемых автоматов А и В (если существует). Данный алгоритм дает возможность строить полные проверяющие тесты относительно неразделимости путем перебора автоматов из области неисправности.
