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

кандидата технических наук
Коломеец, Антон Владимирович
город
Томск
год
2010
специальность ВАК РФ
05.13.01
Диссертация по информатике, вычислительной технике и управлению на тему «Алгоритмы синтеза проверяющих тестов для управляющих систем на основе расширенных автоматов»

Автореферат диссертации по теме "Алгоритмы синтеза проверяющих тестов для управляющих систем на основе расширенных автоматов"

004610145

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

Коломеец Антон Владимирович

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

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

Автореферат

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

Томск-2010 ^^ ^^

004610145

Работа выполнена на кафедре информационных технологий в исследовании дискретных структур ГОУ ВПО «Томский государственный университет»

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

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

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

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

Защита состоится 4 октября 2010 года в 10.30 па заседании диссертационного совета Д 212.267.12 при ГОУ ВПО «Томский государственный университет» по адресу: 634050, г. Томск, пр. Ленина, 36, II уч. корпус, ауд. 212 б.

С диссертацией можно ознакомиться в Научной библиотеке ГОУ ВПО «Томский государственный университет» по адресу: 634050, г. Томск, пр. Ленина, 34а.

Автореферат разослан 10 сентября 2010 г.

кандидат технических наук, доцент Громаков Евгений Иванович

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

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

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

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

Актуальность проблемы. Построение качественных проверяющих тестов для дискретных управляющих систем, в частности, для текоммуиикационных протоколов, является актуальной технической задачей. Для построения проверяющего теста с гарантированной полнотой необходимо иметь, в первую очередь, адекватную математическую модель поведения системы и ошибки (неисправности). Классические хорошо изученные модели, такие как-конечный автомат, полуавтомат, входо-выходной полуавтомат имеют слишком большое число состояний (и переходов), что затрудняет их использование для решения практических задач. Кроме того, эти модели описывают не все аспекты поведения управляющей системы, например, не описывают ситуации, когда область определения некоторого параметра (например, временной переменной) бесконечна. Поэтому в настоящее время активно исследуется вопрос о построении тестов с гарантированной полнотой на основе более компактных моделей, одной из которых является расширенный автомат. Модель расширенного автомата достаточно часто используется при описании телекоммуникационных протоколов, в частности, расширенный автомат достаточно просто построить по описанию поведения в языке SDL или If или UML. Однако практически все методы синтеза тестов для расширенных автоматов доставляют проверяющие тесты, полнота которых остается неизвестной, и соответственно разработка методов синтеза проверяющих тестов с гарантированной полнотой для расширенных автоматов является актуальной задачей.

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

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

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

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

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

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

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

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

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

1. Проект TAROT в рамках 6й рамочной программы ЕС «Мобильность молодых ученых», 2003 - 2007 гг.

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

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

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

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

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

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

Апробация работы. Все теоретические и практические результаты, составившие основу диссертационной работы, по мере их получения обсуждались на семинаре кафедры информационных технологий в исследовании дискретных структур радиофизического факультета ТГУ. Кроме того, результаты работы докладывались на следующих научных конференциях: Российской конференции с международным участием «Новые информационные технологии в исследовании дискретных структур» (Томск, 2003 и 2008, Иркутск, 2004, Шушенское, 2006), международной научной студенческой конференции «Студент и научно - технический прогресс» (Новосибирск, 2004 и 2006), на международной конференции по

тестированию программного обеспечения, 1С8Т'2008, (Лиллехаммер, Норвегия, 2008)

Структура и объем работы. Диссертация состоит из введения, 4 глав, заключения и списка используемой литературы. Диссертация содержит 11 рисунков и 3 таблицы. Объем диссертации составляет 108 страницы, в том числе: титульный лист - одна страница, оглавление -две страницы, основной текст — 96 страницы, библиография из 88 наименований - 11 страницы, приложение - 21 страниц.

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

СОДЕРЖАНИЕ РАБОТЫ Во введении дается общая характеристика работы, обосновывается актуальность исследований, определяется тематика и формулируется цель работы, кратко излагаются основные задачи и результаты, выносимые на защиту.

Первая глава посвящена основным понятиям и обозначениям, относящимся к конечным и расширенным автоматам, и, кроме того, содержит обзор известных методов по синтезу проверяющих тестов для расширенных автоматов; Под конечным автоматом {или просто) автоматом понимается пятёрка $ = (Б, I, О, во), где 5 - непустое конечное множество состояний с выделенным начальным состоянием ¿о, I - непустое конечное множество входных символов, называемое входным алфавитом, О - непустое конечное множество выходных символов, называемое выходным алфавитом, с /х 5 х 5х О -отношение поведения. В данной работе мы рассматриваем инициальные автоматы, то есть автоматы с фиксированным начальным состоянием; такие автоматы описывают поведение систем, обладающих сигналом сброса. Инициальному автомату можно сопоставить специальную словарную функцию, которая описывает отображение входных слов (слов во входном алфавите) в выходные слова. Если каждому входному слову соответствует единственное выходное слово, то автомат называется детерминированным: в противном случае автомат называется недетерминированным.

