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

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

ГРОМОВ Максим Леонидович

Разработка методов синтеза условных тестов для

автоматных моделей с недетерминированным

поведением

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

автореферат

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

- 3 ДЕН 2009

Томск 2009

003486047

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

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

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

Официальные оппоненты: доктор физ.-мат. наук,

старший научный сотрудник Бурдонов Игорь Борисович

кандидат техн. наук, доцент Голубева Ольга Ивановна

Ведущая организация: Институт математики им. С.Л. Соболева СО РАН,

г. Новосибирск

Защита состоится:

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

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

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

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

профессор

В.И. Смагин

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

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

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

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

Научная новизна.

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

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

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

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

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

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

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

1. 6ая рамочная программа TAROT «Мобильность молодых учёных», 20032007 гг.

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

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

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

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

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

2. Р1еобход1шые и достаточные условия распознавания двух входо-выходных полуавтоматов условным экспериментом и представление такого условного эксперимента конечным входо-выходным полуавтоматом.

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

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

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

Результаты работы докладывались на российских и международных конференциях: «East-West Design and Test Workshop» (Одесса, 2005 и Львов, 2008); IX международном семинаре «Дискретная математика и её приложения» (Москва, 2007); Российской конферетцш с международным участием «Новые информационные технологии в исследовании сложных структур» (Иркутск, 2004 и Шушенское, 2006); международных конференциях TESTCOM-2007 (Таллин, 2007) и SYRCoSE (Санкт-Петербург, 2008).

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

Структура и объем диссертации. Диссертация состоит из введения, четырех глав, заключения и списка литературы; изложена на 152 страницах, включая 7 рисунков и список литературы из 77 наименований.

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

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

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

Под детерминированным входо-выходным полуавтоматом (или просто полуавтоматом) с входным алфавитом I и выходным алфавитом О будем понимать пятёрку

L = (L, I, О, I, Al), где L - непустое конечное множество состояний с выделенным начальным состоянием I; I и О - непересекающиеся конечные алфавиты входных и выходных действий (символов) соответственно, IVO ф 0- Отношение А¡_ С Lx (IVO) х L есть отношение переходов; если (I, а, I') € Xl и (I, а, I") £ Xl, то I' = I". Переход (/, а, I') для удобства будем записывать как I —♦ I . Состояние I полуавтомата L называется молчащим, если для любого действия а из О и любого состояшш V из L верно {I, а,/') g Ль

В данной работе мы предполагаем, что ситуацию, когда полуавтомат находится в молчащем состоянии, можно отличить от ситуации, когда полуавтомат находится в состоянии, в котором он готов произвести выходное действие. Для формального описания этой возможности вводится новое выходное действие <5, и если некоторое состояние I - молчащее, то подразумевается, что I —* I. Естественным образом отношение переходов распространяется на последовательности из алфавита (IxO U {¿}).

Введём следующие обозначения:

1. [i|„ - множество всех состояний, достижимых из состояния I по последовательности 17 £ (/ х О U {<5})*. В детерминированном полуавтомате |Ио-| < 1.

2. out(i) - множество всех выходных действий, включая S, переходы по которым определены в состоянии I.

3. in(l) - множество всех входных действий, переходы по которым определены в состояшш I.

4. s-tracesL - множество всех конечных последовательностей из (I х О х {<5})*, таких, что по ним возможны переходы из начального состояния полуавтомата L.

Полуавтомат L называется полностью определённым по входам (или просто полностью определённым), если для каждого его состояния I справедливо in(I) = I.

Полностью определённый полуавтомат L находится в отношении ioco с полуавтоматом К (обозначение: L ioco К), если для любой последовательности а из s-tracesu справедливо out([/J<7) С out([fc]7). Полуавтомат L будем называть ioco -реализацией полуавтомата К.

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

Под наблюдаемым конечным автоматом (или просто автоматом) с входным алфавитом I и выходным алфавитом О будем понимать пятёрку F = (F. 1,0, /, Ар), где F - непустое конечное множество состояний с выделенным начальным состоянием /; In О - непересекающиеся конечные алфавиты входных и выходных действий (символов) соответственно. Отношение Ар С FxIxOxF - есть отношение переходов, причём, если (f,i.o,f) 6 Ар и (/.г,о,/") 6 Ар, то /' = /". Отношение переходов естественным образом распространяется на входные и выходные последовательности, причём если (/, а, ß, /') € Xf, то пара (a,ß) называется входо-выходной последовательностью автомата в состоянии /, а ß называется выходной реакцией автомата на входную последовательность а в состоянии /.

Введем следующие обозначения:

1/1» ~ множество всех состояний, достижимых из состояния / по входо-выходной последовательности а. В наблюдаемом автомате ||/J„| i 1.

2. out (f. г) - множество всех выходных действий, переходы по которым в паре с

входным действием г определены в состоянии /.

3. ¡п(/) - множество всех входных символов, переходы по которым определены в состоянии /.

4. IV - множество всех конечных бходо-выходных последовательностей в начальном состоянии автомата Р.

Автомат Г называется полностью определенным, если для каждого его состояшш / справедливо т(/) = I.

Полностью определённый автомат Г называется квази-редукцией автомата б (обозначение Г ^ С), если для любой входо-выходной последовательности сг из Гс и любого входного символы i нз т(1з]„) верно следующее: оиЩ/],,, г) С ои^д]^, г).

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

Наблюдаемый временной автомат V (или просто временной автомат) есть шестёрка (V, I, О, г>, ДI/) , где V - конечное непустое множество состояний с выделенным начальным состоянием у,1 и О непересекающиеся конечные входной и выходной алфавиты соответственно, АуС1/х7хОхК- отношение переходов, причём, если (у,г,о,у') £ Ау и (у,¿,о,г>") е Ау, то г/ = и"; Ду : V —» V х (Ми{оо)), где N - множество натуральных чисел, причём, если Ду(и) = (у', оо), то V = к'. Как обычно,

