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

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

¿І1І с/

Жигулин Максим Владимирович

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

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

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

1 О '¡Д.1 2Ш

Томск-2012

005017056

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

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

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

Официальные оппоненты: Матросова Анжела Юрьевна,

доктор технических наук, профессор, ФГБОУ ВПО «Национальный исследовательский Томский государственный университет», зав. кафедрой программирования

Громаков Евгений Иванович, кандидат технических наук, доцент, ФГБОУ ВПО «Национальный исследовательский Томский политехнический университет», доцент кафедры интегрированных компьютерных систем управления

Ведущая организация: ФГБУН Институт вычислительного

моделирования СО РАН, г. Красноярск

Защита диссертации состоится 23 мая 2012 года в 10.30 на заседании диссертационного совета Д 212.267.12 при Томском государственном университете по адресу: 634050, г. Томск, пр. Ленина, 36, II уч. корпус, ауд. 2126.

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

Автореферат разослан 20 апреля 2012 г.

Ученый секретарь — Тарасенко

диссертационного совета ,-/"7 Петр Феликсович

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

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

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

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

Научная новизна работы состоит в следующем.

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

Исследовано отношение эквивалентности между детерминированными временными автоматами и установлены необходимые и достаточные условия

эквивалентности временных автоматов с таймаутами на основе соответствия между множествами их состояний.

Для понижения избыточности тестов относительно модели «черного ящика» методы построения полного проверяющего теста для конечного автомата адаптированы для построения тестов непосредственно по временному автомату.

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

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

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

НИР «Разработка математических и программных средств обеспечения надежного и безопасного доступа к электронным ресурсам коллективного пользования» (в рамках инновационного проекта ТГУ), 20062007 гг.

НИР «Проведение прикладных и проблемно-ориентированных поисковых исследований в области информационно-телекоммуникационных систем с участием научных организаций Франции» (шифр заявки «2009-041.4-00-02-003»), госконтракт №02.514.12.4002 от 09.06.2009г.

Основные положения, выносимые на защиту.

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

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

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

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

Апробация работы. Все теоретические и практические результаты, составившие основу диссертационной работы, по мере их получения обсуждались на семинаре кафедры информационных технологий в исследовании дискретных структур радиофизического факультета ТГУ. Кроме того, результаты работы докладывались на научных конференциях: VI (VII, VIII) Российской конференции с международным участием «Новые информационные технологии в исследовании дискретных структур», с. Шушенское, 2006 г. (Томск, 2008 г. и 2010 г.); Российской конференции «VI Всесибирский конгресс женщин-математиков», Красноярск, 2010 г.; Международной научно-практической конференции «Актуальные проблемы радиофизики», Томск, 2010 г.; Международной конференции по качеству программного обеспечения, QSIC'2011, Мадрид, Испания, 2011 г.

Структура и объем работы. Диссертация состоит из введения, 4 глав, заключения и списка используемой литературы. Диссертация содержит 13 рисунков. Объем диссертации составляет 121 страницу, в том числе: титульный лист - одна страница, оглавление - три страницы, основной текст - 99 страниц, библиография из 85 наименований - 10 страниц, приложение -8 страниц.

Публикации. По результатам проведенных исследований опубликовано 9 статей в научных журналах и материалах конференций различного уровня. Работы [1-4] опубликованы в изданиях, входящих в список ВАК.

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

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

Первая глава посвящена основным понятиям и обозначениям, относящимся к конечным и временным автоматам, и, кроме того, содержит

обзор известных методов по синтезу проверяющих тестов для временных автоматов. Под конечным автоматом (автоматом) понимается пятерка 5 = (8,1, О, ¿о), где 5 - конечное непустое множество состояний с выделенным начальным состоянием я0; / и О - конечные непустые входной и выходной алфавиты; Т2 с 8x1x8x0 - отношение переходов; четверка «текущее состояние, входной символ, следующее состояние, выходной символ», называется переходом в автомате. В данной работе мы рассматриваем инициальные автоматы, то есть автоматы с фиксированным начальным состоянием; такие автоматы описывают поведение систем, обладающих сигналом сброса. Инициальный автомат описывает отображение входных последовательностей (слов) в выходные последовательности (слова). Если каждому входному слову соответствует единственное выходное слово, то автомат называется детерминированным: в противном случае автомат называется недетерминированным.

Далее, через N обозначается множество натуральных чисел; через Х+ -множество неотрицательных целых чисел.

Временным автоматом называется семерка 5 - (5,1, О, 50, 7'5, Д5, с5). где 5 - конечное непустое множество состояний с выделенным начальным состоянием «о, / и О - конечные, непересекающиеся входной и выходной алфавиты, 75с:5х/х0х5- отношение переходов, 5 -> 5 х (Ы и {°о}) -функция задержки, определяющая время, по истечении которого состояние автомата может спонтанно измениться, если на автомат в текущем состоянии не поступил ни один входной символ, (75: 75-» N определяет время задержки выходного символа после подачи входного воздействия на соответствующем переходе. Соответственно, поведение такого автомата зависит не только от входного символа, но и от момента времени, в который подается входной символ.

Временным входным символом называется пара (/, I) е / х 2+. Временной входной символ (/, /) означает, что входной символ г поступает на вход автомата в момент времени / после получения выходного символа на предыдущий входной символ. Для того чтобы определить выходную реакцию автомата на временной входной символ (г, /) в состоянии необходимо вычислить, в каком состоянии будет находиться автомат в г-й момент времени после перехода автомата в состояние 5.

Временным выходным символом называется пара (о, г) е О х Временной выходной символ (о, г) означает, что выходной символ о появился на выходе автомата через : единиц времени после подачи соответствующего входного символа. Значение переменной г определяется

6

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

Введем отображение times'. S х Z+ S. По определению, timers, 0) = s для любого состояния s. Воспользовавшись функцией As, можно определить состояние s' = timers, t) как состояние, достижимое из состояния s по задержкам (таймаутам), пока сумма задержек из состояния s не превышает t, и становится больше t, если прибавить задержку в состоянии 5'. Тогда во временном автомате существует временной переход (s, (/, /), (о, г), s'), если и только если во временном автомате существует переход {timers, t), /', (о,:), s'), где значение г определяется функцией as для данного перехода. Таким образом, множество outsis, (/, 0) выходных символов в состоянии times(s, t) на входной символ i есть множество выходных реакций временного автомата в состоянии s на временной входной символ (г, t). Множество next_siatcs(s, (У, t)) есть множество состояний, в которые переводит входной символ / автомат S из состояния timesis, t).