Формально под расширенным автоматом М понимается пятерка (5, X, Г, Т, Г7), где Я - непустое конечное множество состояний

автомата, X - непустое множество входных символов, называемое входным алфавитом, У - непустое множество выходных символов, называемое выходным алфавитом, V - конечное, возможно, пустое множество контекстных переменных, Т - множество переходов между состояниями из 5.

Каждый переход / из множества Т есть семёрка (.?, х, Р, ор, у, ир, л'), где л и я' принадлежат множеству состояний $ и являются начальным и конечным состояниями перехода; .х е X есть входной символ и обозначает множество входных векторов, компонентами которых являются значения параметров, соответствующих входному символу х (далее входные параметры); у е 1' - выходной символ, и Оаи,у обозначает множество выходных векторов, компонентами которых являются значения параметров, соответствующих выходному символу у (далее выходные параметры); Р, ар и ир - функции, определенные над входными параметрами и контекстными переменными из V:

- Р: Д„;>* х Ву -> {Истина, Ложь} - предикат, где Оу- множество контекстных векторов, то есть векторов, компонентами которых являются значения контекстных переменных;

- ор : В1прх х О у -> йт/у - функция вычисления выходного параметра;

- ир : Д„рХ х О у Оу - функция вычисления значения контекстной переменной.

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

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

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

При построении тестов с гарантированной полнотой необходимо ввести модель неисправности. Во второй главе рассматриваются модели ошибок для расширенного автомата. Модель неисправности <Н, БиЬ{НН)>, как обычно, содержит три компоненты, а именно, эталонное поведение, которое представляется детерминированным полностью определенным расширенным автоматом (спецификацией Н), отношение конформности или соответствия, и область неисправности, то есть множество проверяемых систем, поведение каждой из которых также описано расширенным автоматом. В данной работе отношением конформности является отношение эквивалентности г, и область неисправности 5иЬ (НИ) совпадает с множеством всех полностью определенных подавтоматов специального мутационного автомата ИИ. Посредством моделирования по мутационному расширенному автомату строится

конечный мутационный автомат. Если такой конечный автомат существует, то задача синтеза проверяющих и диагностических тестов сводится к задаче синтеза таких тестов но мутационному конечному автомату, то есть по модели неисправности <АМ, =, 8иЬ{ Ат1)>.

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

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

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

Вход: Полностью определенный детерминированный связный конечный автомат М- (М, 1, О, Т', .у0), который определяет возможные

переходы в мутационном автомате; приведенная форма 5 автомата (М, I, О, Г', 5о).

Выход: Полный проверяющий тест относительно модели неисправности 2,

Полагаем./: = 1, В: = М х I.

Шаг 1. Если множество В не является пустым, то в множество Дг заносим максимальное число пар (т, г) е В таких, что частичный подавтомат автомата И после удаления всех переходов, соответствующих этим парам, остается связным.

./44-

Если множество В = 0, то Шаг 2.

Шаг 2. Пусть тс = {Ви ..., Вк} есть разбиение множества переходов расширенного автомата на классы.

Пока У < Л:

Строим мутационный автомат ИН;. для каждой пары (/я, /) е Д/ добавляем все переходы (т, г, о, т'), о е О, т' е »г,

Строим полный проверяющий тест Г.?/ относительно модели <5, БиЪ{НН)>\

./4-4-;

Шаг 3. 73 = ига,.

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

Конец.

Теорема 1. Проверяющий тест 75, доставляемый алгоритмом 2.2, является полным относительно модели неисправности ^иЬ(Щ).

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

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

2. По мутационному расширенному автомату строится эквивалентный конечный автомат.

3. Полученный эквивалентный конечный автомат проверяется на связность.

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

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

Для упрощения решения задачи достижимости в расширенном автомате, мы предлагаем построить срез Slice ;<(М), который сохраняет свойства достижимости исходного расширенного автомата М. Мы называем такой срез R-срезом и для его построения предлагаем следующий алгоритм.

Алгоритм 2 построения Л-среза расширенного автомата

Вход: Расширенный автомат Н

Выход: Срез Slice ¡¿М) автомата И

Шаг 1: Переменная v, удаляется из множества контекстных переменных V, если ни одна из свободных переменных любого предиката расширенного автомата не зависит от переменной vt. Другими словами, удаляются все контекстные переменные, не влияющие на выполнимость предикатов. Пусть У с V есть сокращенное множество контекстных переменных.

Шаг 2: Если на некотором переходе функция определения значения контекстной переменной зависит от некоторой переменной

из множества У\У, то данное соотношение удаляется из расширенного автомата.

Шаг 3: Если существует переход в расширенном автомате К на котором функция определения выходного параметра зависит от контекстной переменной из множества (АV, то данное соотношение удаляется из расширенного автомата. Соответствующему выходному параметру присваивается любое допустимое значение. Конец.

Удаление контекстных переменных, от которых не зависит ни один из предикатов расширенного автомата, не влияет на достижимость состояний. Поэтому справедливо следующее утверждение. Пусть И - расширенный автомат и его срез БИсг^И) получен по алгоритму 2.

Теорема 2. Если параметризованная входная последовательность а переводит расширенный автомат ¿7/сеЛ(//) из начального состояния я в состояние й', то последовательность а также переводит автомат М из начального состояния ^ в состояние s'. Более того, если под действием параметризированного входного символа (х,р) в автомате БИсея(А) выполним переход ; = (.¡¿с,Р,ор',у',ир',.<,'), то под действием параметризированного входного символа (х,р) выполним соответствующий переход в автомате М.

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

Идея построения среза состоит в удалении переходов, на которых предикат зависит от контекстных переменных, т.е. переходов, выполнение которых зависит от значений контекстных переменных. Тем не менее, некоторые переходы, имеющие предикаты, зависящие от контекстных переменных можно сохранить, воспользовавшись следующим свойством. Пусть, например, Р есть дизъюнкция предикатов Л и Р2, и предикат Л не зависит от контекстных переменных. Тогда переход с предикатом Р будет возбужденным, если для заданных значений входных параметров предикат 1\ принимает значение «ИСТИНА». В общем случае такая замена предиката возможна, если предикат Р можно представить в виде суперпозиции предикатов Рх и Ръ Р = _/ГРь Рг), из которых предикат зависит только от входных параметров, иЛ\, 0) = 1) = 1. В этом случае

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

Алгоритм 3 построения FSM-среза расширенного автомата

Вход: Расширенный автомат И

Выход: Конечно автоматный срез SliceFSM(И) автомата М

Шаг 1: Из расширенного автомата М удаляются все переходы, на которых предикат зависит только от контекстных переменных. Если предикат Р можно представить в виде композиции предикатов Р1 и Р2, Р = j{Pu Р2), из которых предикат Р] зависит только от входных параметров и_Д1, 0) =J[l, 1) = 1, то предикат Р заменяется предикатом