переход (у, i, о, у') записывается как у у', а переход Ду(и) = (г>",4) - как и Д г/', и этот переход будем называть переходом по временной задержке

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

времени. Если у у', то временной автомат V, находясь в состоянии у, может принять входное воздействие г и отреагировать на него выходным действием (сигналом) о, в тот же момент временной автомат перейдёт в состояние у' и «сбросит» часы (то

есть в состоянии у' время вновь начнёт отечнтываться с 0). Если V у", и ни одно из возможных входных воздействий не прикладывается к временному автомату в течение (¿' — 1) такта после перехода временного автомата в состояние у, то в момент времени I1 временной автомат перейдёт в состояние у", и «сбросит» часы (то есть в состоянии V ' время начнёт отсчитываться с 0). Здесь мы предполагаем, что если функция Av(v) — (г),ос), то система может оставаться в состоянии v бесконечно долго.

Другими словами, если входное воздействие г подаётся на временной автомат в состоянии V в моменты времени 0, 1, 2, ..., ь' - 1, то временной автомат выдаст на выходной сигнал о и мгновенно изменит своё состояние на состояние у'. Однако, если воздействие г на временной автомат в состоянии у будет подано в момент I' или позже, то временной автомат примет его, находясь уже не в состоянии и, а в состоянии у", поскольку в момент времени временной автомат, руководствуясь переходом

у у", перейдёт в состояние у". При этом временной автомат «сбросит» часы, и воздействие, поданное в момент времени ¿', поступит на временной автомат в состоянии у" в момент времени 0.

Временным входным воздействием назовём пару (г, I) е / х 2р", где 2ц - множество целых неотрицательных чисел. Пара (г, означает, что входное воздействие г подано на временной автомат в момент времени £, считая от момента перехода временного автомата в состояние у.

Чтобы определить выходную реакцию временного автомата в состоянии у на входное временное воздействие (¿,4), пеобходимо определить такое состояние у', в которое временной автомат попадёт из состояния V за время используя переходы по временным задержкам. Затем, согласно отношению переходов, найти переход из состояния у' по входному воздействию г, то есть переход у' у". Выходная реакция о будет выходной реакцией временного автомата в состоянии у на временное входное воздействие (¿, (), а состояние у" - конечным состоянием перехода по временному входному воздействию {г, £}. Понятие переходов по временным входным воздействиям есте-ственш.ш образом распространяется на временные входные и выходные последовательности, причём если у у', где а € (I X Жд х О)', то а называется временной входо-выходной последовательностью временного автомата в состоянии у.

Введём следующие обозначения:

1. И, - множество всех состояний, достижимых из состояния у по временной входо-выходной последовательности а.

2. ои(;(г>, г) - множество всех выходных символов о 6 О, для каждого из которых существует такое у' € V, что (?;, г, о, V1) £ Ау.

3. оиЦ^, (г, 4)) - множество всех выходных реакций временного автомата на временное входное воздействие (г, 4) в состоянии у.

4. ¡п(г1) - множество всех входных действий, переходы по которым определены в состоянии и.

5. 1пх(у) - множество всех временных входных действий, переходы по которым определены в состоянии у.

6. Гу - множество всех конечных времетпых входо-выходных полседовательно-стей временного автомата V в начальном состоянии.

Временной автомат V называется полностью определённым, если для каждого его состояния у справедливо тх(и) = I.

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

Вторая глава посвящена различающим уставным экспериментам с конечными автоматами.

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

Пересечением двух автоматов и 6 называется автомат Н = Г П С = (Н, 1,0, к,\н), где к = {/. у), Н С рх <3 - минимальное множество, полученное

с использованием следующего правила для \ц- если (/, г, о, /') € Ар и {</, г, о, 6 А с, TO ({f,g),i,o,(f',g'))eXF.

Ми вводим понятие r-различающего автомата, который будет представлять условный эксперимент по распознаванию двух r-различимых автоматов Под г-различающим автоматом понимается автомат R — {R, ItO,f, Ar) , для которого справедливы следующие условия:

1. Д Э {_Lf,Xg,±}.

2. Граф переходов автомата R - ациклический,

3. Для всякого г € Ä\ {±f,-Lc,-L} выполняется |in(r)| = 1 ц out (г, г) = О, где in(r) = {г}-

4. Состояния ±f, -Lg и J_ - тупиковые.

Говорят, что r-различающий автомат R различает автоматы F и G, если в пересечении Hfr — F П R для всех тупиковых состояний {/, г), верно г = _Lf, в то время как в пересечении Hgr = G П R для всех тупиковых состояний {д, г), верно г = ±с.

Пусть для распознавания предъявлены автоматы F и G, для которых существует r-различающий автомат Rfg- Условный эксперименте использованием автомата Rfg строится следующим образом. В начальный момент времени автомат Rfg находится в начальном состоянии г.

Пусть автомат Rfg перешёл в состояние г, в котором определён переход по входному символу г 6 I- В этом случае на предъявленный для распознавания автомат подаётся входной символ i. Предъявленный автомат реагирует на входной символ некоторым выходным символом о 6 О, на основании которого вычисляются следующее состояние г-различающего автомата Rfg и следующий входной символ.

Эксперимент заканчивается, как только r-различающий автомат переходит в одно из специальных состояний _Lf, -Lg или _L. Если r-различающий автомат Rfg достиг состояния _Lf, то предъявленный автомат распознаётся как автомат F; если r-различающий автомат Rfg достиг состояния _Lg, то предъявленный автомат распознаётся как автомат G. Если автомат Rfg достиг состояния J_, то предъявленный автомат не является ни автоматом F, ии автоматом G. Поскольку граф переходов автомата Rfg ациклический, то условный эксперимент на основе г-различающего автомата является конечным.

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

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

Пусть F и G - автоматы и Н = F П G. Состояние (/,</) € Н называется 1-недоопределённым, если существует входное воздействие г £ тр(/) П in dg) такое, что i тн({/,д))- Состояние {/, д) пересечения Н называется z-недоопределённым, z > 1, если оно (z — 1)-недоопределённое или существует входное воздействие г 6 inр(/) П indg) такое, что все состояния пересечения Н, достижимые из {/,<?) по входному символу г, являются (z — 1)-недоопределёнными.

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

Алгоритм 1 Построение г-различающего автомата

Вход: Два наблюдаемых автомата F = {F, 2, О, /, Ар) иС = (G, I, О, д, Ас)-Выход: Я-различающий автомат Rгс■ если F н G - г-различимы. 1: Яо := {X, J-F, -1с}; Ar := 0; Н := Fn G;

2: Строим Qi - множество 1-недоопределённых состояний, Q2 - 2-недоопределённых состояний и

так далее пока Qj ф Qj+i. 3: Если Vj (/, д) gQj, то

4: Исходные автоматы не r-различимы; Конец. 5: Пусть и - такое число, что {/, д) 6 Q„, но </,s) £ Qn-1; 6: г := п.; Я„ := {(/,д)}'> := 0-, Я„_2 0; ...; Hi : = 0;

7: Пока (г > 0)

8: Для каждого (h = (/, й) 6 Яг)

9: Выберем такое произвольное t € *тя(/) ninc(ff), что для всех о € О выполняется [/ф/о С

10: Для каждого о £ 0\ (outp(/, г)LJoutc(sf, *)) Добавим в множество Ar переходы {h, i, о, J.); 11: Для каждого о 6 outp(/, i) \outc(<7,i) добавим в множество Ar переходы i-p);

12: Для каждого о £ outc(s,») \ o"tp(jf, i) добавим в множество Хя переходы (h, _Le); 13: Для каждого перехода (h, г, о, h') из Ан добавим в множество Ar переход (/г, г, о, /г'), а в

множество Я^/ состояние h', где z' < z - такое число , что /i' 6 Q./, но h' £ Qar_ 14: г := г - 1; 15: 11 :=

16: Автомат (Я, О, т\ Ar) - искомый автомат; Конец.

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

Тестовым примером называется наблюдаемый автомат Р = (Р, ItO,p, Ар) со следующими свойствами:

1. Р Э {Т,±}. Состояние Т соответствует вердикту «Тест пройден успешно», а _L - «Обнаружена неисправность».

2. Граф переходов автомата Р ациклический,

3. Для всякого р е Р \ {Т. ±} выполняется |in(p)| = 1 и out(p, г) = О, где in(p) =

{»}.

4. Состояния Т и _L тупиковые.

Будем говорить, что тестовый пример Р не согласуется с полностью определённым автоматом G, если в пересечении G Л Р для всех тупиковых состояний (д,р) верно р = -L. Тестовый пример Р абсолютно согласуется с полностью определённым автоматом G, если в пересечении G П Р для всех тупиковых состояний (у, р) верно р = Т.

Проверяющим тестом относительно модели (F,^, £) называется конечное множество Т тестовых примеров, входной и выходной алфавиты которых совпадают с входным и выходным алфавитом автомата-спецификации.

Проверяющий тест Т называется исчерпывающим относительно модели {F. <£), если для любого автомата G 6 £, не являющегося квази-редукцией F, множество Т содержит тестовый пример, который не согласуется с автоматом G.

Проверяющий тест Т называется непротиворечивым относительно модели (F.^. С), если любой автомат G G С, являющийся квази-редукцией автомата-спецификации F, абсолютно согласуется с каждым тестовым примером множества Т.

Проверяющий тест Т называется полным относительно модели (Р, €), если тест является исчерпывающим и непротиворечивым.

Пусть задана модель неисправности (Р, б), в которой множество £ конечно, состоит из полностью определённых автоматов, и каждый автомат из множества £ является либо квази-рсдукцией автомата Р, либо г-разл1гчим с Я. Тогда полный проверяющий тест для этой модели неисправности молено построить следующим образом.

Выбираем очередной автомат <? 1гз множества неисправностей £ и применяем к автоматам Р и б алгоритм 1. Если вердикт этого алгоритма «Автоматы Гиб т-совместимы», то переходим к следующему автомату из Если автоматы Р и С г-различимы, то алгоритм построит автомат /?, г-различагащий автоматы Г и й. Отождествив состояние с состоянием Л. и переобозначив состояние как состояние Т, получим тестовый пример Р для обнаружения автомата С, который заносим в тест. Затем переходим к следующему автомату из £ и так далее.

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

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

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