Обычным образом поведение временного автомата расширяется на временные входные и выходные последовательности. Пусть задана временная входная последовательность а - (i\, t\)(i2, h) ■■■ (h, h) и p = (Oj, ^Хсь,:2)...(ok, zk) - временная выходная последовательность автомата. Четверка (s, а, р, .v') 6 7's, если и только если во временном автомате существует последовательность переходов (s, (г'ь (оь г,), si), Obfe'2), (02, -2), «2), ..., Сч-и (ih h\ (О*. Zk), s')- В этом случае говорят, что временной автомат S в состоянии s может выдать временную выходную последовательность р на временную входную последовательность а и пара а/р называется временной входо-выходной последовательностью автомата.

Во временном автомате выделяют два вида состояний: /г-состояния, достижимые из начального состояния по некоторой временной входной последовательности, и iur-состояния, которые достижимы из некоторого /r-состояния только по задержкам. Временной автомат называется связным, если каждое состояние s' этого автомата является ir-состоянием или существуют //--состояние 5 и такое t, что times{s, t) = s'. Мы рассматриваем только связные временные автоматы.

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

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

Пусть = (5,1,0,50, Т2, с5) и Р = (Р,!,О,р0, ТР, АР, пР) -полностью определенные детерминированные временные автоматы. Будем говорить, что состояния .V автомата Б и р автомата Р эквивалентны (обозначение: .V = р), если для любой временной последовательности а справедливо ои^-?, а) = оШр(р, а). В противном случае состояния называются различимыми.

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

Временные автоматы Б и Р эквивалентны (обозначение: Б = Р), если эквивалентны их начальные состояния; в противном случае автоматы называются различимыми. Говорят, что временная входная последовательность а, для которой временные выходные последовательности автоматов 5 и Р не совпадают, различает автоматы Б и Р.

Поскольку при определении отношения эквивалентности временные выходные последовательности автоматов на каждую временную входную последовательность должны совпадать, то определение временного автомата можно упростить, а именно, рассматривать временной автомат как шестерку 5 = (5,1, О', ¡о, Т^, А5) [7], в которой выходной алфавит О' содержит пары (о, г), показывающие, в какой момент времени производится выходной символ о.

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

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

Самым простым способом задания модели неисправности является явное перечисление всех временных автоматов из области неисправности и нахождение для каждого неконформного автомата последовательности, отличающей этот временной автомат от автомата-спецификации. В общем случае такое описание области неисправности возможно только для небольшого числа неисправностей, и в случае, когда такое перечисление невозможно, в качестве модели неисправности часто рассматриваются модели «серого ящика» и «черного ящика». При использовании модели «серого ящика» предполагается, что частично известна структура проверяемой системы. При использовании модели «чёрного ящика» предполагается, что внутренняя структура проверяемой системы неизвестна. В модели «черного ящика» обычно предполагается известной верхняя оценка числа состояний проверяемого автомата, т.е. предполагается, что любая неисправность может увеличить число состояний только в некоторых пределах. В классической теории автоматов полные проверяющие тесты относительно модели «черного ящика» строятся на основе установления соответствия между состояниями и переходами автомата-спецификации и проверяемого автомата. Поскольку в этом случае проверяются все переходы в системе, то тесты, построенные относительно этой модели, являются достаточно качественными. Однако длина теста пропорциональна ¡/¡"'~"", где (т - п) равно разности числа состояний проверяемого автомата и автомата-спецификации и ¡7) - мощность входного алфавита.

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

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

{^-методом в предположении, что поведение полуавтомата-спецификации и полуавтомата-реализации можно описать детерминированным конечным автоматом, и известна верхняя оценка числа временных областей для проверяемого полуавтомата. Однако как замечают авторы, получаемый в результате тест оказывается слишком избыточным, что затрудняет его использование на практике. Тем не менее, данная статья впервые показывает, что для временных автоматов/полуавтоматов можно построить конечный проверяющий тест с гарантированной полнотой даже в том случае, когда область определения временной переменной есть множество неотрицательных рациональных чисел, т.е. является бесконечной. Во второй группе представлены работы, в которых обсуждаются методы построения проверяющих тестов по модели временного автомата, как конечного автомата с таймаутами. В этих работах авторы рассматривают различные отношения конформности между такими автоматами, и, кроме того, устанавливают необходимые и достаточные условия различимости двух, возможно недетерминированных, временных автоматов на основе их пересечения. Было показано, что модель (расширенного) автомата с таймаутами является достаточно выразительной; с ее помощью можно описывать поведение различных временных систем, в частности, телекоммуникационных протоколов и шеЬ-приложений. Однако в большинстве работ авторы используют эвристические методы построения тестов, полнота которых остается неизвестной. Поэтому в данной работе мы продолжаем исследование автоматов с таймаутами с целью построения на основе этой модели проверяющих тестов с гарантированной полнотой.

Поскольку методы построения тестов с гарантированной полнотой хорошо развиты для классических конечных автоматов, то во второй главе диссертации (разделы 2.1 и 2.2) мы предлагаем метод преобразования временного автомата в соответствующий классический конечный автомат [10], который заключается в следующем. На первом шаге из исходного временного автомата удаляются все переходы по задержкам. Если в некотором состоянии значение таймаута равно Г, то в строящемся классическом автомате добавляется (I - 1) копия этого состояния. В каждой копии автомат имеет такое же поведение, как в оригинальном состоянии для всех входных символов. Вводятся дополнительный входной символ 1, обозначающий ожидание входного воздействия в течение одной единицы времени, и выходной символ п, обозначающий отсутствие выходного сигнала. Исходное состояние, его копии, и состояние, в которое автомат переходит по задержке из этого состояния, соединяются цепочкой переходов,

каждый из которых помечен входо-выходной парой I/o. Если таймаут в некотором состоянии равен «бесконечности», то в этом состоянии добавляется петля, помеченная входо-выходной парой 1 In. Чтобы промоделировать задержки на выходе в классическом автомате каждый временной выходной символ заменяется абстрактным, представляющим пару «выходной символ, задержка выходного символа».

Показывается, что между временными входо-выходными последовательностями исходного временного автомата S и построенного классического автомата As существует взаимно однозначное соответствие.

Утверждение 1. Для любой временной входо-выходной последовательности (г'ь /^/о, ... (im,tm)!om временного автомата S в соответствующем конечном автомате As существует входо-выходная последовательность \/п..Л/п /i/o-, ... 1/и...!/« iJom.

'1

Кроме того, для любой входо-выходной последовательности \/п... 1/77 i\iü\ ... \/п... \/п imlom автомата As в автомате S существует

временная входо-выходная последовательность (г'ь t{)lo\ ... (;,„, tm)/om.

Теорема 1. Два временных полностью определенных автомата S = (S, /, О, s0, Ts, As) и Р = (Р, I, О, ро, Тр, Ар) эквивалентны, если и только если эквивалентны конечные автоматы As и Ар.

В разделе 2.3 мы рассматриваем тесты, построенные на основе обхода графа переходов соответствующего конечного автомата. Данный подход позволяет строить проверяющие тесты с гарантированной полнотой не только для управляющих систем, поведение которых описано детерминированным временным автоматом, но также и для систем, для которых соответствующий временной автомат является недетерминированным и/или частичным. В разделе 2.3 рассматривается проверяющий тест для протокола TFTP, построенный подобно тесту для протокола 1RC [4], на основе обхода графа переходов соответствующего конечного автомата, который выявил ряд несоответствий в доступных реализациях этого протокола: класса TFTPServer из библиотеки commons-net-2.0.0, сервера atftpd для Linux. Кроме того, компьютерные эксперименты, проведенные со случайно сгенерированными временными автоматами, показали, что тесты, построенные непосредственно по временному автомату, короче тестов, построенных по соответствующему классическому автомату.

Как известно, тесты, построенные на основе обхода графа переходов, гарантированно обнаруживают только выходные ошибки. Для обнаружения

11

всех ошибок перехода системы под действием входного символа в «неправильное» состояние проверяющий тест должен строиться относительно модели «черного ящика».

В третьей главе обсуждаются методы построения проверяющих тестов для временных автоматов относительно модели «черного ящика». В разделе 2.2 показывается, что методы построения полного проверяющего теста для временного автомата относительно модели «черного ящика» по соответствующему классическому автомату обычно доставляют тесты с большой избыточностью [10]. Этот факт объясняется тем, что область неисправности для построенного конечного автомата содержит «лишние» автоматы, которые не соответствуют ни одному временному автомату из области неисправности. Поэтому в третьей главе мы адаптируем методы из классической теории автоматов для построения полных проверяющих тестов непосредственно по временному автомату.

Для этого первоначально устанавливаем конструктивные необходимые и достаточные условия эквивалентности двух детерминированных временных автоматов на основе соответствия между конечным множеством их состояний (раздел 3.2) [2, 7, 10].

Утверждение 2. Если S = (S, s,h I, О, Ts, A s) — приведенный автомат, то автоматы S и Р эквивалентны, если и только если существует отображение h: Р —> S, со следующими свойствами:

а) h(p0) = s0;

б) Vp е Р и Vi е I выполняется outfip, (/', 0)) = outs(h(p), (i, 0)) и h{next stateр{р, (/', 0))) = next state${h(p), (/, 0));

в) Vp e Pir и любого момента времени t справедливо h{timep(p, t)) = times(h(p), t).

