автореферат диссертации по информатике, вычислительной технике и управлению, 05.13.01, диссертация на тему:Синтез тестов для проверки взаимодействия дискретных управляющих систем методами теории автоматов

Томский государственный университет

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

Спицына Наталия Владимировна

СИНТЕЗ ТЕСТОВ ДЛЯ ПРОВЕРКИ ВЗАИМОДЕЙСТВИЯ ДИСКРЕТНЫХ УПРАВЛЯЮЩИХ СИСТЕМ МЕТОДАМИ ТЕОРИИ АВТОМАТОВ

Специальность 05.13.01 «Системный анализ, управление и обработка информации (в отраслях информатики, вычислительной техники и автоматизации)»

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

Томск-2005

Работа выполнена в Томском государственном университете.

Научный руководитель:

доктор технических наук, профессор

Евтушенко Нина Владимировна

Официальные оппоненты:

доктор технических наук, профессор

Матросова Анжела Юрьевна

кандидат физ.-мат. наук, научный сотрудник

Кулямин Виктор Вячеславович

Ведущая организация:

Томский политехнический университет

Защита состоится 7 апреля 2005 г в 12.30 на заседании диссертационного совета Д 212.267.12 при Томском государственном университете по адресу. 634050, г. Томск, пр. Ленина 36.

С диссертацией можно ознакомиться:

В научной библиотеке Томского государственного университета.

Автореферат разослан: «_» марта 2005 г.

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

д.т.н., профессор

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ

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

Поведение дискретных управляющих систем описывается при помощи формальных языков, а также таких моделей, как полуавтоматы (источники), сети Петри, автоматы и т д Моделью дискретной системы, относительно которой достаточно хорошо развиты методы построения проверяющих тестов, является модель с конечным числом переходов, которая в русскоязычной литературе называется конечным автоматом. Тестирование дискретных управляющих систем автоматными методами активно развивалось в работах Г. Бокмана, М П. Василевского, И.С. Грунского, Н.В Евтушенко, А. Кавалли, М Кима, В В Кулямина, Д. Ли, Б Д Лукьянова, А.Ю. Матросовой, А.Ф. Петренко, М. Янакакиса и других авторов.

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

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

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

гис. НАЦИОНАЛЬНА,

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

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

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

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

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

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

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

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

Реализация полученных результатов. Исследования, результаты которых изложены в диссертации, проводились, в частности, в рамках работ по программе «Университеты России», НИР «Алгебра конечных автоматов и полуавтоматов: отношения, операции, решение уравнений» (2002-2003 г.), а также в рамках международного проекта по исследованию и обучению методам тестирования TAROT (Training and Research on Testing, с 2004 г.) и по программе МОН РФ «Развитие научного потенциала высшей школы», НИР «Разработка методологии тестирования совместного функционирования телекоммуникационных протоколов на основе теории автоматов» (2005 г.). Кроме того, результаты исследований по тестированию таких дискретных систем, как сетевые протоколы, нашли свое применение при выполнении НИР «Лабораторные работы по курсу «Интернет-программирование» при поддержке ИДО ТГУ в рамках программы информатизации ТГУ. Разработанная система автоматизированного тестирования студенческих реализаций протоколов прикладного уровня внедрена в учебный процесс на радиофизическом факультете ТГУ.

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

Международная конференция «Компьютерные науки и информационные технологии», посвященная памя ги профессора А М. Богомолова, Саратов, 2002.

- Четвертая всероссийская конференция с международным участием «Новые информационные технологии в исследовании сложных структур», Томск, 2002.

- Девятая международная научно-практическая конференция студентов, аспирантов и молодых ученых «Современные техника и технологии», Томск, 2003

- Вторая сибирская научная школа-семинар с международным участием «Проблемы компьютерной безопасности и криптографии», посвященная 125-летию основания Томского государственного университета, Томск, 2003.

- 23rd IFIP WG 6 1 Inter. Confer. on Formal Techniques For Networked and Distributed Systems (FORTE), Berlin, Germany, 2003.

- Четвертая всероссийская конференция «Современные средства и системы автоматизации», Томск, 2003.

- Восьмой международный научный семинар «Дискретная математика и ее приложения», Москва, 2004.

- 16th IFIP International Conference on Testing of Communication Systems, Oxford, U.K., 2004.

Структура и объем диссертации. Диссертация состоит из введения, 5 глав, заключения и списка используемой литературы. Объем диссертации составляет 158 страниц текста, набранного в редакторе MS Word 2000 (Шрифт - Times New Roman, размер шрифта - 14 pt, межстрочный интервал - 1,5 строки), в том числе: титульный лист 1 стр , оглавление - 3 стр., основной текст, включающий 53 рисунка и 3 таблицы, - 141 стр, библиография из 78 наименований - 8 стр, приложение - 5 стр.

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

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

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

В параграфе 1.1 описываются модели дискретных систем, такие как полуавтоматы и автоматы Дискретную систему можно рассматривать как мемент, который характеризуется множесгвом полюсов. Каждому полюсу соответс гвует некоторый алфавит, т. е не пустое конечное множество символов; элементу также сопоставлен некоторый алфавит, который определяется на основе алфавитов полюсов элемента. Поведение элемента С описывается языком Ь в алфавите элемента С, т. е. множеством последовательностей конечной длины в заданном алфавите Несмотря на то, что алфавит элемента С конечен, язык элемента может быть бесконечным Существуют различные способы конечного задания бесконечного языка; наиболее известными из них являются грамматики и распознаватели К распознавателям относят, в частности, математические модели с конечным множеством состояний (памятью), такие, как полуавтоматы (источники), конечные автоматы.

Определение 1. Почуавтоматом (или источником) называется пятерка А - (5>, V, Т, л0, Г), где 5 - конечное множество состояний с выделенным начальным состоянием 50 и множеством Г финальных состояний, V - конечное множество действий, и Гс5х - отношение переходов. Языком полуавтомата А, обозначение: ЬА, называется множество последовательностей в алфавите V, получаемых при последовательных переходах из начального состояния в финальные состояния.

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

Определение 2. Недетерминированным (нд-) автоматом или просто автоматом А называется пятерка (5, X, У, И, .?0), где .V - множество состояний с выделенным начальным состоянием 5'0, X и К - соответственно входной и выходной алфавиты, /гс;5х^х5х У - отношение переходов-выходов Элементами множества И являются четверки вида (.у, х, 5', у), называемые переходами; при этом говорят,