Два полуавтомата (.и К назовём ¡осо-совместимыми ('юсо-разлччимыми), если для них существует {не существует) общая полностью определённая 1осо-реализация.

Пересечением полуавтоматов ¿.и К назовём полуавтомат J = /1 Г1 К = (.7. О и и {Д},А./), где А £ / и О и {¿}, j = (1.к), J С Ь х К - минимальное множество, полз'ченное с использованием следующих правил для если (I. а, Г) £ А[. и (к, а, к') 6

А/с, то ({I, к), а, {Iк')) 6 Ал если I - молчащее и к - молчащее, то (¿, А;) (I, А;) 6 А.;.

Введём понятие юсо-различающего полуавтомата. Под юсо-различающим полуавтоматом будем понимать такой полуавтомат Я = (Л,/,О и {й},г,А«), где в & / и О и {5}, для которого справедливы следующие условия:

1. Л 2 {-Ц, Хк, !}•

2. Граф переходов полуавтомата Н ациклический.

3. Для всякого г е Л\{X, ±1., _1_к} либо т(г) = {г}, ои!;(г) = {5} и |г|; П {Х[_, 1к,= 0, либо т(г) = 0 и ои<;(г) = Ои{5}.

4. Состояния Хь Хк и X - тупиковые.

Пересечением полуавтомата И. и ¡осораздичалощего полуавтомата Я назовём связный полуавтомат 3 = £ Пе /? = {,/, О и {б},7, Л^), где = (I, г), 3 С I х Л - минимальное множество, полученное с использованием следующих правил для А./: если а. Г) € А1. и (г, а, г') 6 А/?, то ({1,г),а, (/',г')) е А./; если / - молчащее и {г,0,г') € А/г, то <г,г> д <г,г'> е л.,.

Говорят, что юсо-различающий полуавтомат Я1 различает полуавтоматы ¿.и К, если в пересечении З^к = Лв Л для всех тупиковых состояний (/, г) верно г = Х(., в то время как в пересечении Зкг? = К П» /? для всех тупиковых состояний {к, г) верно г = ХК-

Условный эксперимент по распознаванию двух полуавтоматов ¿и К, для которых существует юсо-различающий полуавтомат Л^к, строится следующим образом. В начальный момент полуавтомат находится в начальном состоянии г.

Пусть полуавтомат перешёл в состояние г и пусть в состоянии г определён переход по некоторому входному символу г. В этом случае па предъявленный для распознавания полуавтомат подаётся входное воздействие г и вычисляется новое состояние г' полуавтомата /?/_к как [г]^.

Если т(г) = 0, то ожидается выходная реакция от исследуемого полуавтомата. Если полуавтомат реагирует выходным символом о 6 О, то следующее состояние г' полуавтомата /?1.к есть [г|0. Если реакцией исследуемого полуавтомта является молчание, то следующее состояние полуавтомата /?/.к есть [г]^.

Эксперимент заканчивается, как только юсо-различающий полуавтомат переходит в одно из специальных состояний Х(., Хк или X. Если полуавтомат RLK достигает состояния Х(., то предъявленный полуавтомат распознаётся как полуавтомат Ц если полуавтомат Ли< достигает состояния Хк, то предъявленный полуавтомат распознаётся как полуавтомат К. Если полуавтомат /?(.к достигает состояния X, то предъявленный полуавтомат не является ни полуавтоматом /., ни полуавтоматом К.

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

Пусть /.и К два заданных полуавтомата и J — LГ\ К. Состояние (I, к) € 3 называется 1-недоопределённым, если оно молчащее. Состояние (1,к) 6 3 пересечения -/ называется г-не.доопределённым, если это состояние является (г — 1)-недоопределённым, или существует такое входное воздействие г е {(1,к)), что все состояния в множество являются (г — 1)-недоопределёниыми, либо если для всех о 6 оиЦ{1,к)) все состояния в [(£,&)]<, являются (г - 1)-недоопределёнными.

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

Алгоритм 2 Получение ¡осо-различающего полуавтомата

Вход: Два детерминированных полуавтомата /. = {Ь, I, О, I, Ах.) и К — (Кл I, О, А к)-Выход: 1оса-различаюи;ий полуавтомат Рч_к, если [.и К - юсо-различимы. 1: Л, := {-1-, -и, А„ е>-, J := L П К;

2: Строим - множество 1-недоопределённых состояний, (За - 2-недоопределёнпых состояний и

та 1С далее пока -/ +ь 3: Если Уг (I, к) £ С},, то

4: Исходные полуавтоматы юсо-совместимы; Конец. 5: Пусть п - такое число, что (1,к) € 0П> но (I, к) £ £?п-г; 6: г := и; := {{¡, к)}\ 3„-х := 0; := 0; . ..; Л := 0;

7: Пока (г > 0)

8: Для каждого ~ А:) £ Jл)

9: Если outj(^) = г ила Ыои^Ш £ то

10: Для каждого о € (О и {¿}) \ (ои^СО и добавим в множество Ак переходы

{з, о, когда о ф 6 и переход _1_) когда о = 11: Для каждого о £ оц^(/) \ оиЬк(к) добавим в множество Ая переходы 0, о, когда

о б и переход (.}, _1_1.) когда о = <5; 12: Для каждого о £ ои1«(А:) добавим в множество А« переходы когда

о ^ (5 и переход 0, Хк) когда о = Ь\ 13: Для каждого перехода (1,0.У) из АJ добавим в множество Ая переход • а в

множество состояние У, где г' < 2 - такое число, что з' € С)и е -1 -14: иначе

15: Выберем такое произвольное г £ ini.fi) П ¡пк(&), что ((I, к)^ С

16: Добавим в множество Ак переход из А./, а в множество Зг> состояние У, где

г' < г - такое число, что У 6 (¿^г и У £ 1 17: г г - 1; 18: Л := и?=0Л;

19: Автомат = (Я, О и {(?}-, г, Ад) - искомый автомат; Конец.

Таким образом, два полуавтомата разлитамы условным экспериментом, если и только если эти полуавтоматы являются ¡осо-различимыми. Мы предлагаем способ построения ¡осо-различающего полуавтомата (алгоритм 2).

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

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

Если К есть полуавтомат-реализация, юсо-различимый со спецификацией /., то тестовый пример получается из ¡осо-различающего автомата /?1.к заменой состояния ±1. на Т, и отождествлением состояния Лк с состоянием Состоянию Т соответствует вердикт «Тест пройден успешно», а1- «Обнаружена неисправность«-.

Будем говорить, что тестовый пример Р не согласуется с полностью определённым полуавтоматом К, если в пересечении Кг\д Р для всех тупиковых состояний (к, р), верно р — Тестовый пример Р абсолютно согласуется с полностью определённым полуавтоматом К, если в пересечении соответствия КПд Р для всех тупиковых состояний {к.р), верно р = Т.

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

(L, ioco, С) определяются так же как и для автоматной модели неисправности.

Пусть (L, ioco , С) - модель неисправности, в которой конечное множество С, состоит из полностью определённых полуавтоматов, и каждый полуавтомат из множества является либо ioco-реализацией спецификации L, либо ioco-различим с ней. Тогда полный проверяющий тест для этой модели неисправности можно построить перебором полуавтоматов из области неисправности. Для каждого выбранного полуавтомата, ¡осо-различимого со спецификацией, строится тестовый пример на основе алгоритма 2, который включается в проверяющий тест.

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

С этой целью вводится следующее преобразование полуавтомата L к автомату F^: F = L и если (1,а,1') и а € I, то {1,а.е0,1') £ Ар; если {1,а,1'} и а £ О, то (l,eL,a,l') £ Ар; если I - молчащее состояние, то (i,Ei,5,¡') £ Ар.

Теорема 3. L ioco К тогда и только тогда, когда F^ ^

Таким образом, благодаря теореме 3, становится возможным переходить от полуавтоматной модели неисправности (L, ioco , {Li, ¿2, • ■ •}) к автоматной модели неисправности (Fc, {Fj1, Fj2,...}}. Пусть Р - автоматный тестовый пример для модели неисправности {F^1, F^2,...}). Переход от него к полуавтоматному тестово-

му примеру Pi можно осуществить по следующим правилам: если in(p) = i £ / и (p,i,£0,p') £ Ар, то {p,i,p) £ apL\ если in(p) = £i и (p,ei,o,p) £ Ар, и о Ф е0, то то (р,о, р') £ Apl.

Теорема 4. Пусть задана полуавтоматная модель неисправности (L, ioco, {¿1, /.2,. - •}), по которой построена автоматная модель неисправно-cmu , ,...}), Тогда, если Т — {Р1, Р2,...} - полный проверяющий тест

относительно модели неисправности (F^, ;<, {F^', F^2,...}), то Tl = {PIjPL---} ~ полный проверяющий тест для модели неисправности (L, ioco, {Li, L2, • • •})•

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

Полностью определённый временной автомат U называется квази-редукцией временного автомата V (обозначение U ^ V), если для любой временной входной-выходной последовательности а из IV и всякого временного входного воздействия (i.t) из inx([ija) верно следующее: out([ii|^, (г, t)) С out([iJ^, (г, i)).

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

Для построения условного эксперимента, различающего два временных автомата мы вводим понятие пересечения этих автоматов. Пересечением временных автоматов U и V назовём временной автомат W — (W, I. О, w, А^. Д w), где w = (й,0, 0,0), К = {0.1,..., fc}, к - min(niax(Auiz+),max(Ai/Iz+)), nWCUxKxVxK-минимальное множество, полученное согласно следующим правилам для отношения Aw и функции ДW:

1. Если < (1и и ¿2 < £¿4 и (и, г, о, и') 6 Ли, и (и, ¿, о, г>') £ Ау, то {(и, ¿1, и, ¿2), г, о, (а', 0, ?/, 0)) £ Л, где Ди(и) = Ду(и) =

2. А({и,к1,у,к2)) = ((и',^,«',^),*:), где Ду(и) = (зи,сг„), Ду(и) =

/с = гшп(с/и — к\,(1ъ — /сг) и если ¿и = со или = оо, или — = dv — к2, то {и ,к[,у' ,к'2) = (,9„, 0, я„, 0); если (с1и-к]) £20+и {¿„-к?) £ 2,5', и (¿„-¿О < {(1„-к-2), то (и1 ,к[,у' ,к2) = {ви,0,у,к2 + если (¿и — £1) 6 и - £2) 6 и

— ¿1) > (<£„ — ¿2), то (и', к[,у', к'2) = (и, + /с, 0).

Под г-различающим временным автоматом понимается времешгой автомат /? = = (Д, /, О, г, Ая, Дд), для которого справедливы следующие условия:

1. Л Э {Ху.Ху, X}.

2. Граф переходов автомата /? ациклический, не считая петель X X, ±ц —* ±и и XV Ху.

3. Для всякого г £ Л\{Ху,XV,X} выполняется либо |т(г)| = 1 и ои!(г,г) = О, где ¡п(г) = {г}, и в этом случае Д/?(г) = (X, £), £ £ Н; либо т(г) = 0 и в этом случае Дк(г) = (г', 4), « 6 N. г' £ {X, Ху. Ху}.

4. Из состоя1шй Ху, Xу и X не определено ни одного перехода по входо-выходным парам и Д/?(Х) = (X, оо), Д/?(Ху) = (Ху.оо), Д«(Ху) = (Ху.оо).

Говорят, что г-различающий временной автомат И различает временные автоматы и и V, если в подмножестве {(и, к„, г, кг) 6 \Vijr \ т((и,ки,г,кг)) = 0} множества состояний пересечения IVш? = и Г\ R найдутся состояния, для которых г = Ху и для всех состояний подмножества г ф Ху, все переходы, ведущие в состояния вида (и, ки, X, кх), помечены только време1шыми задержками, и если (&.1у((и,ки,г,кТ))) 1ду= (и,к'и,±,к'±), то г = X; в то время как в подмножестве {(г), к„, г, кг) £ И'"ук | 1п((и, к„, г, кг)) = 0} множества состояний пересечения И/ук = V П /? найдутся состояния, для которых г = Ху и для всех состояний подмножества г ф Ху, все переходы, ведущие в состояния вида {у,к„, ±,к±), помечены только временными задержками, и если (Дц/((и, г, кг)))1\у= (у',к'^, X, к'±), то г = X.

Пусть для распознавания представлены временные автоматы С и V, для которых существует г-различающий временной автомат Ruv■ Условный эксперимент с использованием автомата Ruv строится следующим образом. В начальный момент значение переменной £ равно 0, а Ruv находится в начальном состоянии г.

Пусть £ = и временной автомат Ruv перешёл в состояние г, в котором определён переход по входному символу г £ 7. В этом случае на предъявленный для распознавания временной автомат подаётся входной символ г в момент времени £', В ^ < 23 + ¿г, где ¿г - значение временной задержки в состоянии г (время отсчи-тывается от момента получешш последней выходной реакции предъявленного для эксперимента временного автомата). Предъявленный временной автомат реагирует на входной символ некоторым выходным символом о, на основании которого вычисляется следующее состояние г-различающего временного автомата Ruv, значение переменной £ обнуляется. Если в текущем состоянии г-различающего временного автомата не определён переход по любому входному символу, то к значению О переменной £ прибавляется величина временной задержки в текущем состоянии, и следующее состоя1ше г-различающего временного автомата /?уу вычисляется по значению Дя(г). Эксперимент заканчивается, как только г-различающий временной автомат переходит в одно из специальных состояний Ху или Ху. Если г-различающий времешюй автомат /?уу достигает состояния Ху, то предъявленный временной автомат

Алгоритм 3 Получение г-различающего временного автомата

Вход: Два наблюдаемых временных автомата и = (и, I, О, й, Ли, Ду) и V = (V, О, V, Ау, Лу). Выход: Я-различающий временной автомат Ruv, если и и V - г-различимы. 1: Н'о := Ху, Ав := И; IV := I/ П V;

2: Строим - множество 1-недоопределённых состояний, (¿2 ~ 2-недоопределённых состояний и

так далее пока О] ф <5:7+13: Если Ч] (й,0,г,0) <{. ¿¡¡, то

4: Исходные временные автоматы г-совместимы; Конец. 5: Пусть п - такое число, что (й, 0,0,0) £ С5„, но (й, 0,0,0) £ <9,1-1; 6: 2 := п; := {(и, 0, С, 0)}; := 0; И^з := 0; ...; И^ := 0;

7: Пока (г > 0)

8: Для каждого (ш = (и,ки,у,к„) 6 IV»)

9: Если для всех г 6 1!'и(и) П и всех о & О выполняется [>'"¿1/- £ то

10: Положим Дя(ги) (и>',()), где (и>',1) = Д№(и;);

11: Добавим состояние и/ в множество 1У2;

12: иначе

13: Выберем такое произвольное г € ¡пу(и) П что для всех о £ О выполняется

М>/о £

14: Для каждого о 6 О \ (ои1у(и, г) и ои1у(и,г)) добавим в множество А/? переходы

(ш, г, о, Х);

15: Для каждого о 6 ои1и(и, г) \ои1у(г;,1) добавим в множество Ад переходы {ш, г, о, ±и);

16: Для каждого о € ои^(г>, г)\ои1у(и,г) добавим в множество Ад переходы (ги. ¿, о, .1 у);

17: Для каждого перехода (ш,г,о,и>') из Ауу добавим в множество Ая переход (и:, г, о, 7:/),

а в множество состояние и/, где г' < г - такое число, что ад' € но и/ £ 18: Если = (ти,оо), то положим Ан(и)) (±,1), иначе Если Д^ц;) = (у)", г) Е

IV X Ы, то положим Дя(ти) := {X, 1}; 19: г:=г-1; 20: Л:= и"^^;

21: Временной автомат (Л,О, г, Ак, Дя) - искомый временной автомат; Конец.

распознается как временной автомат 11; если г-различающий временной автомат Ящ/ достигает состояния то предъявленный времегаюй автомат распознается как временной автомат V.

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

Теорема 5. Два временных автомата г-различимы тогда и только тогда, когда для них существует г-различающий временной автомат.

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

Состояние и> — (и, и,/с„) пересечения VI/ = и П V называется 1-недоопределённым, если найдётся такой входной символ г из ¡пу(а') О ¡пу(у'), по которому нет ни одного перехода из состояния и>. Также состояние называется 1-недоопределённым, если из него можно перейти в другое 1-недоопределённое состояние по временной задержке. Состояние ш пересечения И/ называется г-недоопределённым, z > 1, если оно (г - 1)-недоопределённым, или найдётся такой входной символ г £ т((и, ки, V, кг.)), что все состояния, достижимые из и> но входному символу г, являются (г - 1)-недоопределёнными. Состояние ы будет г-недоопределённым также в случае, когда из него по временной задержке достижимо некоторое г-недоопределённое состояние.

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

При построении тестов с гарантированной полнотой вместо различающего полуавтомата используют понятие тестового примера. Если V есть временной автомат-реализация, различимый со спецификацией и, то тестовый пример получается из различающего автомата заменой состояния ±у на состояние Т, отождествлением состояния с состоянием ±, введением нового состояния I, и заменой всех переходов г Л. на г I, где г € N. Состоягше Т соответствует вердикту «Тест пройден успешно», состояние ± - «Обнаружена неисправность», а состояние I - «Результат не определён».

Будем говорить, что тестовый пример Р не согласуется с полностью определённым временным автоматом V, если в подмножестве {{г1, к»,р, кр) | т({г>, = 0} множества состояний пересечения И/ = УП Р найдутся состояния, для которых р = для всех состояшш этого подмножества р Ф Т и если Д ки, р, кр)) = ({у1, к'у, I, к), Ь) для некоторого то р = I. Тестовый пример Р абсолютно согласуется с полностью определённым временным автоматом V, если в подмножестве {{и,ку,р,кр) | т({ь,ки,р,кр)) = 0} множества состояний пересечения ]/\/ = V Г\ Р найдутся состояния, для которых р = Т, для всех состояний этого подмножества р ф X и если Аш^^,,^,^}) = I,к), для некоторого ^ то р = I.

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

ЗАКЛЮЧЕНИЕ

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

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

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

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

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

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

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

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

— 2008. — №6. — С. 1-11.

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

3. Gromov М., Willemse Т. Testing and Model-Checking Techniques for Diagnosis // Vol.4581 of LNCS. - Springer, 2007. - P.138-154.

4. Громов М.Л., Шабалдина H.B. О распознавании недетерминировашюго автомата в заданном классе // Материалы IX Международного семинара «Дискретная математика и её приложения» / Под ред. О.М. Касим-Заде. — М.: ММФ МГУ, 2007.

- С. 157-160.

5. Громов М.Л. Метод построения полного проверяющего теста для входо-выходных полуавтоматов // Вестник ТГУ. Управление, вычислительная техника и информатика. — 2008. - №3(4). — С. 85-98.

6. Gromov М., Evtushenko N., Kolomeets A. On the synthesis of adaptive tests for nondeterministic finite state machines // Program. Comput. Softw. — 2008. — Vol. 34. N. 6. - P. 322-329.

7. Громов М.Л., Кондратьева O.B. Об одном классе автоматов с полиномиальной оценкой числа состояний в наблюдаемой форме // Журнал СФУ. Серия: Математика и физика - 2008. - Т. 1, №3. - С. 257-251.

8. Gromov М. A novel method for derivation of a test with guaranteed coverage for LTS /'/ Proceedings of SYRCoSE 2008. - St.Peterburg: S-PSU, 2008. - P. 47-49.

9. Gromov M., Popov D., Yevtushenko N. Deriving test suites for timed Finite State Machines // Proceedings of IEEE East-West Design к Test Symposium'08. — Kharkov, Ukraine: SPD FL Stepanov V.V., 2008. - P. 339-343.

10. Gromov M., El-Fakih K., Shabaldina N., Yevtushenko N. Distinguing Non-deterministic Timed Finite State Machines // Vol. 5522 of LNCS. — Springer, 2009. — P. 137-151.

Тираж 150 экз. Отпечатано в КЦ «Позитив» 634050 г. Томск, пр. Ленина 34а

Введение

Принятые обозначения

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

1.1 Введение.

1.2 Входо-выходные полуавтоматы.

1.3 Автоматы.

1.4 Временные автоматы.

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

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

2 Различающие эксперименты с недетерминированными автоматами

2.1 Введение.

2.2 Отношения r-совместимости и г-различимости.

2.3 Алгоритм построения r-различающего автомата.

2.4 Синтез проверяющих тестов при явно заданной области неисправности и по мутационному автомату.

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

2.5.1 Модель неисправности и распознавание неисправной компоненты.

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

2.5.3 Модель неисправности и распознавание неисправной компоненты.

2.5.4 Результаты компьютерных экспериментов.

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

3 Различающие эксперименты с входо-выходными полуавтоматами

3.1 Введение.

3.2 Отношение ioeo-различимости.

3.3 Алгоритм построения ioco-различающего полуавтомата

3.4 Синтез проверяющих тестов на основе перебора элементов из области неисправности.

3.5 Связь между ioco и квази-редукцией.

3.5.1 Построение конечного автомата по входо-выходному полуавтомату.

3.5.2 Построение полного проверяющего теста для входо-выходных полуавтоматов на основе полного проверяющего теста для автоматов

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

4 Различающие эксперименты с временными автоматами

4.1 Введение.

4.2 Отношение г-совместимости.

4.3 Алгоритм построения r-различающего временного автомата

4.4 Синтез проверяющих тестов для явно заданной области неисправности

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

Актуальность проблемы. Тестирование является неотъемлемой частью жизненного цикла любой системы. Под тестированием понимается процесс подачи входных воздействий на тестируемую систему, наблюдение выходных реакций и вывод заключения о правильном или неправильном поведении системы [1-3]. Эмпирические тесты оказались недостаточными в первую очередь для систем управления сложными процессами, что, в свою очередь, привело к новому витку развития тестирования на основе формальных моделей. Для дискретных управляющих систем одной из широко используемых моделей при синтезе тестов является автоматная модель(см., например, [4-7]), и методы синтеза проверяющих тестов с гарантированной полнотой хорошо развиты для детерминированных автоматов [4,8-13]. Однако в ряде случаев поведение системы описывается недетерминированным автоматом [14-17]. Причины появления недетерминизма в спецификациях и реализациях, вообще говоря, различные [18,19]; среди них можно выделить возможность различных опций при реализации, уровень абстракции описания, невозможность полной управляемости и наблюдаемости для реализации и так далее. Одной из основных проблем при синтезе тестов для недетерминированных реализаций является тот факт, что в общем случае недетерминированный (проверяемый) автомат может реагировать различными выходными последовательностями на одну и ту же входную последовательность. Поэтому обычно при тестировании peaлизаций с недетерминированным поведением делается допущение о «всех погодных условиях» [20-22], то есть предполагается, что каждая тестовая входная последовательность подается на реализацию достаточно большое число раз в «различных погодных условиях», и поэтому можно считать, что тестер пронаблюдал все возможные выходные реакции реализации на каждую входную последовательность. Допущение о «всех погодных условиях» является скорее теоретическим, так как никто не знает, сколько раз достаточно подать входную последовательность, чтобы дать возможность тестеру «увидеть» все выходные реакции реализации. Более того, такому предположению невозможно удовлетворить, если проверяемый автомат является только частично контролируемым, что имеет место, например, при удаленном тестировании реализаций телекоммуникационных протоколов. В [23,24] предлагаются методы синтеза проверяющих тестов без использования предположения о «всех погодных условиях» при проведении безусловного эксперимента с проверяемой системой. Длины этих тестов большие, однако известно (см., например, [25-27]), что длина тестов может быть существенно сокращена на основе условного тестирования проверяемой системы. Таким образом, разработка методов синтеза условных проверяющих и диагностических тестов для систем с автоматным поведением без использования предположения о «всех погодных условиях» является актуальной задачей.

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

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

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

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

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

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

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

1. Необходимые и достаточные условия распознавания двух недетерминированных автоматов посредством условного эксперимента и представление конечным автоматом условного эксперимента по распознаванию двух различимых автоматов.

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

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

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

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

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

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

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

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

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

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

Результаты работы докладывались на российских и международных конференциях: «East-West Design and Test Workshop» (Одесса, 2005 и Львов, 2008); IX Международном семинаре «Дискретная математика и её приложения» (Москва, 2007); Всероссийской конференции с международным участием «Новые информационные технологии в исследовании сложных структур» (Иркутск, 2004 и Шушенское, 2006); TESTCOM-2007 (Таллин, 2007); SYRCoSE (Санкт-Петербург, 2008, Москва, 2009).

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

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

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

3. Gromov, М. Testing and Model-Checking Techniques for Diagnosis / M. Gromov and T. Willemse // Vol.4581 of LNCS. - Springer, 2007. - Pp.138-154.

4. Громов, M.JI. О распознавании недетерминированного автомата в заданном классе / M.JI. Громов, Н.В. Шабалдина // Материалы IX Международного семинара «Дискретная математика и её приложения» / Под ред. О.М. Касим-Заде. - М.: ММФ МГУ, 2007. - С. 157-160.

5. Громов, М. Метод построения полного проверяющего теста для входо-выходных полуавтоматов / М. Громов // Вестник ТГУ. Управление, вычислительная техника и информатика. — 2008. — №3(4). — С. 85-98.

6. Gromov, M.L. On the synthesis of adaptive tests for nondeterministic finite state machines / M.L. Gromov, N.V. Evtushenko, A.V. Kolomeets // Program. Comput. Softw. - 2008. - Vol. 34, no. 6. - Pp. 322-329.

7. Громов, M. Об одном классе автоматов с полиномиальной оценкой числа состояний в наблюдаемой форме / М. Громов, О. Кондратьева Журнал СФУ. Серия: Математика и физика — 2008. — Т.1, №3. -С. 257-261.

8. Gromov, М. A novel method for derivation of a test with guaranteed coverage for LTS / M. Gromov // Proceedings of SYRCoSE 2008. -St.Peterburg:S-PSU, 2008. - Pp. 47-49.

9. Gromov, M. Deriving test suites for timed Finite State Machines / M. Gromov, D. Popov, N. Yevtushenko // Proceedings of IEEE East-West Design & Test Symposium'08. — Kharkov, Ukraine: SPD FL Stepanov V.V., 2008. - Pp. 339-343.

10. Distinguing Non-deterministic Timed Finite State Machines / M. Gromov, K. El-Fakih, N. Shabaldina, N. Yevtushenko // Vol. 5522 of LNCS. - Springer, 2009. - Pp. 137-151.

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

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

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

Заключение

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

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

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

3. Введено понятие ioсо-различимости двух входо-выходных полуавтоматов. Установлены необходимые и достаточные условия различимости двух входо-выходных полуавтоматов условным экспериментом. Показано, что два входо-выходных полуавтомата различимы условным экспериментом, если и только если эти полуавтоматы ioco-различимы, то есть если и только если для них существует ioco-различающий полуавтомат.

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

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

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

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

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

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

1. Gill, A. 1.troduction to the theory of Finite-State Machines / A. Gill. — McGraw-Hill, 1962.

2. Moore, E. F. Gedanken-Experiments on Sequential Machines / E. F. Moore; Ed. by C. Shannon, J. McCarthy. — Princeton, New Jersey: Princeton University Press, 1956.— Pp. 129-153.

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

4. Chow, Т. S. Testing software design modeled by finite-state machines / T. S. Chow // IEEE Trans. Softw. Eng. ~ 1978. Vol. 4, no. 3. - Pp. 178187.

5. Conformance testing of protocols specified as communicating finitestate machines a guided random walk based approach / D. Lee, К. K. Sab-nani, D. M. Kristol, S. Paul // IEEE Transactions on Communications. — 1996. - Vol. 44, no. 5. - Pp. 631-640.

6. Lai, R. A survey of communication protocol testing / R. Lai j j J. Syst. Softw. 2002. — Vol. 62, no. 1. - Pp. 21-46.

7. Hennie, F. C. Fault detecting experiments for sequential circuits / F. C. Hennie // Proc. of 5th Annual Symposium on Switching Circuit Theory and Logical Design. — Princeton, USA: Princeton University Press, 1964.-Pp. 95-110.

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

9. Yannakakis, М. Testing finite state machines: fault detection / M. Yan-nakakis, D. Lee j j Selected papers of the 23rd annual ACM symposium on Theory of computing. — Orlando, FL, USA: Academic Press, Inc., 1995. — Pp. 209-227.

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

11. Petrenko, A. Testing from partial deterministic fsm specifications / A. Pe-trenko, N. Yevtushenko // IEEE Trans. Comput2005.- Vol. 54, no. 9,- Pp. 1154-1165.

12. Dorofeeva, R. An improved conformance testing method / R. Dorofeeva, K. El-Fakih, N. Yevtushenko // Formal Techniques for Networked and Distributed Systems FORTE 2005. - LNCS. - Berlin, Heidelberg: Springer, 2005. - Pp. 204-218.

13. Hierons, R. M. Adaptive testing of a deterministic implementation against a nondeterministic finite state machine / R. M. Hierons // The Computer Journal. 1998. - Vol. 41, no. 5. - Pp. 349-355.

14. Hierons, R. M. Generating candidates when testing a deterministic implementation against a non-deterministic finite-state machine / R. M. Hierons // The Computer Journal. 2003. - Vol. 46, no. 3. - Pp. 307-318.

15. Hierons, R. M. Testing from a nondeterministic finite state machine using adaptive state counting / R. M. Hierons // IEEE Trans. Comput. — 2004. — Vol. 53, no. 10. Pp. 1330-1342.

16. Coping with nondeterminism in network protocol testing / R. Miller, D.-L. Chen, D. Lee, R. Hao // Testing of Communicating Systems. — Vol. 3502 of LNCS. Berlin, Heidelberg: Springer, 2005. - Pp. 129-145.

17. Milner, R. Communication and concurrency / R. Milner. — Upper Saddle River, NJ, USA: Prentice-Hall, Inc., 1989.

18. Luo, G. Test selection based on communicating nondeterministic finite-state machines using a generalized wp-method / G. Luo, G. von Bochmann, A. Petrenko // IEEE Trans. Softw. Eng.— 1994.- Vol. 20, no. 2.— Pp. 149-162.

19. Selecting test sequences for partially-specified nondeterministic finite state machines / G. Luo, A. Petrenko, R. Petrenko, G. V. Bochmann //In IFIP 7th International Workshop on Protocol Test Systems. — 1994.— Pp. 91106.

20. Spitsyna, N. Studying the separability relation between finite state machines / N. Spitsyna, K. El-Fakih, N. Yevtushenko // Softw. Test. Verif. Reliab. 2007. - Vol. 17, no. 4. - Pp. 227-241.

21. Hierons, R. M. Concerning the ordering of adaptive test sequences /

22. R. M. Hierons, H. Ural // Formal Techniques for Networked and Distributed Systems FORTE 2003. - Vol. 2767 of LNCS. - Berlin, Heidelberg: Springer, 2003. - Pp. 289-302.

23. Hierons, R. M. Reducing the cost of applying adaptive test cases / R. M. Hierons, H. Ural // Comput. Netw. — 2007. — Vol. 51, no. 1.- Pp. 224-238.

24. Tretmans, J. Test generation with inputs, outputs and repetitive quiescence / J. Tretmans // Software—Concepts and Tools. — 1996.— Vol. 17, no. 3.-Pp. 103-120.

25. Бурдонов, И. Б. Теория конформности для функционального тестирования программных систем на основе формальных моделей: автореф. диссертации на соискание степени д-ра физ-мат. наук: 05.13.11.— М., 2008. 60 с.

26. Merayo, М. 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, no. 6. - Pp. 835-844.

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

28. Громов, М. Л. Об одном классе автоматов с полиномиальной оценкой числа состояний в наблюдаемой форме / М. JI. Громов, О. В. Кондратьева // Журнал Сибирского федерального университета. Серия: Математика и физика. — 2008. — Т. 1, № 3. — С. 257-261.

29. Formal test automation: A simple experiment / A. Belinfante, J. Feenstra, R. G. d. Vries et al. // Proceedings of the IFIP TC6 12th International

30. Workshop on Testing Communicating Systems. — Deventer, The Netherlands: Kluwer, B.V., 1999,- Pp. 179-196.

31. Vries, R. G. d. Towards formal test purposes / R. G. d. Vries, J. Tret-mans // Proceedings of the Workshop on Formal Approaches to Testing of Software / Ed. by E. Brinksma, J. Tretmans. — Vol. NS-01-04. — Aarhus: 2001.-Pp. 61-76.

32. Starke, P. H. Abstract Automata / P. H. Starke.— Elsevier, 1972.— 419 pp.

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

34. Merayo, М. G. Formal testing from timed finite state machines / M. G. Merayo, M. Nunez, I. Rodriguez // Computer Networks. — 2008.— Vol. 52, no. 2.- Pp. 432-460.

35. Gaston, С. Unitary testing of components in context / C. Gaston, P. Le Gall. Invited lecture at 5th TAROT Summer School 2009, Spain.

36. Petrenko, A. Fault model-driven test derivation from finite state models: annotated bibliography / A. Petrenko. 2001. — Pp. 196-205.

37. Hierons, R. M. Testing in the distributed test architecture: An extended abstract / R. M. Hierons // Quality Software, International Conference on. 2008. - Vol. 0. - Pp. 11-14.

38. Hierons, R. M. The effect of the distributed test architecture on the power of testing / R. M. Hierons, H. Ural // Comput. J.— 2008.- Vol. 51, no. 4.- Pp. 497-510.

39. Hierons, R. Checking sequences for distributed test architectures / R. Hierons, H. Ural // Distributed Computing. — 2008. — September. — Vol. 21, no. 3. — Pp. 223-238. http://dx.doi.org/10.1007/s00446-008-0062-4.

40. Hierons, R. M. Overcoming controllability problems with fewest channels between testers / R. M. Hierons, H. Ural j j Comput. Netw. — 2009. — Vol. 53, no. 5. Pp. 680-690.

41. Hierons, R. M. Testing distributed systems / R. M. Hierons. — Invited lecture at 5th TAROT Summer School 2009, Spain.

42. Petrenko, A. Conformance tests as checking experiments for partial non-deterministic fsm / A. Petrenko, N. Yevtushenko // Formal Approaches to Software Testing. — Vol. 3997 of LNCS. ~ Berlin, Heidelberg: Springer, 2006.-Pp. 118-133.

43. Tretmans, J. Model based testing with labelled transition systems / J. Tret-mans // Formal Methods and Testing. — 2008. — Pp. 1-38.

44. G. v. Bochmann, A. Petrenko, M. Yao 11IWPTS '94: 7th IFIP WG 6.1 international workshop on Protocol test systems. — London, UK, UK: Chapman к Hall, Ltd., 1995,- Pp. 55-76.

45. Glabbeek, R. J. v. The linear time-branching time spectrum (extended abstract) / R. J. v. Glabbeek // CONCUR '90: Proceedings of the Theories of Concurrency: Unification and Extension. — London, UK: Springer-Verlag, 1990.- Pp. 278-297.

46. Vaandrager, F. W. On the relationship between process algebra and input/output automata (extended abstract) / F. W. Vaandrager //In Proceedings 6 th Annual Symposium on Logic in Computer Science. — IEEE Computer Society Press, 1991.- Pp. 387-398.

47. Tan, Q. M. Test generation for specifications modeled by input/outputautomata / Q. M. Tan, A. Petrenko // IWTCS: Proceedings of the IFIPf

48. TC6 11th International Workshop on Testing Communicating Systems. — Deventer, The Netherlands: Kluwer, B.V., 1998,- Pp. 83-100.

49. Alur, R. A theory of timed automata / R. Alur, D. L. Dill // Theor. Comput. Sci. — 1994. — Vol. 126, no. 2.- Pp. 183-235.

50. Springintveld, J. Testing timed automata / J. Springintveld, F. Vaandrager,

51. P. R. D'Argenio // Theor. Comput. Scz. 2001. - Vol. 254, no. 1-2.-Pp. 225-257.

52. En-Nouaary, A. Timed wp-method: Testing real-time systems / A. En-Nouaary, R. Dssouli, F. Khendek // IEEE Trans. Softw. Eng. 2002. -Vol. 28, no. 11. - Pp. 1023-1038.

53. Tripakis, S. Folk theorems on the determinization and minimization of timed automata / S. Tripakis // Inf. Process. Lett. — 2006. — Vol. 99, no. 6.- Pp. 222-226.

54. 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. 2008. — Vol. 78, no. 2. — Pp. 98-115.

55. El-Fakih, K. Testing Timed Finite State Machines with guaranteed fault coverage / K. El-Fakih, N. Yevtushenko, H. Fouchal. — Принята к публикации на TESTCOM-2009.

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

57. Громов, М. Л. О распознавании недетерминированного автомата в заданном классе / М. JI. Громов, Н. В. Шабалдина // Материалы IX Международного семинара «Дискретная математика и её приложения» / Под ред. О. М. Касим-Заде,- М.: ММФ МГУ, 2007.- С. 157160.

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

59. Gromov, М. L. On the synthesis of adaptive tests for nondeterministic finite state machines / M. L. Gromov, N. V. Evtushenko, A. V. Kolomeets // Program. Comput. Softw. 2008. - Vol. 34, no. 6. - Pp. 322-329.

60. Евтушенко, H. Недетерминрованные автоматы: Анализ и синтез. Ч. 1. Отношения и операции: Учебное пособие / Н. Евтушенко, А. Петренко, М. Ветрова. — Томск: Томский госуниверситет, 2006. — 142 с.

61. El-Fakih, K. Fsm-based re-testing methods / K. El-Fakih, N. Yevtushenko,

62. G. v. Bochmann // TestCom '02: Proceedings of the IFIP 14th International Conference on Testing Communicating Systems XIV. — Deventer, The Netherlands, The Netherlands: Kluwer, B.V., 2002. Pp. 373-390.

63. Fault diagnosis in extended finite state machines / K. El-Fakih, S. Prokopenko, N. Yevtushenko, G. von Bochmann // Proc. of the IFIP 15th International Conference, TesCom'03 / Ed. by H. Dieter, A. Wiles. — LNCS. Berlin: Springer, 2003.- Pp. 197-210.

64. Громов, M. Метод построения полного проверяющего теста для входо-выходных полуавтоматов / М. Громов // Вестник ТГУ. Управление, вычислительная техника и информатика. — 2008. — № 3(4). — С. 8598.

65. Gromov, М. A novel method for derivation of a test with guaranteed coverage for Its / M. Gromov // Proceedings of SYRCoSE 2008. St. Peterburg: S-PSU, 2008. - Pp. 47-49.

66. Gromov, M. Deriving test suites for timed finite state machines / M. Gromov, D. Popov, N. Yevtushenko // Proceedings of IEEE East-West Design & Test Symposium'08. — Kharkov, Ukraine: SPD FL Stepanov V.V., 2008. Pp. 339-343.