Следствие. Приведенные детерминированные полностью определенные временные автоматы S и Р являются эквивалентными, если и только если существует взаимно однозначное отображение h: S -> Р, такое, что h(s0) — ро и для любого состояния s e S, для каждого перехода s-t->s' и каждого перехода .v - Но —> s' автомат Р имеет переходы h(s) -1 -> h(s') и h(s) - i/o h(s').

На основе установленного соответствия в разделе 3.3 предлагается метод синтеза полного проверяющего теста относительно модели «черного ящика» непосредственно по модели временного автомата [2, 3, 7, 9, 10]. В разделе 3.3.1 предполагается, что число состояний временного проверяемого автомата не превышает числа состояний автомата-спецификации, и конечная задержка в каждом состоянии не превышает некоторой величины В.

12

Предложенный метод синтеза полных проверяющих тестов основывается на (^-методе построения тестов для конечных классических автоматов, однако имеет свои особенности.

Множество IV временных входных последовательностей называется множеством различимости приведенного автомата S, если для любых двух различных состояний s¡ и s¡ существует временная входная последовательность у е IV, такая что ouls(s„ у) * outsisj, у).

Обозначим через S,r множество //-состояний, и через S,„r множество ('«/--СОСТОЯНИЙ. Для каждого СОСТОЯНИЯ 5 е Sin построим временную входную последовательность as, которая переводит автомат S из s0 в состояние s. Префикс замкнутое множество таких последовательностей есть множество достижимости V¡r для //--состояний автомата-спецификации. Для достижения /г/г-состояний определим функцию u: S,„r V,r х / •, которая для каждого шг-состояния s', определяет /r-состояние s, такое, что существует переход по задержке timers, т) = s', и возвращает пару {а,, т}, где а, е V переводит автомат S из sa в s, и т - время задержки, через которое автомат S переходит из 5 в i'.

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

Алгоритм 1. Построение полного проверяющего теста для временных автоматов относительно модели неисправности <S, =, 3„(/, О, В)>.

Вход: Детерминированный полностью определенный приведенный временной автомат-спецификация S = (S, s0,1, О, T$, As) с п состояниями, В — максимальная конечная задержка в состояниях проверяемого автомата.

Выход: Полный проверяющий тест TS относительно модели неисправности <S, s, 3„(I, О, В)>.

Строим множества Vlr и IV для автомата S.

Шаг 1. Строим множество TS¡ = Vir.W. Для каждого гыг-состояния s' фиксируем пару и(У) = {а5, т}. Добавляем as.W в множество TS¡.

Шаг 2. Строим множество TS2 = V„..(i,0).W и для каждого iur-состояния s', которое достижимо из зафиксированного состоянии 5 по задержке т, в множество TS2 добавляем «,.(/, т)Ж

ШагЗ. \fs е Sir в множество TSj добавляем a,.if', t = 1, ..., Т, где Т = As(s)|n если As(.s')»n 00 и Т — В в противном случае.

W е 5,-„„ для которого u(s') = {as, т}, в множество TS3 добавляем as.lVz+', t = 1, ..., Т, где Т ~ As(i')iN если A5(s')|N #юиГ=Вв противном случае.

Шаг 4. Из TS ~ Г51 и TS2 kj TS3 удаляем последовательности, которые являются собственными начальными отрезками других последовательностей.

Теорема 2. Множество TS, построенное по алгоритму 1, есть полный

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

Утверждение 3. Пусть реакции автомата Р е Зт{1,0, В) на последовательности множества TS-, и TS2 (алгоритм 1) совпадают с реакциями автомата-спецификации на эти последовательности и Р' -подмножество состояний проверяемого автомата, для которых установлено соответствие по этим последовательностям. Пусть s е S,r и a, е V переводит автомат S из ,vG R состояние s, и W е Snir зафиксирована пара и(.у') = {а„ т}. Тогда временные входные последовательности из множеств

покрывают все переходы из состояний множества ^//"автомата Р.

Алгоритм 2. Построение полного проверяющего теста относительно модели неисправности <5,,%,(/, О, В)>.

14

Конец.

проверяющий тест относительно модели неисправности <S, =, Я„(/, О. В)>.