Л-

Шаг 2: Из полученного расширенного автомата удаляются все контекстные переменные и функции вычисления контекстных переменных (up).

Шаг 3: Из полученного расширенного автомата удаляются все выходные параметры и соответствующие функции вычисления выходных параметров (ор). Полученный автомат обозначается Slices///). Конец.

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

Различающим автоматом (frjs ® Игlq)/(s,q) контекстно-свободных расширенных автоматов HJs и H-Jq называется наибольший связный подавтомат расширенного автомата <(SxQ)ufail, X, Yyjfail, Т>, где S - множество состояний автомата //,, Q- множество состояний автомата Мъ fail £ S х Q - специальное состояние и специальный выходной символ, X и Y - входной и выходной алфавиты, на которых определены автоматы Их и Нг. Множество переходов различающего автомата определяется следующим образом. Для каждой пары состояний (s, q) е S х Q и для каждой пары переходов из состояний s и q по входному символу х, который определен в каждом из состояний s и с/, с предикатами Р и R, проверяем, является предикат (Р & R) выполнимым, то есть проверяем, существует ли набор значений

входных параметров, на котором предикат (Р & К) принимает значение «Истина». Если такой набор р существует и выходной символ b на этих переходах один и тот же, то в автомате (ffjs ® Milq)l{s,q) есть переход (s, q) —> (х, р)/ Ъ --> (s', q'). Если выходные символы на

переходах из состояний i и q по входному символу х, с предикатами Р и R, не совпадают, то в различающем автомате существует переход (s, q) —* (х, p)//ail -* fail.

На основе R- и FSM-срезов можно предложить следующий алгоритм построения проверяющего теста для расширенного автомата.

Алгоритм 4 построения проверяющего теста для проверки ошибок переходов/выходов на выделенном подмножестве переходов расширенного автомата

Вход: Расширенный автомат Н и подмножество Е переходов этого автомата, подлежащих проверке, число к, определяющее длину параметризированной входной последовательности, которая будет строиться по Л-срезу Slice R(M)

Выход: Тест, проверяющий наличие одиночных ошибок переходов/выходов на подмножестве Е переходов (если такой тест можно построить на основе Л-среза и среза SliceFSi¿ftj)

Шаг 1: Строятся FSM-срез Slice и Л-срез Slice ¡¿И), TS=0. Шаг 2: Рассматривается каждый переход t = (s,x, Р, op, у, up, s) из множества Е. Если в FSM-срезе Sliceсостояние s достижимо из начального состояния по параметризированной входной последовательности а и существует переход из состояния ,v под действием входного символах, то ах заносится в тест TS, и Шаг 3.

Если состояние s недостижимо в FSM-срезе, то посредством моделирования Л-среза проверяется, можно ли построить последовательность а длины к, переводящую Я-срез из начального состояния в состояние s, после которой выполним переход t. Последовательность сих заносится в тест TS, и Шаг 3. Если состояние 5 недостижимо в й-срезе по последовательности длины к, то переходим к проверке следующего перехода.

Шаг 3: На основе алгоритма 3 проверяется, с какими состояниями различимо состояние У в FSM-срезе и строится множество Ws различающих последовательностей. В тест TS заносятся последовательности axWs ■

Шаг 4: Если рассмотрены все переходы из множества Е, то из множества TS удаляются последовательности, которые являются

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

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

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

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

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

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

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

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

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

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

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