что автомат может перейти из сос гояния 6 5 под действием входного символа х е X в состояние л' с 5 с выдачей выходного символа у е У, если четверка («, х, у) содержится в И. Переход из состояния л е нод действием входного символа х е X называется детерминированным, если ($, х, 5', у) е И и не существует другой пары (а", у'), такой что (5, х, я", у') е к.

Если для любых (5, х, у) е Я х X х У в нд-автомате существует не более одного перехода из состояния 5 под действием входного символа х с выходным символом у, то говорят, что нд-автомат является наблюдаемым. Если для каждой пары (5, х) е 5 х X существует хотя бы одна пара («', у) е Я х У, такая что (я, х, у) е И, то автомат называется полностью определенным, а в противном случае - частично определенным (или просто частичным). В полностью определенном автомате из любого состояния существует хотя бы один переход под действием любого входного символа, в то время как в частичном автомате такого перехода может не быть. Автомат называется хаосным, если/7=5хЛГх5х у.

Автомат называется детерминированным (д-автоматом), если для всех (5, х) е 5 х X отношение Ъ содержит не более одного перехода из .у под действием х, т. е. переход из любого состояния под действием любого входного символа в д-автомате является детерминированным.

Отношение переходов обычным образом распространяется на входные и выходные последовательности. Пара а / р называется входо-выходной последовательностью автомата в состоянии л-, если существует состояние 5' такое, что четверка (.?, а, 5', 0) е к. Множество вхо-до-выходных последовательностей в состоянии .? называется языком автомата в состоянии з, обозначение: ЬА(я). Язык автомата в начальном состоянии называется просто языком автомата и обозначается ЬА.

Говорят, что автомат А есть редукция автомата В (обозначение' А < В), если ¿л с: Автомат В квазиэквивалентен автомату А, если А и В - д-автоматы и А < В. Автоматы А и В эквивалентны (обозначение: А = В), если А < В и В <А. Если для любой входной последовательности, на которой определено поведение автоматов А и В, множества выходных последовательностей автоматов А и В пересекаются, то автоматы А и В называются неразделимыми (обозначение: А ~ В), в против-

8

ном случае автоматы А и В называются разделимыми (обозначение: А ф В).

Пусть А = (5, X, У, /г, л'0), В = (Т, X, V, g, г„). Автомат В называется подавтоматом автомата А, если Гс 0 = и £ с; /г, т. е. если каждый переход в автомате В может быть получен путем фиксирования соответствующего перехода в автомате А. Для заданного полностью определенного автомата А множество всех полностью определенных детерминированных подавтоматов автомата А обозначим 5иЬ(А).

Говорят, что состояние .$' достижимо в автомате А, если существует входная последовательность а, такая, что для некоторой выходной последовательности р четверка (.■?(,, «, У, р) е И Говорят, что состояние 5' детерминировано достижимо в автомате А, если в А существует последовательность, детерминировано переводящая автомат в состояние , т. е накрывающая только переходы, в которых однозначно определен переход в следующее состояние по данному входному символу.

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

Параграф 1.3 посвящен описанию особенностей тестирования взаимодействия дискретных систем.

Рис. Структура автоматной композиции

Если взаимодействующие дискретные системы (например, протоколы) были реализованы различными производителями, то возрастает вероятность того, что, а) реализации не мо1у1 функционировать совместно; б) совместное функционирование реализаций не соответствует спецификации. Причиной является тот факт, что в большинстве случа-

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

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

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

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

В параграфе 1.5 описываются задачи, решаемые в работе.

Для построения тестов с гарантированной полнотой необходимо формальное описание композиции взаимодействующих дискретных систем. Известных формальных операций композиции автоматов, введенных в работе Р Брайтона, В. Вонхама, В.М. Глушкова, Н.В. Евтушенко, А.Ф Петренко, Дж. Хартманиса и других авторов, вообще говоря, недостаточно для описания реальных систем, например, для описания поведения дискретных систем при одновременном внешнем воздействии на все компонент!,i системы, так называемом кратном стимулировании Такой режим взаимодействия, как отмечается в работе М. Кима, используется, в частности, при описании работы протокола TCP. Поэтому актуальной остается задача обобщения известных операций композиции для более сложных случаев. В работе вводится операция композиции, позволяющая формально описать функционирование дискретных систем, в том числе в режиме кратного стимулирования.

В работах Д. Ли, А. Кавалли, В Н. Тренькаева и других авторов, посвященных тестированию взаимодействующих конечных автоматов, в основном рассматривается синтез тестов для проверки функционирования бинарной параллельной или синхронной композиции. Авторы предполагают, что взаимодействующие автоматы согласованы, т. е. предполагается соответствие внешних алфавитов взаимодействующих систем, отсутствие несовместимостей при задании их параметров, отсутствие осцилляций при совместной работе и т. п Однако, такое предположение не соответствует действительности, т. к. проверка на осцилляции на этапе валидации (на этапе проверки корректности спецификации), описанная, в частности, в работе Дж. Хольцмана для таких дискретных управляющих систем, как протоколы, не всегда гарантирует, что при взаимодействии реализаций этих систем от разных производителей осцилляции не возникнет

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

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

11

рованных автоматов, на данный момент известны только методы построения тестов относительно эквивалентности и редукции, предложенные в работах Г. Бокмана, Н.В Евтушенко, И.Б. Куфаревой, А.Ф. Петренко и других авторов. При кратном стимулировании возникает необходимость проверки других отношений конформности, например, отношения неразделимости для недетерминированных автоматов. Поэтому в работе исследуется отношение неразделимости между недетерминированными автоматами. »

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

Структура композиции задается при помощи разбиения к, в котором отождествленные полюсы компонент объединены в классы, | ж \ = А. Множество в содержит внешние полюсы системы, 0 с; ж Для задания режима функционирования вводится булева матрица несовместности Мкхк Элемент М, у на пересечении /-й строки и у'-го столбца равен 1, если на полюсах из Ь,-го и Л,-го классов разбиения л не может быть одновременно значащих символов.

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

1) Описать временное «не участие» компоненты в работе композиции (преобразовать язык каждой компоненты в ^замкнутый язык где V— специальный «молчащий» символ)