Вход: Детерминированный полностью определенный приведенный временной автомат-спецификация S = (5, s0,1, 0, 7's, As) с п состояниями, т > п - максимальное число состояний в проверяемом автомате, В -максимальная конечная задержка в состоянии проверяемого автомата.

Выход: Полный проверяющий тест TS относительно модели неисправности <S, =, Зт (/, О, В)>.

Строим множества Vin W, Traversal„^ для автомата S.

Шаг 1. Строим множество TS\ = Vtr. W. Для каждого ;г//--состояния s' фиксируем пару u(s') = {as, т}. Добавляем последовательности aSJVX в множество TSt.

Шаг 3. Строим множество Traversal, равное объединению множеств as.Traversal„j„, as е Vir, и для каждого гмг-состояния s' с зафиксированной парой o(s') = {a5, т} в Traversal добавляем множество a¡.Traversa?пт. В множество TSj для каждой последовательности р е Traversal включаем все последовательности fi.IV и, кроме того, для каждой последовательности

р.(4, tk) е Traversal в TS2 добавляются все последовательности p. W<k .

Шаг 4. Из TS = TSi u TS2 удаляем последовательности, которые являются начальными отрезками других последовательностей.

Конец.

Теорема 3. Множество TS, построенное по алгоритму 2, есть полный проверяющий тест относительно модели неисправности <S, s, Зт{1, О, В)>.

В разделе 3.4 обсуждаются оценки максимальной длины проверяющих тестов, построенных предложенным методом, и показывается, что порядок верхних оценок длины построенных тестов совпадает с таковым для классических конечных автоматов. При одинаковом числе состояний проверяемого автомата и автомата-спецификации верхняя оценка длины полного проверяющего теста полиноминалыю зависит от размерности автомата-спецификации и максимальной величины конечного таймаута в состоянии проверяемого автомата. Если проверяемый автомат может иметь больше состояний, чем автомат-спецификация, то верхняя оценка длины полного проверяющего теста экспоненциально зависит от разности числа состояний в проверяемом автомате и автомате-спецификации. Проведенные эксперименты показывают, что порядок длины теста относительно модели «черного ящика» для случая, когда неисправности не увеличивают число состоя1шй в тестируемой реализации, совпадает с порядком проверяющих тестов для классических конечных автоматов [8]. Более того, длина таких проверяющих тестов близка к длине входо-выходной последовательности,

которую нужно пронаблюдать при пассивном тестировании протокольной реализации [1,2,5,6] для того, чтобы гарантировать полноту проверки относительно модели «серого ящика».

В четвертой главе рассматриваются модификации модели неисправности «черный ящик» [3, 9], и предлагается соответствующая адаптация алгоритмов, описанных в главе 3, при построении полных проверяющих тестов относительно таких моделей неисправности.

В первом случае (раздел 4.1) предполагается, что в проверяемом автомате в каждом из состояний возможны только задержки, которые есть в автомате-спецификации. Пусть задан автомат-спецификация Sen состояниями и множеством конечных задержек П = {¿ь ..., b:}, z < п, т.е. As- 5 —> S х (П и {со}). Мы предполагаем, что проверяемый автомат есть некоторый полностью определенный детерминированный временной автомат Р из множества Я„(/, О, П). т.е. автомат Р имеет не более п состояний, входной и выходной алфавиты / и О, и конечная задержка в состоянии есть некоторый элемент множества П, т.е. АР: РР х (П и {=е}). Алгоритм построения теста для данного случая аналогичен алгоритму 1, только на шаге 3 значение t е П и если As(.?)1n * оо, то / < As(i);N.

Теорема 4. Множество TS, построенное по алгоритму 1 с указанным выше изменением, есть полный проверяющий тест относительно модели неисправности <S, =, 3„{h О, П)>.

Во втором случае (раздел 4.2) предполагается, что конечная задержка в каждом из состояний проверяемого автомата не меньше некоторой известной величины. Пусть задан приведенный автомат-спецификация Sen состояниями. Мы предполагаем, что проверяемый автомат есть некоторый временной автомат Р, который имеет не более п состояний, входной и выходной алфавиты / и О, и конечная задержка в каждом состоянии автомата Р не меньше D и не больше В. Обозначим такую область неисправности как 3„(1, О, [Д В]). Алгоритм построения теста для данного случая аналогичен алгоритму 1, только на шаге 3 значение / е {Д ..., As(s)|n}, если As(.s);n * °° и t е {D, ..., В] в противном случае.

Теорема 5. Множество TS, построенное по алгоритму 1 с указанным выше изменением, есть полный проверяющий тест относительно модели неисправности <S, 3„{1, О, [Д й])>.

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

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

Интуитивно понятно, что сравнение скорости обработки входных воздействий имеет смысл только для автоматов, которые на каждую временную входную последовательность выдают одинаковые выходные последовательности. Такие автоматы будем называть /-эквивалентными [7, 8].

Если проверяемый автомат имеет число состояний, равное числу состояний автомата-спецификации, т.е. принадлежит множеству 3„{1, О, В), п = |5], то для проверки соответствия времени реакции на входные символы достаточно построить обход графа переходов автомата

Для каждого />-состояния .V автомата 5, строим последовательности а5-(л 0), а, б К, / е /. Объединяем все последовательности во множество ТТБх. Для каждого ///^-состояния 5-', находим пару и(л') = {а„ т} и строим последовательности а1.(/, т), / е /. Объединяем все последовательности во множество ТТБ2.

Множество ТТЯ = 7Т5] и ТТ82 есть полный тест для проверки, является ли автомат Р строго не медленнее (строго не быстрее) автомата 5 по времени обработки временных входных последовательностей.

Утверждение 4. Если автомат Р е 3„(/, О, В) является /•эквивалентным автомату 5, то автомат Р строго не медленнее (строго не быстрее) автомата 5, если и только если время обработки каждого временного входного символа из последовательностей множества 7Т5 не больше (соответственно не меньше) времени обработки этого символа автоматом 5.

Заметим, что методы построения полного проверяющего теста, предложенные в главе 3, включают в себя тест для проверки /■эквивалентности, а также включают в себя последовательности теста, необходимые для проверки соответствия времени обработки входных символов.

В заключении формулируются основные результаты работы.

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

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

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

Отметим, что длину полного проверяющего теста относительно модели «черного ящика», построенного по одному из предложенных алгоритмов, можно уменьшить как за счет применения более эффективных методов использования различающих последовательностей, как это делается в HSI, Н и SPY методах для классических конечных автоматов, так и за счет сокращения области неисправности, как предлагается в главе 4.

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

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

1. Жигулин М.В. Оценка полноты проверки при пассивном тестировании на основе автоматной модели / М.В. Жигулин, A.B. Коломеец // Известия Томского политехнического университета. -2009. - Т. 314, № 5. - С. 225-228.

2. Жигулин М.В. Синтез тестов с гарантированной полнотой для временных автоматов / М.В. Жигулин, И.М. Дмитриев, И.В. Евтушенко // Известия Томского политехнического университета. - 2010. - Т. 316, №5.-С. 104-110.

3. Дмитриев И.М. Синтез проверяющих тестов с гарантированной полнотой для временных автоматов с конечными задержками / И.М. Дмитриев, М.В. Жигулин // Известия высших учебных заведений. Физика. - 2010. - Т. 53, № 9/3. - С. 196-198.