Список публикаций по теме диссертации

1. Громов М.Л., Евтушенко Н.В., Коломеец A.B. К синтезу условных тестов для недетерминированных автоматов // Программирование. - 2008. - № 6. - С. 1-11.

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

3. Коломеец А.В., Прокопенко С.А. Метод синтеза диагностических тестов для расширенных конечных автоматов // Вестник ТГУ. Приложение. -2003. -№ б. - С. 174-177.

4. Коломеец A.B. ¿Метод синтеза проверяющих тестов для расширенных конечных автоматов // Студент и научно-технический прогресс. Информационные технологии : материалы XL5I международной научной студенческой конференции. - Новосибирск, 2004.-С. 174-176.

5. Громов М.Л., Коломеец A.B., Евтушенко Н.В. Синтез диагностических тестов для автоматных сетей // Вестник ТГУ. Приложение. - 2004. - № 9 (1). - С. 204-209.

6. Коломеец A.B. Экспериментальное исследование диагностических тестов для локализации одиночных выходных ошибок и ошибок переходов в расширенных автоматах // Наука. Технологии. Инновации : материалы всероссийской научной конференции молодых ученых : в 7 ч. - Новосибирск : Изд-во НГТУ, 2006. -Ч. 1.-С. 238-240.

7. Коломеец A.B., Шабалдин A.B., Спицина Н.В. Автоматизация тестирования реализаций протоколов прикладного уровня в лабораторном практикуме И Современные средства и системы автоматизации : материалы IV научно-практической конференции. - Томск : Изд-во ТУСУР, 2003. - С. 222-225.

8. Коломеец A.B., Прокопенко С.А. Соответствие между ошибками в программных реализациях протоколов и расширенных автоматах//Вестник ТГУ. Приложение.-2005.-№ 14.-С. 154-157.

9. Коломеец A.B., Прокопенко С. А. Метод синтеза проверяющих тестов для расширенных автоматов без построения эквивалентного конечного автомата // Вестник ТГУ. Приложение. -2006. -№ 18.-С. 62-66.

Ю.Михайлов Ю.В., Коломеец A.B. Автоматизация внесения ошибок в программные реализации протоколов на основе модели расширенного автомата // Наука. Технологии. Инновация : материалы всероссийской научной конференции молодых ученых : в 7 ч. -Новосибирск : Изд-во НГТУ, 2006. - Ч. 1. - С. 49-51.

11.El-Fakih К., Kolomeez A., Prokopenko S., Yevtushenko N. Extended Finite State Machine Based Test Derivation Driving By User Defined Faults // International Conference ICST'2008 / IEEE. - 2008. -P. 308-317.

12. Михайлов Ю.В., Коломеец A.B. Проверка переходов в расширенном автомате на основе срезов // Вестник ТГУ. Управление, вычислительная техника и информатика. - 2008. - № 3 (4). -С.110-118.

Тираж 120 экз. Отпечатано в ООО «Позиггив-НБ» 634050 г. Томск, пр. Ленина 34а

Оглавление автор диссертации — кандидата технических наук Коломеец, Антон Владимирович

Введение.

1. Основные определения.

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

1.2. Расширенные автоматы.

1.3. Построение эквивалентного конечного автомата.

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

1.4.1 Модели неисправности и тесты для конечных автоматов.

1.4.2. Проверяющие тесты.

1.5. Обзор методов по синтезу тестов для расширенных автоматов.

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

2. Модели неисправности на основе мутационного расширенного автомата.

2.1. Модель неисправности на основе мутационного расширенного автомата.

2.2. Ошибки в расширенном автомате.

2.2.1 Выходные неисправности.

2.2.2. Ошибки переходов.

2.2.3. Предикатные ошибки.

2.2.4. Ошибки присвоения.

2.3. Тестирование на основе мутационного автомата.

2.4. Основные результаты главы 2.

3. Синтез тестов для расширенного автомата на основе срезов.

3.1. Построение среза расширенного автомата с сохранением достижимости состояний.

3.2. Построение РБМ-среза расширенного автомата.

3.3. Построение различающего автомата для двух контекстно-свободных расширенных автоматов.

3.4. Алгоритм построения проверяющего теста для проверки ошибок переходов/выходов на выделенных переходах расширенного автомата.

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

3.6. Построение проверяющего теста на основе эквивалентного конечного автомата с ограничением на число состояний.

3.7. Основные результаты главы 3.

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

4.1. Соответствие между программными ошибками и ошибками в расширенном автомате.

4.1.1. Тесты, построенные по расширенному автомату для проверки ошибок переходов.

4.1.2. Тесты, построенные по расширенному автомату для проверки ошибок выходов.

4.1.3. Тесты, построенные по расширенному автомату для проверки предикатных ошибок.

4.1.4. Тесты, построенные по расширенному автомату для проверки ошибок присвоения.

4.1.5. Более сложные ошибки.

4.2. Генерация программных реализаций на основе модели расширенного автомата.

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

4.4. Основные результаты главы 4.