2) Описать поведение компоненты как части композиции (преобразо-

вать язык каждой компоненты в язык Ехр^ЬГ), учитывая структуру композиции и режим ее функционирования)

3) Описать совместное поведение компонент композиции (построить

пересечение полученных языков компонент)

4) Описать внешнее (наблюдаемое) поведение композиции (взять проекцию на внешние полюсы композиции).

Язык Сотрл о Л/£ь •.,£*) = [ЕхрК м^Г) п .. .п ЕхрК «(¿Л] 1в описывает поведение обобщенной композиции элементов, поведение кото-

рых задано языками ¿ь ..., Ln (для заданной структуры композиции % множества внешних полюсов в и матрицы несовместимости М).

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

Largest = Сотр„ рМ{Ц,... JL^, I)

Теорема 1. Если Сотрх 0m(L], ..Largest) = L , то Largest -наибольшее решение уравнения Сотркв ^(1,,. = L. Иначе

уравнение не имеет решения

В работах Г. Бокмана, Н.В. Евтушенко, А.Ф Петренко показано, как описание максимально допустимого поведения компоненты композиции может быть использовано при синтезе тестов.

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

В параграфе 2.3 исследуется возможность распространения введенной операции композиции на случай, когда поведение дискретных систем описывается конечными автоматами. Показывается, что в общем случае распространить операцию композиции так, чтобы результатом композиции был автомат, не удается. Поэтому для автоматов обсуждаются необходимые ограничения на композицию. В частности, при композиции автоматов не разрешается отождествлять выходные полюсы различных автоматов. Кроме того, для того, чтобы остаться в классе автоматных языков, между автоматами - элементами композиции в некоторых случаях приходится вводить буферы, в которых «запасаются» поступившие входные символы. Таким образом, для описания взаимодействия двух автоматов при кратном стимулировании рассматривается композиция из четырех элементов, два из которых являются входными буферами. Дополнительным ограничением обычно является так называемая «медленная» внешняя среда, когда следующий входной сигнал на композицию автоматов может быть подан только после того, как все внутренние каналы становятся пустыми. Такая композиция

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

При взаимодействии автоматов могут возникать бесконечные диалоги, или осцилляции. При построении композиции для описания такой ситуации в автомат композиции добавляется специальное состояние ОСЦИЛЛЯЦИЯ, в которое и определяется всякий переход, по которому возникает осцилляция.

Обозначим композицию с кратным стимулированием автоматов А1 = (£>, X и V, Ух и, И, Яо) и А2 = (Г, / и С/, О х V, g, 10) А1 0хЛ2 = (5,Хх /, (Ух 0)к, Я, <7в/0), где

5с(0х Т и {ОСЦИЛЛЯЦИЯ}).

В параграфе 2 4.4 установливаются некоторые свойства композиции с кратным стимулированием автоматов А1 и А2 (структура композиции представлена на рис. 1).

Утверждение 1. Если автоматы А\ и А1 детерминированные, то композиция А1 0Д А2 будет наблюдаемым недетерминированным автоматом с детерминированной функцией переходов.

Если не важен порядок появления выходных символов на различных внешних полюсах, то обозначим композицию с кратным стимулированием автоматов А\ и А2 А\ О0 А2 = (5,Хх /, У* х О1, II, д0/Д 5с(2х Т и {ОСЦИЛЛЯЦИЯ}).

Утверждение 2. Если автоматы А\ и А2 детерминированные, то композиция А\ 0® А2 будет детерминированным автоматом.

При возможности доступа только к Л1 или только к /42:

- если доступен для управления и наблюдения автомат А\, то обозначим композицию с кратным стимулированием АЮ,1А2 = (Ясвх Т,Х,У*,Н,Яо1„)

- если доступен для управления и наблюдения автомат Л2, то обозначим композицию с кратным стимулированием А\О,3Л2 = (5с0х Т,1,0>,Н,йо1о)

Утверждение 3. Недетерминированный автомат Л 10^/42 (А 1 0,2 А2) может име1ь недетерминированную функцию переходов при детерминированных автоматах А1 и А2.

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

Третья глава посвящена проверке взаимодействующих дискретных систем на отсутствие осцилляций. В данной главе рассматривается бинарная композиция автоматов А\ и А2 с кратным стимулированием, структура которой представлена на рис. 1. Все полученные результаты иллюстрируются для случая, когда не важна очередность появления действий в различных внешних выходных каналах композиции, т. е. для композиции А1 0® А2. Бинарная параллельная композиция является частным случаем композиции с кратным стимулированием, т. е. все результаты этой главы применимы и для параллельной композиции.

Как было отмечено в разделе 1.4, для построения тестов с гарантированной полнотой необходимо ввести модель неисправности. В работе вводится модель неисправности < 91, отсутствие осцилляций >, где 91- множество композиций возможных реализаций автоматов А\ и А2 (раздел 3.1). В этом же разделе обсуждается возможность использования мутационного авюмата для компактного задания множества неисправных композиций.

Множество подавтоматов мутационного автомата определяет множество проверяемых композиций. Выбор мутационного автомата, т. е. выбор класса неисправностей, является достаточно сложной задачей. В данной работе полученные результаты иллюстрируются для класса возможных ошибок, основанного на частичном описании спецификации, что имеет место, в частности, для сетевых протоколов. В разделе 3.2 описывается построение мутационного автомата для такого класса ошибок, и рассматривается пример протокола АТМ/В-^ЭЫ, спецификация которого является частичной, и некоторые ее доопределения приводят к возникновению осцилляций.

В работе предлагается метод построения полных проверяющих тестов относительно модели неисправности < 91, отсутствие осцилляций > для композиции А1 0® А2. Согласно утверждению 2, поведение эталон-

ной и проверяемой композиций описывается детерминированными автоматами Проверяющий тест определяется как множество входных последовательностей. Тест называется полным относительно модели неисправности < 9?, отсутствие осцилляции >, если тест обнаруживает любую композицию из множества 91, в которой возможна осцилляция. Т. к. осцилляции первого и второго рода обнаруживаются обычно посредством таймера, то для любой системы, в которой возможна осцилляция, полный проверяющий тест должен содержать входную последовательность, которая «накрывает» соответствующий переход в композиции. В разделе 3.3 обсуждаются особенности тестирования относительно осцилляций. В разделе 3.4 предлагается метод построения безусловного полного проверяющего теста, и метод построения проверяющего теста при проведении условного эксперимента с проверяемой системой относительно осцилляций

В разделе 3.5 приводятся результаты компьютерных экспериментов. Проведенные компьютерные эксперименты показали, что при наличии неопределенных переходов в спецификациях порядка 10% и выше практически всегда возможны такие их доопределения при реализации, которые приводят к возникновению осцилляций при взаимодействии реализаций. Длина проверяющего теста на осцилляции также существенно зависит от количества неопределенных переходов в спецификациях. В частности, если неопределенных переходов в спецификации порядка 4-6%, то в большинстве мутационных автоматов (90-95%) все состояния, из которых есть переход в состояние ОСЦИЛЛЯЦИЯ, детерминировано достижимы, в результате чего тесты будут достаточно короткими.

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

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

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

В разделе 4.1 рассматривается композиция А \ О* А2 с кратным стимулированием двух детерминированных автоматов А\ и А2 Автомат композиции, согласно утверждению 1, является наблюдаемым недетерминированным автоматом с детерминированной функцией переходов. Таким образом, эталонный и проверяемый автоматы являются недетерминированными, и проверяющие тесты должны строиться для недетерминированных автоматов относительно отношения эквивалентности. Однако, в разделе 4.1 показывается, что можно перейти от эталонного недетерминированного автомата с детерминированной функцией переходов А к детерминированному автомату А", при этом полный проверяющий тест, построенный для автомата Аа в классе неисправностей с офаничением на число состояний, будет являться полным и для автомата А, т. е. справедливо следующее утверждение

Утверждение 4. Полный проверяющий тест относительно модели <А\~, ¡Пта> является полным проверяющим тестом относительно модели <А,=, !Ят>.

Эю утверждение позволяет при построении проверяющего теста для композиций с кратным стимулированием А1 0Х А2 использовать хорошо известные методы синтеза проверяющих тестов для детерминированных автоматов, например, метод Василевского и и о модификации.

В разделе 4.2 рассматривается композиция А{ О® А2 - частный случай композиции с кратным стимулированием двух детерминированных автомагов А\ и А2, когда не важен порядок выдаваемых системой символов в разных выходных каналах Согласно утверждению 2, в этом

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

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

В разделе 4 3 рассматривается синтез тестов для композиции А 10,|Л2 (А1 0,2 А2), т. е композиции с кратным стимулированием при отсутствии доступа ко входам и выходам компоненты А2 (А 1). Согласно утверждению 3, автомат А10 ,, А2 (/Л 0,2 А2) может быть наблюдаемым недетерминированным автоматом при детерминированных автоматах А1 и А2, и, поскольку отсутствует доступ ко входам второй компоненты, единственным отношением между проверяемой и эталонной композицией, которое можно гарантировать в процессе тести-

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

Утверждение 5. Проверяющий тест, полный относительно отношения эквивалентности (или редукции) и области неисправности 91, не является полным относительно неразделимости

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

Утверждение 6. Существуют наблюдаемый автомат А с п состояниями и В с т состояниями, для которых кратчайшая разделяющая последовательность имеет длину больше тп

Предлагается алгоритм построения разделяющей последовательности для заданных наблюдаемых автоматов А и В (если существует). Данный алгоритм дает возможность строить полные проверяющие тесты относительно неразделимости путем перебора автоматов из области неисправности.

В пятой главе описывается система автоматизированного тестирования студенческих реализаций протоколов прикладного уровня. В параграфе 5 1 приводится краткое описание лабораторных работ, предлагаемых для выполнения по курсу «Интернет-программирование». В параграфах 5 2 и 5 3 вводится классификация наиболее вероятных ошибок, которые могут быть свойственны либо реализации только данного протокола, либо реализации любого протокола прикладного уровня, предлагаются тестовые последовательности, гарантирующие обнаружение и/или локализацию таких ошибок В параграфе 5.4 описывается подход к автоматизации процесса тестирования студенческих реализаций протоколов, который был реализован при выполнении проекта «Лабораторные работы по курсу «Интернет-

программирование» при поддержке ИДО ТГУ в рамках программы информатизации ТГУ.

Заключение

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

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

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

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

2 Модель неисправности для проверки композиции автоматов на отсутствие осцилляции, и метод построения полных проверяющих тестов относительно этой модели

3 Алгоритмы синтеза полных проверяющих тестов для композиции конечных автоматов с кратным стимулированием при различных условиях доступа к каналам композиции.

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

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

ПУБЛИКАЦИИ ПО ТЕМЕ ДИССЕРТАЦИИ

1 Евтушенко Н В , Спицына Н В Синтез полуавтоматов посредством решения логических уравнений // Материалы международной конференции «Компьютерные науки и информационные технологии», посвященной памяти профессора А. М. Богомолова. - Саратов, 2002. - С. 26.

2 Спицына НВ , Евтушенко Н В , Петренко А Ф Решение уравнений в алгебре полуавтоматов для операции обобщенной композиции // Вестник ТГУ. Приложение. 2002. № 1(11). С. 265-270.

3 Спицына Н В , Шабалдин А В Интернет-программирование. Лабораторные работы Часть 1 ■ Методическое пособие. - Томск- Изд-во ТГУ, 2002. - 50 с.

4 N Spilsyna Interaction Testing' Introducing Class of Failures by the Example of the Protocol POP3 // Proceedings of the 9th International Scientific and Practical Conference of Students, Post-graduates and Young Scientists on Modern Techniques and Technologies. - Tomsk Polytechnic University, 2003 - P. 214-216.

5 Спицына HВ Этапы тестирования на взаимодействие // Материалы Международной конференции «Современные проблемы физики и высокие технологии». - Томск- Изд-во НТЛ, 2003 - С. 500-502

6. Спицына Н В , Шабачдин А В Тестирование программных реализаций протоколов в лабораторном практикуме // Материалы Всероссий-

21

ской конференции «Инфокоммуникационные и вычислительные технологии и системы». - Улан-Удэ: Издательство Бурятского госуниверситета, 2003. - С. 78-81.

7. Спицына H В , Тренькаев В H К синтезу тестов для композиции конечных автоматов // Вестник ТГУ Приложение Серия «Математика. Кибернетика. Информатика». 2003. №6 С. 183-187

8. N Spitsyna, V Trenkaev, Kh El-Fakih, N Yevtushenko. FSM Based Interoperability Testing: Work in Progress // Proceedings of the Work in Progress Session of 23rd IFÏP WG 6.1. Inter Confer. on Formal Techniques for Networked and Distributed Systems, 2003 - P. 29-38.

9. N Spitsyna, V Trenkaev. FSM Based Interoperability Testing of Communication Protocols // Proceedings of the IEEE-Siberian Conference on Control and Communications, 2003. - P. 20-23.

10. Шабалдин А В , Спицына H В , КоломеецА.В Автоматизация тестирования реализаций протоколов прикладного уровня в лабораторном практикуме // Материалы четвертой научно-практической конференции «Современные средства и системы автоматизации». - Томск: Изд-во ТУСУР, 2004. - С. 222-225.

11 К El-Fakih, V Trenkaev, N Spitsyna, N Yevtushenko. FSM Based Interoperability Testing Methods // Lecture notes in Computer Science 2978, 2004.-P. 60-75.

12 Спицына H В , Евтушенко H В Трансляция тестов для компоненты автоматной сети посредством решения автоматных уравнений // Материалы пятой международной конференции «Автоматизация проектирования дискретных систем» - Минск: НАН Беларуси, 2004. - Т. 2 - С. 96-103.

13 Спицына H В , Евтушенко H В Синтез условных проверяющих тестов для недетерминированных автоматов // Материалы VIII Международного семинара «Дискретная математика и ее приложения». - М.: Изд-во механико-математического факультета МГУ, 2004. - С. 310313.

п

2-3 8 1 ^

РНБ Русский фонд

2006-4 7231

Размножено 100 экз. Копировальный центр «Южный», г.Томск, ул. 19-й Гвардейской дивизии, 75 тел. 41-34-47

ВВЕДЕНИЕ.

1. ОСНОВНЫЕ ПОНЯТИЯ, ПОСТАНОВКА ЗАДАЧИ И ОБЗОР ЛИТЕРАТУРЫ.

1.1. Модели дискретных систем.

1.2. Представление сетевых протоколов при помощи конечных автоматов

1.3. Особенности проверки взаимодействия дискретных систем.

1.4. Модели неисправности и проверяющие тесты.

1.5. Описание задач, решаемых в работе.30,

1.6. Обзор существующих методов.

1.6.1. Известные операции композиций дискретных систем, решение языковых и автоматных уравнений.

1.6.2. Обзор методов построения тестов для проверки взаимодействия дискретных систем.

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

2. КОМПОЗИЦИЯ ЯЗЫКОВ, ПОЛУАВТОМАТОВ И АВТОМАТОВ.

2.1. Обобщенная композиция элементов, поведение которых описано формальными языками.

2.1.1. Элементы и системы взаимодействующих элементов.

2.1.2. Построение языка, описывающего поведение системы взаимодействующих элементов.

2.1.3. Построение языка, описывающего поведение неизвестного элемента в системе.

2.2. Обобщенная композиция полуавтоматов.

2.2.1. Описание системы взаимодействующих полуавтоматов.

2.2.2. Нахождение неизвестного полуавтомата в системе взаимодействующих полуавтоматов.

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

2.4. Частные случаи композиции автоматов.

2.4.1. Синхронная композиция автоматов.

2.4.2. Параллельная композиция автоматов.

2.4.3. Бинарная композиция с кратным стимулированием.

2.4.4. Некоторые свойства бинарной композиции с кратным стимулированием

2.4.5. Нахождение неизвестного автомата в системе взаимодействующих автоматов.

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

3. ТЕСТИРОВАНИЕ ОТНОСИТЕЛЬНО ОСЦИЛЛЯЦИЙ.

3.1. Модель неисправности для тестирования относительно осцилляций.

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

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

3.4. Метод построения проверяющих тестов на отсутствие осцилляций по Щ мутационному автомату.

3.4.1. Построение полного проверяющего теста на основе безусловного тестирования.

3.4.2. Построение полного проверяющего теста на основе условного тестирования.

3.5. Экспериментальные результаты.

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

4. МОДЕЛИ НЕИСПРАВНОСТИ И СИНТЕЗ ТЕСТОВ ДЛЯ ПРОВЕРКИ ФУНКЦИОНИРОВАНИЯ ВЗАИМОДЕЙСТВУЮЩИХ АВТОМАТОВ ПРИ КРАТНОМ СТИМУЛИРОВАНИИ.

4.1. Синтез тестов для композиции А1 0ХЛ2.

4.2. Синтез тестов для композиции А1 0®Л2.

4.2.1. Полный проверяющий тест при использовании мутационного автомата

4.2.2. Модель неисправности при тестировании композиции А \ 0®А2.

4.2.3. Алгоритм построения полного проверяющего теста.

4.2.4. Построение тестов для компонент сети на основе решения автоматных уравнений.

4.3. Синтез тестов для удаленной компоненты.

4.3.1. Построение тестов для композиций А1 А2 (Л1 0*2-<42).

4.3.2. Исследование отношения неразделимости.

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

5. ТЕСТИРОВАНИЕ ПРОГРАММНЫХ РЕАЛИЗАЦИЙ ПРОТОКОЛОВ В ЛАБОРАТОРНОМ ПРАКТИКУМЕ.

5.1. Краткое описание предлагаемых лабораторных работ.

5.2. Ошибки, типичные при реализации любого протокола прикладного уровня.

5.3. Возможные ошибки при реализации конкретного протокола прикладного уровня.

5.3.1. Возможные ошибки при реализации протокола РОРЗ.

5.3.2. Возможные ошибки при реализации протокола SMTP.

5.3.3. Возможные ошибки при реализации протокола TFTP.

5.3.4. Возможные ошибки при реализации протокола TIME.

5.3.5. Возможные ошибки при реализации протокола HTTP.

5.4. Автоматизация тестирования студенческих реализаций протоколов

5.4.1. Постановка задачи автоматизации тестирования.

5.4.2. Архитектура тестера.

5.4.3. Пример тестирования РОРЗ-сервера.

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

Общая характеристика Актуальность проблемы. Под дискретной системой в работе понимается система, поведение которой описывается последовательностями действий в некотором алфавите. Поведение управляющих дискретных систем описывается при помощи формальных языков, а также таких моделей, как полуавтоматы (источники), сети Петри, автоматы и т. д. [1-11]. Примерами взаимодействующих дискретных систем являются интегральные схемы [5], аппаратные и программные реализации сетевых протоколов [8, 11], мультиагентные системы [13]. При этом системы могут быть соединены между собой различными способами, и режимы их совместного функционирования также могут быть различными. Совместная работа дискретных систем проверяется путем подачи на вход системы проверяющих тестов - последовательностей входных воздействий, и наблюдения выходных реакций системы с последующим их анализом [1, 3, 6]. Моделью дискретной системы, относительно которой достаточно хорошо развиты методы построения проверяющих тестов, является модель с конечным числом переходов, которая в русскоязычной литературе называется конечным автоматом. Тестирование дискретных управляющих систем автоматными методами активно развивалось в работах Г. Бокмана, М.П. Василевского, И.С. Грунского, Н.В. Евтушенко, А. Кавалли, М. Кима, В.В. Кулямина, Д. Ли, Б.Д. Лукьянова, А.Ю. Матросовой, А.Ф. Петренко, М. Янакакиса и других авторов.

Взаимодействующие дискретные управляющие системы могут быть соединены между собой различными способами, и режимы их совместного функционирования также могут быть разными. Методы построения тестов существенно зависят от режима взаимодействия дискретных систем. Известных формальных операций композиции автоматов [2, 40-42], вообще говоря, недостаточно для описания реальных систем, например, для описания поведения дискретных систем при кратном стимулировании, когда входные сигналы могут поступать на компоненты композиции как одновременно, так и поочередно [36]. Поэтому актуальной остается задача обобщения известных операций композиции для более сложных случаев.

Большинство публикаций по тестированию взаимодействующих конечных автоматов посвящено синтезу тестов для проверки функционирования некоторых видов автоматных композиций, особенно для бинарной параллельной или синхронной композиции [15, 17-20, 22, 63]. Авторы предполагают, что взаимодействующие автоматы согласованы, т. е. предполагается соответствие внешних алфавитов взаимодействующих систем, отсутствие несовместимостей при задании их параметров, отсутствие осцилляций при совместной работе и т. п. [15]. Однако, такое предположение не соответствует действительности, т. к. проверка на тупики и осцилляции на этапе валидации [21], т. е. на этапе проверки корректности спецификации, например, таких дискретных управляющих систем, как протоколы, не всегда гарантирует, что при взаимодействии реализаций этих систем от разных производителей осцилляций не возникнет. Поэтому в последнее время появились работы [16], в которых предлагаются методы синтеза тестов только для проверки, могут ли системы функционировать совместно. Тестьг для двух этапов строятся независимо друг от друга, т. к. неизвестна связь между этими тестами. В известных нам работах тесты для проверки совместимости систем строятся эвристически без математической модели [15-20]. Таким образом, актуальной является задача разработки технологии тестирования взаимодействующих автоматов, включающей в себя тестирование на возможность совместного функционирования, для более сложных режимов совместного функционирования, в частности для режима кратного стимулирования.

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

Для достижения поставленной цели решаются следующие задачи.

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

2. Разработка модели неисправности и метода синтеза полных проверяющих тестов для проверки дискретных систем на совместимость (отсутствие осцилля-ций при взаимодействии).

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

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

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

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

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

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

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

Реализация полученных результатов. Исследования, результаты которых изложены в диссертации, проводились в рамках работ по программе «Университеты России» (2002-2003 г.), НИР «Алгебра конечных автоматов и полуавтоматов: отношения, операции, решение уравнений», а также в рамках международного проекта по исследованию и обучению методам тестирования TAROT (Training and Research on Testing, с 2004 г.) и по программе МОН РФ «Развитие научного потенциала высшей школы» (2005 г.), НИР «Разработка методологии тестирования совместного функционирования телекоммуникационных протоколов на основе теории автоматов». Кроме того, результаты исследований по тестированию сетевых протоколов нашли применение при выполнении НИР «Лабораторные работы по курсу «Интернет-программирование» при поддержке

ИДО ТГУ в рамках программы информатизации ТГУ. Разработанная система автоматизированного тестирования студенческих реализаций протоколов прикладного уровня внедрена в учебный процесс на радиофизическом факультете ТГУ.

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

Апробация работы. Научные результаты [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 стр. Основное содержание работы

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

В данной главе рассматривается задача тестирования реализаций протоколов в лабораторном практикуме. Вводится классификация наиболее вероятных ошибок, которые могут быть свойственны либо реализации только данного протокола, либо реализации любого протокола прикладного уровня, предлагаются тестовые последовательности, гарантирующие обнаружение и/или локализацию таких ошибок, а также описывается подход к автоматизации процесса тестирования студенческих реализаций протокола, который был реализован при выполнении проекта «Лабораторные работы по курсу Интернет-программирование» при поддержке ИДО ТГУ в рамках программы информатизации ТГУ.

Заключение

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

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

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

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

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

3. Алгоритмы синтеза полных проверяющих тестов для композиции конечных автоматов с кратным стимулированием при различных условиях доступа к каналам композиции.

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

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

1. Мур Э. Ф. Умозрительные эксперименты с последовательными машинами // Автоматы. -М.: Изд-во иностр. лит., 1956. С. 179-210.

2. Глушков В. М. Синтез цифровых автоматов. М: Физматгиз,1962. - 476 с.

3. Гилл А. Введение в теорию конечных автоматов. М: Наука, 1966. - 272 с.

4. Трахтенброт Б. А., Барздинь Я. М. Конечные автоматы (поведение и синтез). М.: Наука, 1970. - 400 с.

5. Агибалов Г. П., ОрановА. М. Лекции по теории конечных автоматов. — Томск: Изд-во Томского госуниверситета, 1984. 184 с.

6. Богомолов А. М., Грунский И. С., Сперанский Д. В. Контроль и преобразования дискретных автоматов. Киев: Наук, думка, 1975. - 176 с.

7. Матросова А. Ю. Алгоритмические методы синтеза тестов. Томск: Изд-во Томского госуниверситета, 1990. - 207 с.

8. Грунский И. С., Петренко А. Ф. Построение проверяющих экспериментов с автоматами, описывающими протоколы // Автоматика и Вычислительная техника. 1988. - № 4. - С. 7-14.

9. Бурдонов И. Б., Косачев А. С., Кулямин В. В. Использование конечных автоматов для тестирования программ // Программирование. 2000. - №2. - С. 1228.

10. Hartmanis J., Stearns R. Algebraic Structure Theory of Sequential Machines. — Printice-Hall, New-York, 1966. 210 p.

11. Карпов Ю. Г. Теория автоматов. СПб.: Питер, 2003. - 208 с.

12. Лукьянов Б. Д. О различающих и контрольных экспериментах с недетерминированными автоматами // Кибернетика и системный анализ. 1995. - №5. — С. 69-76.

13. A. Haddadi. Communication and Cooperation in Agent Systems: A Pragmatic Theory // Lecture Notes in Computer Science, 1056, Springer-Verlag, 1996.

14. Wonham W. M. Supervision of DES // www.control.utoronto.ca/des, 1999. 324 P

15. C. Viho, S. Barbin, L. Tanguy. Towards a formal framework for interoperability testing // Proceedings of the 21st Inter. Conf. FORTE 2001, Korea. P. 51-68.

16. Yannakakis M., Lee D. Testing finite state machines // AT&T Bell Labs, internal memorandum, 1990.

17. N. Griffeth, R. Hao, D. Lee, R. Sinha. Interoperability testing of VoIP Systems // Proceedings of the Global Telecommunications Conference, 2000, GLOBECOM'OO, IEEE, Vol.3. P. 1565-1570.

18. D.Lee, K. Sabnani, D. Kristol, S. Paul. Conformance testing of protocols specified as communicating finite state machines a guided random walk based approach // In IEEE Transactions on Communications, vol. 44, N 5, 1996. - P. 631-640.

19. Kang D., Kang S., Kim M., Yoo S. A weighted random walk approach for conformance testing of system specified as communicating finite state machines // Proceedings of the Inter. Conf. FORTE X /PSTV XVII, 1997. P. 267-282.

20. Cavalli A., Lee D., Rinderknecht C., Zaidi F. Hit-or-jump: an algorithm for embedded testing with application to IN services // Proceedings of the IFIP Joint Inter. Conf. FORTE/PSVT, 1999. P. 41-56.

21. Gerard J. Holzmann. Design and validation of computer protocols // Prentice-Hall, Englewood Cliffs, 1991.

22. J. Farrell. IP Fragmentation Attacks on Checkpoint Firewalls // http://www.sans.org/rr/firewall/fragattacks.php, 2001.

23. Василевский M. П. О распознавании неисправности автоматов // Кибернетика. 1973. - №4. - С. 98-108.

24. Т. S. Chow. Test design modeled by finite-state machines I I IEEE Trans. SE, vol. 4, no. 3, 1978.-P. 178-187.

25. S. Fujiwara, G. v. Bochmann, F. Khendek, M. Amalou, and A. Ghedamsi. Test selection based on finite state models // IEEE Trans. SE, vol. 17, no. 6, 1991. P. 591-603.

26. A. Petrenko, N. Yevtushenko, A. Lebedev, and A. Das. Nondeterministic state machines in protocol conformance testing // Proc. of the IFIP 6th IWPTS, France, 1993.-P. 363-378.

27. N. Yevtushenko, A. Petrenko. Test derivation method for an arbitrary deterministic automaton // Automatic Control and Computer Sciences, Allerton Press Inc., USA, no. 5,1990.

28. F. C. Hennie. Fault detecting experiments for sequential circuits // Proc. of 5th Annual Symposium on Switching Circuit Theory and Logical Design, Princeton, 1964. — P. 95-110.

29. КуфареваИ. Б., Дорофеева M. Ю. Минимизация проверяющих тестов для конечных автоматов. //ВестникТГУ. Приложение. 2002. № 1 (II). С. 357-362.

30. S. Т. Vuong, W. W. L. Chan, and М. R. Ito. The UlOv-method for protocol test sequence generation // Proc. of the IFIP TC6 2nd IWPTS, North-Holland, 1989. P. 161-175.

31. B. Yang, H. Ural. Protocol conformance test generation using multiple UIO sequences with overlapping // Computer Communication Review, No. 4, 1990. P. 118-125.

32. LuoG., Petrenko A., Bochmanv.G. Selecting test sequences for partiallythspecified nondeterministic state machines // Proceedings of IFIP 6 International Workshop on Protocol Test Systems, 1995. P. 95-110.

33. A. Petrenko, N. Yevtushenko, G. V. Bochmann. Testing deterministic implementations from their nondeterministic specifications // Proceedings of the IFIP Ninth International Workshop on Testing of Communication Systems, Germany, 1996. P. 125-140.

34. Куфарева И. Б. Применение недетерминированных автоматов в задачах синтеза проверяющих тестов для систем логического управления: Диссертация на соискания ученой степени канд. технических наук. — Томск, 2000. — 176 с.

35. Seol S., Kim М., Chanson S. Т. Interoperability Test Generation for Communication Protocols based on Multiple Stimuli Principle // Proceedings of the IFIP 14th Inter. Conf. TestCom2002. P. 151-169.

36. P. Starke. Abstract automata, North-Holland / American Elsevier, 1972. 419 p.

37. Rose M. Post Office Protocol Version 3. RFC 1460, June 1993. // http://www.faqs.org/rfcs/rfcl460.html.

38. Евтушенко H. В., Куфарева И. Б. Отношения между недетерминированными автоматами. Томск: Изд-во Института оптики атмосферы СО РАН, 2001. -26 с.

39. Т. Kim, Т. Villa, R. Brayton, A. Sangiovanni-Vincentelli. Synthesis of FSMs: -functional optimization. Kluwer Academic Publishers, 1997.

40. H. Евтушенко, Т. Вилла, А.Петренко, Р.Брайтон, А. Санджованни- ' Винцентелли. Решение уравнений в логическом синтезе // Препринт, Томск: Изд-во «Спектр», 1999. 27 с.

41. Yevtushenko N., Villa Т., Brayton R., Petrenko A., Sangiovani-Vincentelli A. Solution of synchronous language equations for logic synthesis // Вестник ТГУ. Приложение. 2002. № 1(11). С. 132-137.

42. P. Merlin and G. Bochmann. On the construction of submodule specifications and communication protocols // ACM Transactions on Programming Language and Systems, 5(1): 1-25, January 1983.

43. H. Qin, P. Lewis. Factorisation of Finite State Machines under strong and observational equivalences // Formal Aspects of Computing, 3:284-307, Jul.-Sept. 1991.

44. A. Petrenko, N. Yevtushenko. Solving asuynchronous equations. // Formal desrip-tion techniques/Protocol specification, testing and verification. Kluwer Academic Publishers, 1998.-P. 125-140.

45. A. Petrenko,N. Yevtushenko, G. v. Bochmann. Fault models for testing in context // Proceedings of the IFIP 1st Joint International Conference FORTE/PSTV, Chapman & Hall, 1996.-P. 163-178.

46. N. Yevtushenko, T. Villa, R. Brayton, A. Petrenko, A. Sangiovanni-Vincentelli. Sequential Synthesis by Language Equation Solving // Technical report, 2003.

47. S. Hassoun, T. Villa. Optimization of synchronous circuits. // In R. Brayton, S. Hassoun, andT. Sasao, editors, Logic Synthesis and Verification, 2001. P. 225-253.

48. С. H. West. An automated technique of communication protocols validation // IEEE Trans. Comm., 26 (1978) 1271-1275.

49. D. Brand and P. Zafiropulo. On communicating finite state machines // J. ACM 30(2), (1983) 323-342.

50. G. v. Bochmann, C. A. Sunshine. Formal methods in communication protocol design // IEEE Trans, on Comm., Vol 28, 1980. P. 624-631.

51. Cavalli A., Prokopenko S., Yevtushenko N. Fault detection power of a widely used test suite for a system of communicating FSMs // Proceedings of the IFIP 13th Inter. Conf. TestCom2000. P. 35-59.

52. S. Naito, M. Tsunoyama. Fault detection for sequential machines by transition tours // Proceedings of Fault Tolerant Comp, Syst., 1981. P.23 8-243.

53. Watanabe Y., Brayton R. K. The maximum set of permissible behaviors for FSMS network // Trans. Of IEEE / ACM Int. Conf. On Compute-aided design, 1993. -P. 316-328.

54. Евтушенко H. В., Петренко А. Ф., Тренькаев В. H. Метод тестирования автоматных сетей, основанный на тестируемом поведении компоненты // Автоматика и вычислительная техника. 1996. - № 2. - С. 48-59.

55. К. El-Fakih, N. Yevtushenko. Fault Propagation by Equation Solving // Proceedings of the 24th IFIP WG 6.1. Inter. Confer. Formal Techniques For Networked and Distributed Systems, FORTE 2004. P. 185-198.

56. R. M. Hieron, Adaptive Testing of a deterministic implementation against a non-deterministic finite state machines // The computer journal, v.41, 1998. P. 349-355.

57. Hopcroft J. E., UlmanJ. D. Introduction to automata theory, Languages and Computation // Addison-Wesley Publishing Company, 1979.

58. Буфалов С. А. Исследование живых и безопасных решений параллельных уравнений и неравенств на множестве полуавтоматов и автоматов: Диссертация на соискание ученой степени кандидата тех. наук, 2002.

59. Koufareva, A. Petrenko, N. Yevtushenko. Test generation driven by user-defined fault models // Testing of Communicating Systems: Methods and Applications. Kluwer Academic Publishers, 1999. - P. 215-233.

60. Евтушенко H. В., Тренькаев В. H. Методы синтеза тестов для цифровых автоматов: Учебно-методическое пособие. Томск: Изд-во ТГУ, 1997. - 34 с.

61. Тренькаев В. Н. Разработка методов синтеза проверяющих тестов для сетей из конечных автоматов: Диссертация на соискание ученой степени кандидата тех. наук, 2000. 188 с.

62. К. El-Fakih, N. Yevtushenko and G. Bochmann. Protocol re-testing methods // Proc. of the IFIP 14th International Conference on Testing of Communicating Systems, 2002.

63. K. El-Fakih, N. Yevtushenko, and G. v. Bochmann. FSM-based incremental conformance testing methods // IEEE Transactions on software engineering, 2004, v.20, N7.-P. 425-436.

64. Дорофеева М. Ю., ЕвтушенкоН. В. Усовершенствование метода синтеза проверяющих тестов по мутационному автомату // Вестник ТГУ. Приложение. Серия «Математика. Кибернетика. Информатика». 2003. № 6. С. 164—169.

65. Евтушенко Н. В., СпицынаН. В. Синтез полуавтоматов посредством решения логических уравнений // Материалы международной конференции, посвященной памяти профессора A.M. Богомолова. Саратов, 2002. - С.26.

66. Спицына Н. В., Евтушенко Н. В., Петренко А. Ф. Решение уравнений в алгебре полуавтоматов для операции обобщенной композиции // Вестник ТГУ. Приложение. 2002. № 1(11). С. 265-270.

67. СпицынаН. В., ШабалдинА. В. Интернет-программирование. Лабораторные работы. Часть 1: Методическое пособие. — Томск: Издательство ТГУ, 2002. 50 с.

68. СпицынаН. В. Этапы тестирования на взаимодействие // Материалы Международной конференции «Современные проблемы физики и высокие технологии». Томск: Издательство НТЛ, 2003. - С. 500-502.

69. Спицына Н. В., Тренькаев В. Н. К синтезу тестов для композиции конечных автоматов // Вестник ТГУ. Приложение. Серия «Математика. Кибернетика. Информатика». 2003. № 6. С. 183-187.

70. N. Spitsyna, V. Trenkaev. FSM Based Interoperability Testing of Communication Protocols // Proceedings of the IEEE-Siberian Conference on Control and Communications, SIBCON-2003, P. 20-23.

71. К. El-Fakih, V. Trenkaev, N. Spitsyna, N. Yevtushenko. FSM Based Interoperability Testing Methods // In Proc. of the IFIP 16th International Conference on Testing of Communicating Systems, Oxford, U.K., 2004, Published as LNCS 2978, P. 60-75.