4. M.B. Жигулин Тестирование программной реализации протокола IRC на основе модели расширенного автомата / М.В. Жигулин, A.B. Коломеец, Н.Г. Кушик, A.B. Шабалдин // Известия Томского политехнического университета. - 2011. - Т. 318, № 5. - С. 8184.

5. Жигулин М.В. Преобразование спецификации при пассивном тестировании телекоммуникационных протоколов / М.В. Жигулин, С.А. Прокопенко, Н.В. Евтушенко // Новые информационные технологии в исследовании сложных структур : доклады VI Всероссийской конференции с международным участием // Вестник Томского государственного университета. Приложение. - Томск, 2006. - № 18. - С. 62-66.

6. Жигулин М.В. Оценка полноты проверки при пассивном тестировании на основе автоматной модели / М.В. Жигулин // Новые информационные технологии в исследовании сложных структур : тезисы докладов седьмой Российской конференции с международным участием. — Томск,2008.-С. 48.

7. Жигулин М.В. Необходимое и достаточное условие /■эквивалентности временных автоматов / М.В. Жигулин, И.М. Дмитриев // VI Всесибирский конгресс женщин-математиков : материалы Всероссийской конференции. — Красноярск, 2010. - С. 137-141.

8. Проведение прикладных и проблемно-поисковых исследований в области информационно-телекоммуникационных систем с участием научных организаций Франции. Этап 4. Экспериментальные исследования поставленных перед НИР задач. Обобщение и оценка результатов исследования: отчет о НИР (заключительный) / Том. гос. ун-т ; рук. Н.В. Евтушенко. - Томск, 2010. - 301 с. - № ГР 01200962727.

9. Жигулин М.В. Алгоритм синтеза проверяющего теста с гарантированной полнотой для конечных временных автоматов с фиксированным набором задержек для модели «черного ящика» / М.В. Жигулин, И.М. Дмитриев, Д.Д. Попов // Новые информационные технологии в исследовании сложных структур : тезисы докладов восьмой Российской конференции с международным участием. - Томск, 2010. - С. 50.

10. Zhigulin М. FSM-Based Test Derivation Strategies for Systems with Time-Outs / M. Zhigulin, N. Yevtushenko, S. Maag, A. Cavalli // 11th International conference on quality software. - Madrid, 2011. - P. 141-150.

Подписано в печать 18.04.2012 г. Формат А4/2. Ризография . л. 1,0. Тираж 100 экз. Заказ № 15/04-12 Отпечатано в ООО «Позитив-НБ» 634050 г. Томск, пр. Ленина 34а

Введение

1. Основные понятия и краткий обзор литературы

1.1. Конечные автоматы

1.2. Конечные автоматы с временными задержками

1.3. Отношения между временными автоматами

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

1.4.1. Полные проверяющие тесты

1.4.2. Построение теста перечислением неисправностей

1.4.3. Модель «черного ящика» для классических конечных автоматов

1.4.4. Синтез проверяющего теста для конечного автомата на основе обхода графа переходов

1.4.5. Модель «серого ящика» (мутационный автомат) для классических конечных автоматов

1.5. Синтез полных проверяющих тестов для временных автоматов

1.5.1. Автоматная модель Алюра и Дилла

1.5.2. Автоматная модель с задержками на переходах и выходах

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

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

2.1. Построение соответствующего конечного автомата

2.1.1. Метод построения конечного автомата для удаления переходов по задержке

2.1.2. Соответствие между временным автоматом и построенным конечным автоматом

2.2. Построение проверяющих тестов для временного автомата на основе соответствующего конечного автомата

2.2.1. Алгоритм построения проверяющего теста на основе соответствующего конечного автомата

2.2.2. Построение проверяющих тестов на основе явного перечисления неисправностей

2.2.3. Построение полных проверяющих тестов относительно выходных неисправностей

2.2.4. Построение проверяющих тестов для проверки переходов временного автомата

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

2.3.1. Временной автомат, описывающий поведение протокола ТРТР, и построение проверяющего теста по временному автомату

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

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

2.5. Результаты главы

3. Метод синтеза проверяющих тестов для временных автоматов относительно модели «черного ящика»

3.1. Модель «черного ящика» для временных автоматов

3.2. Необходимые и достаточные условия эквивалентности временных автоматов

3.3. Синтез полного проверяющего теста для временных автоматов относительно модели «черного ящика»

3.3.1. Множества различимости и достижимости для временного автомата

3.3.2. Построение проверяющего теста при т-п

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

3.4. Оценка сложности проверяющих тестов относительно модели «черного ящика»

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

3.6. Результаты главы

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

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

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

4.3. Отношения между временными автоматами в зависимости от времени обработки входных воздействий

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

4.5. Результаты главы

Актуальность проблемы. Тестирование является неотъемлемой частью жизненного цикла любой управляющей системы. Цена ошибки в таких системах резко возрастает по мере нарастания сложности и важности решаемых задач, и существенный прогресс в области тестирования таких систем связывается с развитием формальных методов [18, 20, 30, 32, 35, 45]. При синтезе проверяющих и диагностических тестов для дискретных управляющих систем широко используются конечно-автоматные модели [см. например, 10, 59, 60, 62, 79, 81], методы синтеза тестов с гарантированной полнотой для которых хорошо известны. Однако классические автоматные модели явно не описывают временные аспекты поведения системы, такие как таймауты для ожидания подтверждения, допустимую задержку выходного отклика на поданное входное воздействие и т.п. Поэтому в настоящее время активно исследуется вопрос о построении тестов с гарантированной полнотой на основе временных полуавтоматов и автоматов [24, 29, 31, 39, 41, 43, 44, 47, 49, 50, 53, 58, 66, 67, 72, 77, 82, 84]. Однако практически все известные методы синтеза тестов для временных автоматов доставляют конечные проверяющие тесты, полнота которых остается неизвестной, и, соответственно, синтез конечных проверяющих тестов с гарантированной полнотой для систем с явно выраженными временными аспектами требует дополнительных исследований. Достаточно выразительной моделью является конечный автомат с таймаутами, и, таким образом, разработка методов синтеза проверяющих тестов с гарантированной полнотой для таких временных автоматов является актуальной задачей.

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

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

Научная новизна работы состоит в следующем.

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

Исследовано отношение эквивалентности между детерминированными временными автоматами и установлены необходимые и достаточные условия эквивалентности временных автоматов с таймаутами на основе соответствия между множествами их состояний.

Для понижения избыточности тестов относительно модели «черного ящика» методы построения полного проверяющего теста для конечного автомата адаптированы для построения тестов непосредственно по временному автомату.

Основные положения, выносимые на защиту.

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

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

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

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

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

1. НИР «Разработка математических и программных средств обеспечения надежного и безопасного доступа к электронным ресурсам коллективного пользования» (в рамках инновационного проекта ТГУ), 2006-2007 гг.