Введение 2010 год, диссертация по информатике, вычислительной технике и управлению, Коломеец, Антон Владимирович

Актуальность проблемы. Построение качественных проверяющих тестов для дискретных управляющих систем является актуальной технической задачей. Для построения проверяющего теста, с гарантированной полнотой необходимо иметь, в первую очередь, адекватную математическую модель протокола и ошибки (неисправности). Классические хорошо изученные модели, такие как конечный автомат [1], полуавтомат, входо-выходной полуавтомат [2] имеют слишком большое число состояний (и переходов), что затрудняет их использование для решения практических задач. Кроме того, эти модели описывают не все аспекты поведения протокола, в частности, не описывают ситуации, когда область определения некоторого параметра (например, временной переменной) бесконечна. Поэтому в настоящее время активно исследуется вопрос о построении тестов с гарантированной полнотой на основе более компактных моделей, таких как расширенный автомат [3], временной автомат. Модель расширенного автомата достаточно часто используется при описании технических систем, в частности, расширенный автомат достаточно просто построить по описанию технической системы в языке SDL [4] или If или UML [5]. Однако практически все известные методы синтеза тестов для расширенных и временных автоматов доставляют проверяющие тесты, полнота которых остается неизвестной. Синтез проверяющих тестов с гарантированной полнотой требует дополнительных исследований, которые в данной работе проводятся для модели расширенного автомата. Таким образом, разработка методов синтеза проверяющих тестов с гарантированной полнотой для расширенных автоматов является актуальной задачей.

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

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

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

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

2. Предложено понятие среза расширенного автомата. Предложены три среза расширенного автомата и алгоритм построения проверяющего теста с гарантированной полнотой на их основе.

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

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

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

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

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

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

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

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

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

1. 6™ рамочная программа TAROT «Мобильность молодых ученых», 2003-2007 гг.

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

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

Апробация работы. Все теоретические и практические результаты, составившие основу диссертационной работы, по мере их получения обсуждались на семинаре кафедры информационных технологий в исследовании дискретных структур радиофизического факультета ТГУ. Кроме того,1 результаты работы докладывались на научных конференциях: всероссийской конференции с международным участием «Новые информационные технологии в исследовании дискретных структур» (Томск, 2003 и 2008 гг., Иркутск, 2004 г., Шушенское, 2006 г.), международной научной студенческой конференции^ «Студент и научно - технический прогресс» (Новосибирск, 2004 и 2006 гг.), на международной конференции по тестированию программного обеспечения, ICST'2008, (Лиллехаммер, Норвегия, 2008 г.)

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

1. Коломеец A.B., Прокопенко С.А. Метод синтеза диагностических тестов для расширенных конечных автоматов // Вестник ТГУ. Приложение. -2003.-№6. -С. 174-177.

2. Коломеец A.B. Метод синтеза проверяющих тестов для расширенных конечных автоматов // Студент и научно - технический прогресс. Информационные технологии : материалы XLII международной научной студенческой конференции. - Новосибирск. - 2004. - С. 174-176.

3. Громов М.Л., Коломеец A.B., Евтушенко Н.В. Синтез диагностических тестов для автоматных сетей // Вестник ТГУ. Приложение. - 2004. - № 9 (I). - С. 204-209.

4. Коломеец A.B. Экспериментальное исследование диагностических тестов для локализации одиночных выходных ошибок и ошибок переходов в расширенных автоматах // Наука. Технологии. Инновации : материалы всероссийской научной конференции молодых ученых в 7 ч. Новосибирск : Изд-во НГТУ, 2006. - Ч. 1. - С. 238-240.

5. Коломеец A.B., Шабалдин A.B., Спицына Н.В. Автоматизация тестирования реализаций протоколов прикладного уровня в лабораторном практикуме // Современные средства и системы автоматизации : материалы IV научно-практической конференции. - Томск : Изд-во. ТУ СУР, 2003. - С. 222-225.

6. Коломеец A.B., Прокопенко С.А. Соответствие между ошибками в программных реализациях протоколов и расширенных автоматах // Вестник ТГУ. Приложение. - 2005. - № 14. - С. 154-157.

7. Коломеец A.B., Прокопенко С.А. Метод синтеза проверяющих тестов для расширенных автоматов без построения эквивалентного конечного автомата // Вестник ТГУ. Приложение. - 2006. - № 18. - С.62-66.

8. Михайлов Ю.В., Коломеец A.B. Автоматизация внесения ошибок в программные реализации протоколов на основе модели расширенного автомата // Наука. Технологии. Инновация : материалы всероссийской научной конференции молодых ученых в 7 ч. - Новосибирск : Изд-во НГТУ, 2006.-Ч. 1.- С. 49-51.

9: El-Fakih К., Kolomeez A., Prokopenko S., Yevtushenko N. Extended' Finite State Machine Based Test Derivation Driving» By User Defined Faults // International Conference ICST'20087 IEEE. - 2008. - P. 308-317.

10. Михайлов Ю.В., Коломеец A.B. Проверка переходов, в расширенном автомате на основе срезов // Вестник ТГУ. Управление, вычислительная техника и информатика. - 2008. - № 3 (4). - С. 140-118.