2. НИР «Проведение прикладных и проблемно-ориентированных поисковых исследований в области информационно-телекоммуникационных систем с участием научных организаций Франции» (шифр заявки «2009-04-1.400-02-003»), госконтракт №02.514.12.4002 от 09.06.2009г.

Апробация работы. Все теоретические и практические результаты, составившие основу диссертационной работы, по мере их получения обсуждались на семинаре кафедры информационных технологий в исследовании дискретных структур радиофизического факультета ТГУ. Кроме того, результаты работы докладывались на научных конференциях: VI (VII, VIII) Российской конференции с международным участием «Новые информационные технологии в исследовании дискретных структур», с. Шушенское, 2006 г. (Томск, 2008 г. и 2010 г.); Российской конференции «VI Всесибирский конгресс женщин-математиков», Красноярск, 2010 г.; Международной научно-практической конференции «Актуальные проблемы радиофизики», Томск, 2010 г.; Международной конференции по качеству программного обеспечения, QSIC'2011, Мадрид, Испания, 2011 г.

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

Жигулин М.В. Преобразование спецификации при пассивном тестировании телекоммуникационных протоколов / М.В. Жигулин, С.А. Прокопенко, Н.В. Евтушенко // Вестник Томского государственного университета. Приложение. Доклады VI Всероссийской конференции с международным участием "Новые информационные технологии в исследовании сложных структур". - Томск, 2006. - № 18. - С. 62-66.

Жигулин М.В. Оценка полноты проверки при пассивном тестировании на основе автоматной модели // Новые информационные технологии в исследовании сложных структур: тезисы докладов седьмой Российской конференции с международным участием. - Томск, 2008. - С. 48.

Жигулин М.В. Оценка полноты проверки при пассивном тестировании на основе автоматной модели / М.В. Жигулин, А.В. Коломеец // Известия Томского политехнического университета. — 2009. - Т. 314, № 5. - С. 225-228.

Жигулин М.В. Необходимое и достаточное условие /-эквивалентности временных автоматов / М.В. Жигулин, И.М. Дмитриев // VI Всесибирский конгресс женщин-математиков: материалы Всероссийской конференции. -Красноярск, 2010. - С. 137-141.

Жигулин М.В. Синтез тестов с гарантированной полнотой для временных автоматов / М.В. Жигулин, И.М. Дмитриев, Н.В. Евтушенко // Известия Томского политехнического университета. — 2010. - Т. 316, № 5. — С. 104-110.

Жигулин М.В. Алгоритм синтеза проверяющего теста с гарантированной полнотой для конечных временных автоматов с фиксированным набором задержек для модели «черного ящика» / М.В. Жигулин, И.М. Дмитриев, Д.Д. Попов // Новые информационные технологии в исследовании сложных структур: тезисы докладов восьмой Российской конференции с международным участием. - Томск, 2010. - С. 50.

Дмитриев И.М. Синтез проверяющих тестов с гарантированной полнотой для временных автоматов с конечными задержками / И.М.Дмитриев, М.В. Жигулин II Известия высших учебных заведений: Физика. - Томск, 2010. - Т. 53, № 9/3. - С. 196-198.

М.В. Жигулин Тестирование программной реализации протокола IRC на основе модели расширенного автомата / М.В. Жигулин, A.B. Коломеец, Н.Г. Кушик, A.B. Шабалдин // Известия Томского политехнического университета. - Томск, 2011. - Т. 318, № 5. - С. 81-84.

Zhigulin М. FSM-Based Test Derivation Strategies for Systems with TimeOuts / M. Zhigulin, N. Yevtushenko, S. Maag, A. Cavalli // 11th International conference on quality software - Madrid, 2011. - P. 141-150.

Структура и объем работы. Диссертация состоит из введения, 4 глав, заключения и списка используемой литературы. Диссертация содержит 13 рисунков. Объем диссертации составляет 121 страница, в том числе: титульный

ЗАКЛЮЧЕНИЕ

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

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

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

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

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

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

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

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

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

4. Громов M.JI. Разработка методов синтеза условных тестов для автоматных моделей с недетерминированным поведением: дис. на соискание ученой степени канд. физ.-мат. наук / M.J1. Громов. Томск, 2009. - 154 с.

5. Громов M.J1. Синтез условных различающих экспериментов для автоматов с недетерминированным поведением / M.JI. Громов, Н.В. Евтушенко // Прикладная дискретная математика. Томск, 2009. - № 4(6). - С. 90-101.

6. Громов M.JI. Синтез различающих экспериментов для временных автоматов / M.JI. Громов, Н.В. Евтушенко. // Программирование. 2010. -№ 4. - С. 40-50.

7. Дорофеева М.Ю. Исследование и разработка конечно-автоматных методов синтеза проверяющих тестов для управляющих систем: дис. на соискание ученой степени канд. тех. наук / Дорофеева М.Ю. Томск, 2007. - 145 с.

8. Дмитриев И.М. Синтез проверяющих тестов с гарантированной полнотой для временных автоматов с конечными задержками / И.М. Дмитриев, М.В.Жигулин // Известия высших учебных заведений: Физика. 2010. -Т. 53, № 9/3 - С. 196-198.

9. Евтушенко Н.В. Метод построения эксперимента для произвольного детерминированного автомата / Н.В. Евтушенко, А.Ф. Петренко // Автоматика и вычислительная техника. 1990. - № 5. - С. 73-76.

10. Ю.Евтушенко Н.В. Недетерминированные автоматы: анализ и синтез. 4.1. Отношения и операции: учеб. пособие / Н.В. Евтушенко, А.Ф. Петренко, М.В. Ветрова. Томск: Томский государственный университет, 2006. -142 с.

11. Жигулин М.В. Оценка полноты проверки при пассивном тестировании на основе автоматной модели / М.В. Жигулин, А.В. Коломеец // Известия Томского политехнического университета. 2009. - Т. 314, № 5. - С. 225228.

12. Жигулин М.В. Необходимое и достаточное условие /-эквивалентности временных автоматов / М.В. Жигулин, И.М. Дмитриев // VI Всесибирский конгресс женщин-математиков: материалы Всероссийской конференции. -Красноярск, 2010.-С. 137-141.

13. Жигулин М.В. Синтез тестов с гарантированной полнотой для временных автоматов / М.В. Жигулин, И.М. Дмитриев, Н.В. Евтушенко // Известия Томского политехнического университета. 2010. - Т. 316, № 5. - С. 104110.

14. Жигулин М.В. Алгоритм синтеза проверяющего теста с гарантированной полнотой для конечных временных автоматов с фиксированным набором задержек для модели «черного ящика» / М.В. Жигулин, И.М. Дмитриев,

15. Д.Д. Попов // Новые информационные технологии в исследовании сложнь1х структур: тезисы докладов восьмой Российской конференции с международным участием. Томск, 2010. - С. 50.

16. Жигулин М.В. Тестирование программной реализации протокола IRC на основе модели расширенного автомата / М.В. Жигулин, A.B. Коломеец, Н.Г. Кушик, A.B. Шабалдин // Известия Томского политехнического университета. 2011. - Т. 318, № 5 - С. 81 -84.

17. Карибский В.В. Основы технической диагностики / В.В. Карибский, П.П. Пархоменко, Е.С. Согомонян, В.Ф. Халчев -М.: Энергия, 1976. 464 с.

18. Куфарева И.Б. Применение недетерминированных автоматов в задачах синтеза проверяющих тестов в системах логического проектирования: дис. на соискание ученой степени канд. тех. наук / И.Б. Куфарева. Томск, 2000. - 168 с.

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

20. Мур Э. Умозрительные эксперименты с последовательными машинами. / Э. Мур, Автоматы. Сб. статей под ред. К. Шеннона, Д. Маккарти. М.: Изд-во иностр. лит, 1956. - С. 179-213.

21. Трахтенброт Б.А. Конечные автоматы. Поведение и синтез / Б.А. Трахтенброт, Я.М. Барздинь. М.: Наука, 1970. - 396 с.

22. Adjar N. Testing real-time systems using TINA / N. Adjar, P. De Saqui-Sannes, К. M. Rahmouni // Testing of software and communication systems. Lecture notes in computer science. 2009. - Vol. 5826. - P. 1-15.

23. Advanced TFTP Электронный ресурс. Электрон, текст, дан. - Geeknet, 2011. - URL: http://freecode.com/projects/atftp (дата обращения: 06.09.2011).

24. Alur R. A theory of timed automata / R. Alur, D.L. Dill // Theoretical computer science.-1994.-Vol. 126, No. 2.-P. 183-235.

25. Alur R. Automata-theoretic verification of real-time systems / R. Alur, D.L. Dill // In formal methods for real-time computing, trends in software series. 1996. -P. 55-82.

26. Apache commons net Электронный ресурс. Электрон, текст, дан. - The Apache software foundation, 2001-2011. - URL: http://commons.apache.org/net (дата обращения: 06.09.2011).

27. Baumgarten В. Timed systems behaviour and conformance testing a mathematical framework / B. Baumgarten // International federation for information processing. - 1996. - P. 89-104.

28. Bochmann G.V. Protocol testing: review of methods and relevance for software testing / G. von Bochmann, A. Petrenko. // Proceedings of the international symposium on software testing and analysis. Washington, USA, 1994. - P. 109124.

29. Bosnacki D. Integrating real time into SPIN: a prototype implementation / D. Bosnacki, D. Dams // Proceeding of formal description techniques and protocol specification, testing and verification. Netherlands, 1998. - P. 423-439.

30. Brinksma E. Testing transition systems: an annotated bibliography / E. Brinksma, J. Tretmans // Modeling and verification of parallel processes. Lecture notes in computer science. 2001. - Vol. 2067 - P. 187-195.

31. Cao T.-D. Testing of web services: tools and experiments / T.-D. Cao, R. Castanet, P. Felix, G. Morales // IEEE Asia Pacific services computing conference. - Jeju, Korea, 2011. - P. 78-85.

32. Cardell-Oliver R. A practical and complete algorithm for testing real-time systems / R. Cardell-Oliver, T. Glover // Formal techniques for real-time fault tolerant systems. Denmark, 1998. - P. 251-261.

33. Chen W.H. Executable test sequences for the protocol data flow property // Proceedings of the 21st International conference on formal techniques for networked and distributed systems. 2001. - P. 285-299.

34. Chow T.S. Test software design modeled by finite state machine // IEEE Transactions on software engineering. 1978. - Vol. SE-4(3). - P. 178-187.

35. Dorofeeva M. Experimental evaluation of FSM-based testing methods / M. Dorofeeva, K. El-Fakih, A.R. Cavalli, N. Yevtushenko // IEEE International conference on software engineering and formal methods. 2005. - P. 23-32.

36. Dorofeeva M. FSM-based conformance testing methods: A survey annotated with experimental evaluation / M. Dorofeeva, K. El-Fakih, S. Maag, A.R. Cavalli, N. Yevtushenko // Information and software technology. 2010. - Vol. 52(12). -P. 1286-1297.

37. El-Fakih K. Fault diagnosis in extended finite state machines / K. El-Fakih, S. Prokopenko, N. Yevtushenko, G. Bochmann // Testing of communicating systems. Lecture notes in computer science. 2003 - Vol. 2644. - P. 197-210.

38. El-Fakih K. FSM-based incremental conformance testing methods / K. El-Fakih, N. Yevtushenko, G. von Bochmann // IEEE Transactions on software engineering. 2004. - Vol. 30(7). - P. 425-436.

39. El-Fakih K. Testing timed finite state machines with guaranteed fault coverage / K. El-Fakih, N. Yevtushenko, H. Fouchal // Formal techniques for networked and distributed systems. Lecture notes in computer science. 2009. - Vol. 5826. -P. 66-80.

40. En-Nouaary A. Timed test cases generation based on state characterization technique / A. En-Nouaary, R. Dssouli, F. Khendek, A. Elqortobi // Proceedings of the real-time systems symposium. 1998. - P. 220-229.

41. En-Nouaary A. Timed Wp-method: testing real-time systems / A. En-Nouaary, R. Dssouli, F. Khendek // In proceedings of IEEE Trans, software eng. -Vol. 28(11).-2002.-P. 1023-1038.

42. En-Nouaary A. A guided method for testing timed input output automata / A. En-Nouaary, R. Dssouli // Testing of communicating systems. Lecture notes in computer science. 2003. - Vol. 2644. - P. 211-224.

43. Favreau J.P. Automatic generation of test scenario skeletons from protocol specifications written in ESTELLE / J.P. Favreau, R.J. Linn // Proceedings of the protocol specification, testing, and verification, VI. North-Holland, 1986. -P. 191-202.

44. Fujiwara S. Test selection based on finite state models / S. Fujiwara, G. von Bochmann, F. Khendek, M. Amalou, A. Ghedamsi // IEEE Transactions. 1991. -Vol. SE-17, No. 6.-P. 591-603.

45. Gomez R. Discrete timed automata and MONA: description, specification and verification of a multimedia stream / R. Gomez, H. Bowman // Formal techniques for networked and distributed systems Berlin, Germany, 2003. - P. 177-192.

46. Gonenc G. A method for the design of fault detection experiments // IEEE Trans, computers. 1970. - Vol. C-19, No. 6. - P. 551-558.

47. Gromov M. Deriving test suites for timed finite state machines / M. Gromov, D. Popov, N. Yevtushenko // Proceedings of IEEE East-west design & test symposium. 2008. - P. 339-343.