11. Громов МЛ1, Евтушенко Н.В., Коломеец. A.B. К синтезу условных тестов для недетерминированных автоматов; Программирование. - 2008. - № 6. - С. 1-111

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

Структура и объем работы. Диссертация состоит из введения, 4 глав, заключения и списка используемой литературы. Диссертация содержит 11 рисунков и 3 таблицы. Объем диссертации составляет 108 страницы, в том числе: титульный лист - одна страница, оглавление - две страницы, основной текст - 96 страниц, библиография из 88 наименований - 11 страниц, приложение - 2 Г страница.

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

4.4. Основные результаты главы 4

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

Заключение

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

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

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

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

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

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

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

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

Библиография Коломеец, Антон Владимирович, диссертация по теме Системный анализ, управление и обработка информации (по отраслям)

1. Евтушенко, Н.В. Недетерминированные автоматы: анализ и синтез. 4.1.

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

3. Lynch, N. Hybrid I/O Automata / N. Lynch, R. Segala, F. Vaandrager, H. B.

4. Weinberg. // Hybrid Systems III. Eds. R. Alur et al. Lecture Notes in Computer Science 1066. Springer-Verlag. Berlin, Germany.- 1996.- Pp. 496-510.

5. El-Fakih, K. Fault diagnosis in extended finite state machines / K. El-Fakih, S.

6. Prokopenko, N. Yevtushenko, G. Bochmann, // In Proc. of the IFIP 15th International Conference on Testing of Communicating Systems (TestCom2003), France, Published as Lecture Notes in Computer Science 2644.- 2003.- Pp. 197-210.

7. Verilog. ObjectGEODE Simulator, Reference manual, 1997.

8. Horrocks, I. Constructing the user interface with statecharts / I. Horrocks //

9. Addison Wesley Longman Limited, Edinburg Gate, Harlow, Essex CM20 2JE, England and Associated Companies throughout the World.- 1999.- 272 p.

10. Ural, H. Test sequence selection based on static data flow analysis / H.Ural //

11. Computer communications, vol. 10, N 5.- 1987.- Pp. 234 242.

12. Chen, W.-H. Executable test sequences for the protocol data flow property / W.

13. H. Chen // Int. Conference on Formal Techniques for Networked and Distributed Systems (FORTE).- 2001.- Pp. 285-299.

14. Huang, C.-M. An executable protocol test sequence generation method for EFSM-specified protocols / Chung-Ming Huang, Yuan-Chuen Lin, Ming-Yule Yang // Intern Workshop on Ptotocol Test Systems, IWPTS'95.- 1995, Pp. 29-44.

15. Chen, W.-H. Test sequence generation from the protocol data portion based onthe selecting Chinese Postman algorithm / W.-H. Chen // Information Processing Letters, vol. 65.- 1998.- Pp. 261-268.

16. Chen, W.-H. Executable test sequence for the protocol control and data portions / W.-H. Chen // Proc. of IEEE Intern. Conf. on Communications, vol.1.- 2000.-Pp. 505-510.

17. Chen, W.-H. Automatic functional test generation using extended finite state machine model / W.-H. Chen // Proc. IEEE Design Automation Conference.-1993.-Pp. 86-91.

18. Ural, H. Test generation based on control and data dependencies within system specification in SDL / H.Ural, K.Saleh, and A.Williams // Computer Communications, vol. 23.- 2000.- Pp. 609-627.

19. Bozga, M. Using static analysis to improve automatic test derivation / M. Bozga, J.C1. Fernandez, L. Ghirvu // Software Tools and Technologie Transfer 4(2).- 2003.- Pp. 142-152.

20. Faro, A. Sequence Generation from EFSMs for Protocol Testing / A. Faro and A. Petrenko // COMNET'90.- 1990.- Pp. 17-26.

21. Wang, C.J. Generating test cases for EFSM with given fault models / C.J.Wang, M.T.Liu // Proc. IEEE INFOCOM, 1993, Pp. 774 781.

22. Cavalli, A. Hit-or-Jump: An< algorithm for embedded testing with applications to IN services / A. Cavalli, D. Lee,C. Rinderknecht, F. Zaidi // FORTE XII and PSTV XIX, China.- 1999.- Pp. 41-58.

23. El-Fakih, K. Extended Finite State Machine Based Test Derivation Driving By User Defined Faults / K. El-Fakih, A. Kolomeez, S. Prokopenko, N. Yevtushenko // International Conference ICST'2008.- 2008.- Pp. 308-317.

24. Bozga, M. Symbolic Verification for Communication Protocols / M. Bozga // PhD thesis, VERIMAG/IMAG.- 1999.- p. 137.

25. Korel, B. Slicing of state-based-models / B. Korel, I. Singh, L. Tahat, B. Vaysburg // Int. Conference on Software Maintenance.- 2003.- Pp. 34-43.

26. Weiser, M. Program slicing / M. Weiser // IEEE Trans, on Software Engineering, 10(4).- 1982.- Pp. 352-357.