48. Hartmanis J. Algebraic structure theory of sequential machines / J. Hartmanis, R. Stearns. New York: Prentice-Hall, 1966. - 210 p.

49. Hennie F.C. Fault detecting experiments for sequential circuits // Proceedings of the 5th Annual symposium on switching circuit theory and logical design. 1964. -P. 95-110.

50. Hierons R.M Testing from a stochastic timed system with a fault model / R.M. Hierons, M.G. Merayo, M. Nunez // Journal of logic and algebraic programming. 2009. - Vol. 72(8). - 98-115.

51. Kam T. Synthesis of finite state machines: functional optimization / T. Kam and etc.. Boston, MA, USA: Kluwer Academic Publishers, 1997 - 282 p.

52. Khoumsi A. Test cases generation for nondeterministic real-time systems / A. Khoumsi, T. Jeron, H. Marchand // Formal approaches to software testing. -2003.-Vol. 2931.-P. 131-146.

53. Koufareva I. Test generation driven by user-defined fault models / I. Koufareva, A. Petrenko, N. Yevtushenko. // Testing of communicating systems: methods and applications. Hungary, 1999. - P. 215-223.

54. Krichen M. Conformance testing for real-time systems / M. Krichen, S. Tripakis // Formal methods in system design. 2009. - Vol. 34, No. 3. - P 238-304.

55. Laroussinie F. CMC: a tool for compositional model-checking of real-time systems / F. Laroussinie, K. Larsen // Formal description techniques and protocol specification, testing and verification. 1998. - P. 439-456.

56. Lee D. Conformance testing of protocols specified as communicating finite state machines a guided random walk based approach / D. Lee, K.K. Sabnani, D.M. Kristol, S. Paul // IEEE Transactions on communications. - 1996. -Vol. 44(5). - P. 631-640.

57. Lee D. Principles and methods of testing finite state machines a survey / D. Lee, M. Yannakakis // Proceedings of the IEEE. - 1996. - Vol. 84(8). - P. 1090-1123.

58. Lynch N. An introduction to input/output automata / N. Lynch, M. Tuttle // CWI Quarterly. 1989. - Vol. 2. - P. 219-246.

59. Lynch N. Hybrid i/o automata. Hybrid systems III. / N. Lynch, R. Segala,

60. F. Vaandrager, H.B. Weinberg // Lecture notes in computer science 1996. -Vol. 1066.-P. 496-510.

61. Mammar A. A systematic approach to integrate common timed security rules within a TEFSM-based system specification / A. Mammar, W. Mallouli, A. Cavali // Information and software technology. 2012. - Vol. 54(1). - P. 8798.

62. Mattiello-Francisco F. InRob: An approach for testing interoperability and robustness of real-time embedded software / F. Mattiello-Francisco, E. Martins, A. Cavalli, E.T. Yano // Journal of systems and software. 2012. - Vol. 85. -P. 3-5.

63. Morales G. Timed extended invariants for the passive testing of web services /

64. G. Morales, S. Maag, A. Cavalli, W. Mallouli, E.M. de Oca, B. Wehbi // IEEE International conference on web services. 2010. - P. 592-99.

65. Merayo M.G. Extending EFSMs to specify and test timed systems with action durations and time-outs / M.G. Merayo, M. Nunez, I. Rodriguez // IEEE Transactions on computers. 2008. - Vol. 57(6). - P. 835-844.

66. Merayo M.G. Formal testing from timed finite state machines / M.G. Merayo, M. Nunez, I. Rodriguez // Computer networks. 2008. - Vol. 52(2). - P. 432460.

67. Petrenko A. Test suite generation for a given type of implementation errors /tV\

68. A. Petrenko, N. Yevtushenko // Proceedings of IFIP 12 International conference on protocol specification, testing and verification. 1992. - P. 229-243.

69. Petrenko A. Fault models for testing in context / A. Petrenko, N. Yevtushenko, G. von Bochmann // Formal techniques for networked and distributed systems. -1996.-P. 163-178.

70. Poage J.F. Derivation of optimal test sequences for sequential machines /th

71. J.F.Poage, E.J. McCluskey Jr. // Proceedings of the IEEE 5 Symposium on switching circuits theory and logical design. 1964. - P. 121-132.

72. Ru Dai Z. Timed TTCN-3 A real time extension for TTCN-3 / Z. Ru Dai, J. Grabowski, H. Nuekirchen // Testing of communicating systems XIV. - 2002. -P. 407-425.

73. Sabnani K. A protocol test generation procedure / K. Sabnani, A. Dahbura // Computer networks and ISDN systems. 1988. - Vol. 15, No. 4. - P. 285-297.

74. Simao A. Generating reduced tests for FSMs with extra states / A. Simao, A. Petrenko, N. Yevtushenko // Lecture notes in computer science. 2009. -Vol. 5826-P. 129-145.

75. Sollins K. RFC 1350 The TFTP protocol (revision 2) Электронный ресурс. // Internet FAQ archives : online education. - Электрон, текст, дан. - URL: http://www.faqs.org/rfcs/rfcl350.html (дата обращения: 04.09.2011).

76. Springintveld J. Testing timed automata / J. Springintveld, F. Vaandrager, P. D'Argenio // Theoretical computer science. 2001. - Vol. 254 - P. 225-257.

77. Starke P.H. Abstract automata / P.H. Starke North-Holland: American Elsevier, 1972.-419 p.

78. Tan Q.M. Test generation for specifications vodeled by input/output automata / Q.M. Tan, A. Petrenko // The Proceedings of the IFIP 11th International workshop on testing of communicating systems. Deventer, Netherlands, 1998. - P. 83100.

79. Tretmans J. Test generation with inputs, outputs and quiescence // Proceedings of the 2nd International workshop on tools and algorithms for construction and analysis of systems. London, UK, 1996. - P. 127-146.

80. Tretmans J. Model based testing with labelled transition systems // Formal methods and testing. Lecture notes in computer science. 2008. - Vol. 4949 -P. 1-38.

81. Tripakis S. Folk theorems on the determinization and minimization of timed automata // Formal modeling and analysis of timed systems. Lecture notes in computer science. 2004. - Vol. 2791. - P. 182-188.

82. Vuong S.T. The UlOv-method for protocol test sequence generation / S.T. Vuong, W.W. L. Chan, M.R. Ito // Proceedings of the 2nd IFIP International workshop on protocol test systems. 1989. - P. 161-175.

83. Walter T. Real-time TTCN for testing real-time and multimedia systems / T. Walter, J. Grabowski // The proceedings of the International workshop on testing of communicating systems. 1997. - Vol. 6. - P. 37-56.

84. Zhigulin M. FSM-Based Test Derivation Strategies for Systems with Time-Outs / M. Zhigulin, N. Yevtushenko, S. Maag, A. Cavalli // 11th International conference on quality software. Madrid, 2011. - P. 141-150.