27. Михайлов, Ю. В. Проверка переходов в расширенном автомате на основе срезов / Ю. В. Михайлов, А.В.Коломеец // Вестник ТГУ. Управление, вычислительная техника и информатика. 2008. - №3(4). - С. 110-118.

28. El-Fakih, К. Fault Diagnosis in Extended Finite State Machines / K. El-Fakih, S. Prokopenko, N. Yevtushenko, G. Bochmann // Lecture Notes in Computer Science, vol. 2644.- 2003,- Pp. 197-210.

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

30. Petrenko, A. Test suite generation for a FSM with a given type of implementation errors / A. Petrenko and N. Yevtushenko // In Proc. of the 12th Int. Workshop Protocol Specification, Testing and Verification.- 1992.- Pp. 229 243.

31. Bochmann, G. Protocol testing: review of methods and relevance for software testing / G. v. Bochmann, A. Petrenko // ISSTA, Seattle.- 1994.- Pp. 109-123.

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

33. Starke, P. Abstract Automata / P. Starke. // Amsterdam: North-Holland Publishing Company.- 1972.- 419 p.

34. Koufareva, I. Test generation driven by user-defined fault models / I. Koufareva, A. Petrenko, N. Yevtushenko // In Proc. of IFIP TC6 12th International Workshop on Testing of Communicating Systems, Hungary.-1999.- Pp. 215-223.

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

36. Chow, Т. S. Test design modeled by finite-state machines / T.S. Chow // IEEE Transactions on Software Engineering, 4(3).- 1978.- Pp. 178-187.

37. Fujiwara, S. Test selection based on finite state models / S. Fujiwara, G.v. Bochmann, F. Khendek, M. Amalou, A. Ghedamsi // IEEE Transactions on Software Engineering. 17(6).- 1991.- Pp. 591-603.

38. Gonenc, G. A method for the design of fault detection experiments / G. Gonenc // IEEE Trans. Computers, C-19(6).- 1970.- Pp. 551-558.

39. Hsieh, E. P. Checking experiments for sequential machines / E. P. Hsieh // IEEE Trans, on Computers, 20(10).- 1971.- Pp. 1152-1166.

40. Koufareva, I. A novel modification of W-method / I. Koufareva, R. Dorofeeva // Joint Bulletin of the Novosibirsk computing center and A.P. Ershov instituteof informatics systems. Series: Computing science, 18.- 2002.- Pp. 69-81.i

41. Lai, R. A survey of communication protocol testing / R. Lai // Journal of Systems and Software.- 2002.- Pp. 21-46.

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

43. Yao, M. Fault coverage analysis in respect to an FSM specification / M. Yao, A. Petrenko, G. Bochmann // INFOCOM'94.- 1994.- Pp. 768-775.

44. Yvtushenko, N. V. Synthesis of test experiments in some classes of automata / N. V. Yvtushenko, A. F. Petrenko // Automatic Control and Computer Sciences.- 1990.- v.24, N.4.- Pp. 50-55.

45. Vuong, S.T. The UlOv-method for protocol test sequence generation / S.T. Yuong, W.W.L. Chan, M.R. Ito // Proc. of the IFIP TC6 2nd IWPTS, North-Holland.- 1989.- Pp. 161-175.

46. Ural, H. On minimizing the lengths of checking experiments / H.Ural, X.Wu, F. Zhang // IEEE Trans, on Computers, 46(1).- 1997.- Pp. 93-99.

47. Спицына, H. Интернет программирование. Часть 1 / H. Спицына, А. Шабалдин // ТГУ, Томск.- 2002.- 30 с.

48. Petrenko, A. Fault models for testing in context / A. Petrenko, N. Yevtushenko,102

49. Sidhu, D. P. Formal methods for protocol testing: a detailed study / D. P. Sidhu and T. K. Leung // IEEE Trans, on Software Engineering, 1989.- 15(4).-Pp. 413-426.

50. Kwast, E. Automatic test generation for protocol data aspects / E.Kwast // Proc. of IFIP Intern. Symp. On Protocol Specification, Testing, and Verification.-1992.-Pp. 211-226.

51. Chanson, S.T: A unified approach to protocol test sequence generation / S.T.Chanson, J.Zhu//Proc. of INFOCOM.- 1993.- Pp. 106-114.

52. Dssouli, R. Test development for communication protocols: towards automation / R. Dssouli, K. Saleh, E. Aboulhamid, A. En-Nouaary, C. Bourfir // Computer Networks, vol. 31.- 1999.- Pp. 1835 1872.

53. ITU-T, Recommendation Z.lOO-Specification and Description Language (SDL), Geneva.- 1994.- Pp. 246.

54. Boroday, S. Techniques for Abstracting SDL Specifications / S. Boroday, R. Groz, A. Petrenko, Y.-M. Quemener // Proc. of the 3rd SAM (SDL and MSC) Workshop. LNCS, vol. 2599.- 2003,- Pp. 141-157.

55. ISO/IEC, Information processing systems, Estelle-A formal description technique based on extended state transition model, ISO 9074.- 1997.

56. Chun, W. Test case generation for protocols specified in ESTELLE / W. Chun, P. Amer // FORTE'90.- 1990.-Pp. 191-206.

57. Favreau, J.-P. Automatic generation of test scenario skeletons from protocolspecifications written in ESTELLE / J.-P. Favreau, R. J. Linn // Int. Workshop Protocol Specification, Testing and Verification (PSTV).- 1986.- Pp. 191-202.

58. Harel, D. The STATEMATE semantics of statecharts / D. Harel, A. Naamad // ACM Trans. Software Engineering and Methodolody.- 1996.- 5(4).-Pp. 293-333.

59. OMG, Unified Modelling Language, version 1.4, OMG Standard, Nov. 2002.

60. Bensalem, S. Property preserving Simulations / S. Bensalem, A. Bouajjani, C. Loiseaux, J. Sifakis // In 4th International Conference on Computer Aided Verification, volume 663 of Lecture Notes in Computer Science, SpringerVerlag:- 1992.-Pp. 11-44.

61. Lee, D. Passive testing and applications to network management / D. Lee, A.N: Netravali, K.K. Sabnani, B. Sugla, A. John // Proc. of ICNP.- 1997.-Pp. 98-114.

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

63. Cavalli, A. New approaches for passive testing using an Extended Finite State Machine specification / A. Cavalli, C. Gervy, S. Prokopenko // Journal of Information and Software Technology.-2003.- Pp. 837-852.

64. Коломеец, А. В. Метод синтеза диагностических тестов для расширенных конечных автоматов / А. В. Коломеец, С. А. Прокопенко // Вестник ТГУ. Приложение. 2003. - №6. - С. 174-177.

65. Громов, М. JI. Синтез диагностических тестов для автоматных сетей / М. JI. Громов, A.B. Коломеец, Н.В. Евтушенко // Вестник ТГУ. Приложение.- 2004. №9(1). с. 204-209.

66. Коломеец, A.B. Соответствие между ошибками в программных реализациях протоколов и расширенных автоматах / A.B. Коломеец, С.А. Прокопенко // Вестник ТГУ. Приложение. 2005. - №14. - С. 154 - 157.

67. El-Fakih, К. Extended Finite State Machine Based Test Derivation Driving By User Defined Faults / K. El-Fakih, A. Kolomeez, S. Prokopenko, N. Yevtushenko // International Conference ICST'2008. 2008. - Pp. 308-317.

68. Громов, M. JI. К синтезу условных тестов для недетерминированных автоматов / М. JL Громов, Н.В. Евтушенко, A.B. Коломеец // Программирование. 2008. - №6. - С. 1-11.

69. Куфарева, И. Б. Применение недетерминированных автоматов в задачах синтеза проверяющих тестов для систем логического управления: диссертация на соискание степени к-та. тех. наук: 05.13.01.- Томск: ТГУ,1052000.- 176 с.

70. Hierons, R. M. Mutation testing from probabilistic and stochastic finite state machines / R. M. Hierons, M. G. Merayo // Journal of Systems and Software. 82(11).- 2009.- Pp. 1804-1818.

71. Jia, Y. An analysis and survey of the development of mutation testing / Y. Jia, M. Harman // Crest Center, King's College, Londin. Technical Report TR-09-06.- 2006.-Pp. 1-31.

72. Громов, M.JI. К синтезу тестов по мутационному автомату / М.Л.Громов,

73. A.В. Коломеец, М.Ю. Дорофеева // Вестник ТГУ. Приложение. 2006. -№18. - С. 43 - 49.

74. Пархоменко, П.П. Основы технической диагностики / П.П. Пархоменко,

75. B.В. Карибский, Е.С. Согомонян, В.Ф. Халчев // М.: Энергия.- 1976.476 с.

76. Коломеец, А.В. Соответствие между ошибками в программных реализациях протоколов и расширенных автоматах / А.В. Коломеец, С.А. Прокопенко // Вестник ТГУ. Приложение. 2005, №14, С. 154 - 157.

77. Massacci, F. Logical Cryptoanalisys as a SAT Problem: the Encoding of the Data Encryption Standart / F. Massacci, L. Marraro // Dipartimento di Imformatica e Sistemistica. Universita di Roma «La Sapienza».- 1999.- Pp. 165 - 203.

78. Lantao, Z. Validation SAT solvers using an independent resolution-based checker: partical impementations and other applications / Z. Lantao, M. Sharad // Proceedings of Design, Automation and Test in Europe(DATE2003).- 2003.-Pp. 116-122.

79. Солодовников, А. С. Системы линейных неравенств / A.C. Солодовников //M.: Наука.- 1977.- 112 с.

80. Petrenko, A. Testing from Partial Deterministic FSM Specifications / A. Petrenko, N. Yevtushenko // IEEE Trans. Computers 54(9).- 2005.- Pp. 11541165.

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

82. Михайлов, Ю. В. Проверка переходов в расширенном автомате на основе срезов / Ю. В. Михайлов, А.В. Коломеец // Вестник ТГУ. Управление, вычислительная техника и информатика.-2008.- №3(4).- С. 110-118.

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