A Method of the Complete Test Derivation For Labeled TransitionSystems .pdf При построении проверяющих тестов для дискретных реактивных систем наиболее активно используются две модели с конечным числом переходов: конечные автоматы [1] и входо-выходные полуавтоматы [2]. Для каждой из моделей существуют свои отношения конформности (соответствия) и свои методы построения проверяющих тестов с гарантированной полнотой, которые для каждой из моделей имеют свои достоинства и недостатки. В частности, в теории автоматов хорошо развиты методы синтеза конечных проверяющих тестов при условии, что множество проверяемых автоматов является конечным, например, содержит все автоматы, число состояний которых не превышает некоторого целого числа. В теории полуавтоматов таких методов, насколько известно автору, пока не предложено. С другой стороны, методы синтеза проверяющих тестов в теории автоматов в основном развиты для тестирования детерминированных автоматов относительно эквивалентности, и по этой причине практически все известные методы доставляют безусловные тесты. В теории входо-выходных полуавтоматов тестирование с самого начала было адаптивным; поэтому основное внимание уделяется синтезу условных тестов. Поскольку обе модели принадлежат классу так называемых моделей с конечным числом переходов, то представляет интерес возможность объединить достоинства известных методов для обеих моделей с точки зрения построения наиболее эффективных тестов. Однако, несмотря на общие свойства двух моделей, известно, что автоматический перенос методов при переходе от одной модели к другой не является возможным. Методы должны быть соответствующим образом адаптированы. В данной работе показывается, каким образом можно построить полный проверяющий тест для входо-выходного полуавтомата относительно классического отношения ioco на основе полного проверяющего теста для конечного автомата относительно специального отношения квазиредукции, обобщающего ранее известное определение [1]. Для построения полного проверяющего теста относительно расширенной квази-редукции можно использовать методы синтеза полных проверяющих тестов относительно старого понятия квази-редукции с соблюдением некоторых ограничений.Структура работы следующая. В разделе 1 мы напоминаем основные определения для входо-выходных полуавтоматов и конечных автоматов. В разделе 2 показываем, что входо-выходной полуавтомат можно преобразовать в конечный автомат таким образом, что преобразованные автоматы находятся в отношении ква-зи-редукции, если и только если исходные полуавтоматы находятся в отношении ioco. В разделе 3 показывается, каким образом можно построить полный проверяющий тест для входо-выходного полуавтомата на основе проверяющего теста для соответствующего автомата.1. ОпределенияВ данной работе мы рассматриваем детерминированные входо-выходные полуавтоматы с дополнительным, так называемым молчащим, выходным символом, то есть мы предполагаем, что при тестировании системы имеется возможность наблюдать отсутствие выходного сигнала, соответственно автоматы предполагаются наблюдаемыми. Переход к таким полуавтоматам и автоматам является допустимым с точки зрения теории, так как для каждого полуавтомата (автомата) существует эквивалентный (с тем же набором входо-выходных последовательностей) детерминированный полуавтомат (наблюдаемый автомат). В этой части мы вводим основные определения и понятия для входо-выходных полуавтоматов с молчанием (которые мы будем для краткости называть просто полуавтоматами) и автоматов. Определения для полуавтоматов взяты из [2], для автоматов - из [1].1.1. Входо-выходные полуавтоматыОпределение 1. Под входо-выходным полуавтоматом (или просто полуавтоматом) с входным алфавитом I и выходным алфавитом O будем понимать пятёрку (S, I, O, X, s0 > L, где S - непустое множество состояний с выделенным начальным состоянием s0; I и O - непересекающиеся непустые множества входных ивыходных действий соответсвенно, объединение которых мы обозначаем как A. Отношение переходов 1с S х A х S есть функция, отображающая подмножество множества S х A в S .Пусть L = {S,I,O,X,s0>L - некоторый полуавтомат, а s, s', ... - состояния из S. Будем использовать следующие сокращённые записи: для всех действий a мы пишем s --> s', если и только если (s, a, s') е X, s -"->, если и только если существует такое состояние s' е S , что s -- s', и s^-i"^> , если и только если для всех s'е S не выполняется s ---» s'.В теории входо-в^гходных полуавтоматов понятие молчания [2] вводится следующим образом:Определение 2. Состояние s е S полуавтомата L = {S, I, O, X, s0 >L назовём молчащим (устойчивым), если и только если для всякого a из O справедливоs_^->"> . Для удобства дальнейших рассуждений введём предикат 8(s), принимающий значение «истина», если и только если состояние s - молчащее.Неформально, полуавтомат, находясь в устойчивом состоянии, «отказывается» произвести какой-либо выходной сигнал. На практике наблюдаемость «молчания» обеспечивается введением определенного промежутка времени, в течение которого система «обязана» произвести выходной сигнал, если таковой возможен в текущем состоянии. Если в течение этого промежутка времени выходной сигнал от системы не поступает, то предполагается, что система достигла своего устойчивого состояния. Пусть bi A - новый выходной символ, обозначающий возможность наблюдать молчание; Аъ - сокращённая запись дляA и {8}. Пусть се A*, a е Аъ и s, s', s" е S . Тогда, расширяя отношение переходов на последовательности, можно ввести новое отношение =>с S х A* х S как наименьшее множество, удовлетворяющее следующим правилам:ааs = s 'л s' -- s''s == s 'л5( s')E 'а.а'а.5s = ss => s''s => s'Здесь s - пустая последовательность. Будем писать s => s' тогда и только тогда,когда (s, a, s') ; sтогда и только тогда, когда для всех s' е T выполняется (s, a, s') , где се A*Для формализации описания мы вводим следующие операторы и функции (здесь S'с S, s,s' е S , се ):def и1.={s'e S | s ^ s'} - множество состояний, достижимых из состояния s попоследовательности a . Поскольку здесь мы рассматриваем детерминированныеполуавтоматы, то это множество состоит не более чем из одного элемента.defСоответственно для S' полагаем [S']а = [J , [s]a.def2.out(s) = {a e O | s -->} u {8 | 8(s)} - множество выходных символов, вклю-чая специальный символ 8, определённых в состоянии s. Для S' полагаемdefout(S') = UseS,out(s).def3.in( s)={i e I | s -'->} - множество входных символов, определённых в со-defстоянии s. Для S' полагаем in(S') = [J in(s).def &4..s - traces(s) ={ст e As* | s =>} - язык полуавтомата с учётом молчащего символа 8.5..traces(s) = s -traces(s) n A* - язык полуавтомата без учёта молчащего символа 8.def6.der(s) = ^ /Иа - множество состояний, достижимых из состояния s.def7. init(s)={a е As | s -->} - множество всех действий, включая 8, определённых в состоянии s.В этой работе мы рассматриваем только связные полуавтоматы, то есть такие полуавтоматы L = {S, I, O, X, s0 > L, для которых верно der(s0 ) = S, то есть всякое состояние достижимо из начального.Утверждение 1. Введённые операторы обладают следующими свойствами:1..Для всех состояний s полуавтомата верно out(s) .2..Если для некоторого состояния s полуавтомата и некоторой последова-тельности се A* выполняется s/> , то = 0 .3..out(0) = 0.4..[0]a = 0 для любого a е Аъ.Общие свойства двух полуавтоматов удобно характеризовать с помощью пересечения [3]:Определение 3. Пусть L1 = {S1, I, O, Xl, s01 >L и L2 = {S2,1,0, X2, s02 >L - два (де-терминированных) входо-выходных полуавтомата. Пересечением полуавтоматовLl и L2 назовём полуавтомат Ll n L2 = {S, I, O, X, {s01, s02»L , где S с St x S2 - ми-нимальное множество, полученное с использованием следующего правила для X :s -^-»s' л s2 -^ s2, с,< Si' S2 >>( Si, S2 >Согласно [3], пересечение обладает следующими свойствами:Утверждение 2. Пусть Ln L2 = {S, I, O, X, {s01, s02»L - пересечение заданн^1хполуавтоматов L1 = {S1, I, O, X1, s01 > L и L2 = (S2,1, O, X2, s02 >L. Тогдасправедливоследующее:1..init((Sj, s2» = init(sj) n init(s2), где s e Sj, s2 e S2 и (Sj, s2>e S .2..s - traces((sl, s2)) = s -traces(sl) n s - traces(s2).о.Определение 4. Пусть L = (S, I, O, X, s0) L. Состояние s e S называется полностью определённым по входам или просто полностью определённым, если в нём и во всех состояниях, достижимых из него, определены переходы по всем входным символам. Если начальное состояние s0 полуавтомата L полностью определено, то сам полуавтомат назовём полностью определённым.Определение 5. Пусть Ll = {St, I, O, Xl, s01 > L и L2 = {S2,1,0, X2, s02 > L. Полуавтомат Ll находится в отношении ioco с L2 (обозначение Ц ioco L2) тогда и только тогда, когда Lj - полностью определённый полуавтомат и для всякой последовательности ст из s - traces(s02) справедливо out([s0j]п) с out([s02 ]п).Утверждение 3. Пусть L1 = {S1, I, O, X1, s01 > L и L2 = {S2,1, O, X2, s02 > L - два за-даных детерминированных связных полуавтомата, причём Lj - полностью определённый полуавтомат, и пусть Ll n L2 = {S, I, O, X, {s01, s02»L. Тогда L ioco L2, если и только если для всякого состояния (sl, s2) е S перечечения L n L2 справедливо out((, s2 >) = out(), где s e St, а s2 e S2. Доказательство. Необходимость. Пусть Ll ioco L2.Рассмотрим в пересечении полуавтоматов состояние (sl, s2 >, достижимое из начального состояния (s0j, s02 > по последовательности а . Из свойства пересечения 2.2 следует, что s0lasl и s02as2, то есть eres-traces( s0j) и eres-traces( s02), а так как Ц и L2 - детерминированные полуавтоматы, то [s01 ]п = (sj} и [s02L ={s2}. По определению ioco имеем out([s0j ]п) с out([s02 ]п), то есть out(s') n out(s2 ) = out(s'), а из свойства 2.2 следует, что, out((Sj, s2» = out(sj) n out(s2). Отсюда out((s', s2 >) = out^).Достаточность. Пусть для всякого состояния (Sj, s2 > е S пересечения Ll n L2 верно out((sl, s2 >) = out(s'). Рассмотрим произвольную последовательностьeres-traces( s02). Если s01 f> , то тривиально out([s0j ]п) с out([s02 ]п). Пустьs01 ^ и пусть (помним, что Lj и L2 - детерменированные полуавтоматы) Kl 1П = (si) и [s02]п = [s2}. Тогда, согласно свойству 2.2, []п = {}. Из свойства пересечения 2.2 следует, что out(( sl, s2» = out(sj) n out(s2), откуда, ввиду условия теоремы, вытекает, что out^) = out^) n out(s2). Последнее означает, что out(sj) с out(s2).Таким образом, для произвольной последовательности ere s-traces(s02) справедливо out([s0j]п) с out([s02 ]п). ■1.2. АвтоматыОпределение 6. Под автоматом с входным алфавитом I и выходным алфавитом O в работе понимается наблюдаемый инициальный автомат, то есть пятёрка (T, I, O, ц, t0 > F , где T - непустое множество состояний с выделенным начальным состоянием t0; I и O - непересекающиеся множества входных и выходных действий соответственно, объединение которых мы обозначаем как A. Отношение переходов цс TхIхOхT есть функция, отображающая подмножество множества T х I х O в T .Пусть F = {T,I,O,ц,t0>F - некоторый автомат, t,t- какие-то состояния из T . Будем использовать следующие обозначения: для всех входных действий i и всех выходных действий o мы пишем t -»t', если и только если (t, i, o, t'> e ц ; г -, если и только если существует такое состояние t' е T , что t --- t'; иt^^^^, если и только если для всех t' е T не выполняется t --- t'. Отношение ц расширяется на входо-выходные последовательности следующим образом:T х (I х O) х T - наименьшее множество, удовлетворяющее следующим правилам: t ^> t 'л t' "° > t''Б 'Ц.1 / Оt =^> ts =^> s''Здесь, так же как и ранее, s обозначает пустую входо-выходную последовательность. Будем писать t=>t' тогда и только тогда, когда (t,ц,t'> e=> , t=> - тогда итолько тогда, когда существует такое t' е T , что (t, ц, t'> e=> , и tß> - тогда и только тогда, когда для всех t ' е T выполняется {t, ц, t') , где r\e (I хО)".Аналогично полуавтоматам введём следующие операторы и функции (здесь t е T , T 'с T , i e I re (I хО)"):defП def1..[t]n = {t'e T | t => t'}. Соответственно для T' - [T\ = Цет, [t]n .def def2..out(t, i) ={o e O | t "" >}. Для T' - out (Г', i) = [J (ET,out(t, i).def def3..in(t)={i e I | 3o e O : г --->}. Для T' - in(r') = \J ^ in(t).def П4..Tr(t)=(ле(/xO)' | t.def6. init(t)={(/, o)e I x O | г -.В этой работе мы рассматриваем только связные автоматы, то есть такие автоматы F = (T, I, O, Ц, t0 >F , для которых верно der(t0) = T, то есть всякое состояние достижимо из начального.Определение 7. Автомат F = (T, I, O, ц, г0 >F назовём полностью определённым, если в каждом состоянии t е T определен переход по каждому входному символу i е I, то есть найдутся такие o е O и t' е T , что t --- t'.-И.Определение 8. Пусть заданы автоматы F1 = {T1, I, O, ц1 , t01 > F и F2 = {T2,1,O, ц2, t02>F . Пересечением автоматов F1 и F2 назовём автомат F1 гч F2 = (Г, I, O, ц, (t01,t02»F , где T с T х T2 - минимальное множество, полученное с использованием следующего правила для ц:2 где tj, t/e T/ t2, t2 е T.Утверждение 4. Пусть F= I, O, ц, t01 > f , F2 = (T,, I, O, ^, tm > f и F гч F2 = (T, I, O, X, (t01,t02»F . Тогда справедливо следующее:1..init«/1, t2» = init(t1) n init(t2), где tl e Tl, t2 e T2 и {tl, t2 > e T.2..Tr «ti, t2 >) = Tr (ti) n Tr(t2).4.3.t1 =>t/ и t2 ^t'2 тогда и только тогда, когда (tl,t2>^(tj',t'2), где tj, t[ e Tl,t2, t'2 е T2 и ne (I x O)*.4.4.Пересечение Fl n F2 - связный автомат.Определение 9. Пусть F1 = (T1,I,O,\i1,t01>F и F2 = (T2,1,0,ц2,t02>F - наблюдаемые автоматы. Автомат Fl называется квази-редукцией автомата F2 (обозначение F ^ F2), если Fj - полностью определённый автомат и для всякой последовательности п из Tr(t02) и для всякого входного символа i из in([/02]n) справедливо out([t01 ]л, i) с out([?02]л, i).Отметим, что данное выше определение расширяет понятие квази-редукции, известное ранее (см., например, [1]), на наблюдаемые автоматы с так называемыми негармонизированными трассами.Утверждение5. Пусть Fl = (T1,I,O,^,t01 >F и F2 = F - два автомата, Fj - полностью определённый автомат, и пусть F1 гч F2 = (Г, I, O, ц, (701,t02»F . Тогда, F1 г< F2, если и только если для любого состояния (t1, t2 > пересечения Fl n F2 и для любого входного действия i е in(t2) выполняется out((t1, t2 >, i) = out(t1, i), где tl e T, t2 e T2.Доказательство. Необходимость. Пусть F1 r< F2, то есть для всякой последовательности r\e Tr (t02) и всякого входного действия i е in([t02 ]n ) выполняется out([t01 ]n, i) с out([t02]n, i). Рассмотрим в пересечении Fj n F2 состояние (t1,t2>, достижимое из начального состояния (t01, t02 > по последовательности n.Согласно свойству пересечения 4.4, t01 => t1 и t02 => t2, то есть пе Tr(t01) и re Tr (t02). Так как F1 и F2 - наблюдаемые автоматы, то [t01 ]n ={t1} и [t02 ]n = {t2}. Из свойства 4.4 следует, что для всякого i е I, а значит, и для всякого i е in(t2), верно out((t1,t2>, i) = out(t1, i) n out(t2, i), а это, совместно с условием теоремы, означает, что для любого i е in(t2) справедливо out((t1,t2>, i) = out(t1, i), что, ввиду произвольности выбора состояния {tl, t2 > е T, завершает доказательство.Достаточность. Пусть для всякого состояния (tj, t2 >е T и любого i е in(t2) верно out((t1, t2>, i) = out(t1, i). Рассмотрим произвольную последовательностьre Tr (t02). Если t01 /=> , то, поскольку пустое множество - подмножество любого множества, для всякого i е in([/02]n) верно out([t01 ]n, i) с out([t02]n, i). Пустьt01 => и пусть (помним, что Fl и F2 - наблюдаемые автоматы) [t01 ]n = } и [t02 ]n = {t2}. Тогда, согласно свойству 4.4, []n ={{t1, t2 >}. Из свойства 4.4 пересечения следует, что для всякого i е I, а соответственно и для любого i е in(t2), выполняется out((t1,t2>, i) = out(t1, i) n out(t2, i). Условие теоремы позволяет заключить, что для любого i е in(t2) верно out(t1, i) с out(t2, i). Таким образом, для произвольной последовательности r\eTr(t02) и для всякого i е in(t2) справедливо out([t01 ]_, i) с out([t02]_, i). ■ 2. Переход от полуавтомата к автоматуПусть дан детерминированный связный полуавтомат L = {S, I, O, X, s0 > L. Для него построим автомат FEL = {T, IE, 0eS , ц, t0 >F, где е,, е0 ^ A - специальные новые входной и выходной символы (здесь и далее для удобства полагаем IE = I u (s,}, OeS = O и (so, 8}), а ц определяется следующими правилами:.s -->s'a a е Is -->s a a е O 8(s)а/г , 's Ja , ' Б ./5tt't1>t't1>tПри этом каждому состоянию автомата FEL соответствует состояние полуавтомата L и наоборот, то есть состояния в полуавтомате, как обычно, будем обозначать буквой s с индексами или без - s, s', sk и так далее, а в автомате буквой t с индексами или без - t, t', tk. Считаем, что состоянию t автомата соответствует состояние s полуавтомата, состоянию t' - s' и так далее.Новый входной символ s, определяет ситуацию «ожидания выхода от системы», то есть, когда система достигает момента, что в ней возможен переход под действием пустого входного символа и наблюдатель желает «задействовать» этот переход, то ему необходимо «подождать» выходной реакции системы, не подавая ничего на вход. Новый выходной символ so определяет обратное: система при-нимат входное действие, но наблюдатель не должен ожидать реакции от автомата (на данном переходе). Особо подчеркнём, что по постороению в автомате FEL от-сутсеуют переходы с пометками вида е,. 1г0, il/i2, ol/o2, il/o1, ollil, где il, i2 e I,Процесс построения автомата FEL позволяют говорит о следующих его свойствах:Утверждение 6. Пусть L = {S, I, O, X, s0 > L - заданный полуавтомат, а FEL = {T, /Е , OE s, ц, t0 >F - построенный по нему автомат. Тогда справедливы следующие утверждения:1Если L - полностью определённый по входам полуавтомат, то автомат FEL - полностью определённый автомат.2Если L - детерменированный полуавтомат, то FEL - наблюдаемый автомат.3Если L - пересечение некоторых полуавтоматов Ll и L2, то FEL - пересечение автоматов и F^2 (то есть FEL'nL"2 = FEL' n FEL2).По построению автомата FEL справедлива следующая лемма. Напомним, что As = I и O и {8}, а операция iH - проекция на множество H.Лемма 1. Пусть задан полуавтомат L = {S, I, O, X, s0 >L, по которому построен автомат FEL . Тогда Tr(FEL ) iAg = s - traces(L) .Следствие 1. Для любой последовательности а из s - traces(L) и для любого действия a из Аъ справедливо [L]a -a-> тогда и только тогда, когда [FsL ]_ -, где r\lA = а ; i/o = е,/а, если a е O,, и i/o = a/г , если a е I.Теорема 1. Пусть Ц= {Sl, I, O, Xl, s01 >L и L2 = (S2,1,0, X2, s02 >L - два полуавтомата, причём L1 - полностью определённый полуавтомат. Тогда L1 ioco L2,если и только если FL Т3 F/2.Доказательство. Утверждения 3 и 5 позволяют доказывать вместо истиности утверждения « L1 ioco L2, если и только если FL F^2 » истинность утверждения «для произвольного состояния (Sj, s2 )е S пересечения Lj n L2 выполняется out((s1, s2>) = out(s1), если и только если для произвольного состояния (tj, t2 > е Tпересечения F/1 n F/2 и для произвольного входного действия i из in(t2) выполняется out((?1, t2>, i) = out(t1, i) », где S - множество состояний полуавтоматаLj n L2, а T - множество состояний автомата F^1 n F^2.Необходимость. Пусть для любого состояния (s1, s2 )е S верно out((s1, s2>) = out(s1) .Рассмотрим произвольное состояние (tj, t2 >е T пересечения F/1 n F/2, достижимое из начального по некоторой последовательности г\. Свойство 6.6 и следствие 1 из леммы 1 позволяют заключить, что в этом случае в пересечении Lj n L2 достижимо состояние (s1, s2 > по последовательности а = r\lA , причем,так как L, L2 и Lj n L2 - детерменированные полуавтоматы, [s01 ]п = {s1}, [S02L ={s2}, []n ={}. По условию out«s, S2>) = out(s1) и, следовательно, по построению F/1, F^2 и n F/2, справедливо out((t1, t2 >, s,.) = out(t1, s,.) или, что то же самое,init«/,, t2» n ({s,} x OeS) = init(t,) n ({s,} x OBS) .(*)о оНапомним, что в автоматах отсутствуют переходы с пометками вида е,. /е0. Рассмотрим переход, определённый в состоянии t2 автомата F/2 , под действиемпроизвольного входного символов i е in(t2 )\{s,}. Поскольку автомат F/1 (свойство 6.6 и условие теоремы) - полностью определённый, то в состоянии tl автомата F/1 определён переход под действием входного символа i, причём, согласноправилам построения автоматов F/1 и F/2 , в обоих случаях переход будет помечен парой Иг0. Последнее позволяет переписать (*) следующим образом:init«t1,t2>) n (in(t2) x OeS) = init(t1) n (in(t2) x OB s),о очто в виду произвольности выбора состояния (t1, t2 > завершает доказательство.Достаточность. Пусть для произвольнго состояния {tl, t2) е T и произвольного входного символа i е in(t2) выполняется out((t1,t2>, i) = out(t1, i).Рассмотрим произвольное состояние (s1, s2 > пересечения L1 n L2, достижимое из начального состояния по последовательности а = a1... an. Как и в случае доказательства необходимости, это означает, что в автомате i7/1 n i7/2 достижимо состояние {t1,t2> по последовательности ц = i1/o1 .../„/on, где zj/оу = ay/so, если и только если ay е I, и /уloj = s,-/о,-, если и только если ay е Os. Ввиду детерминированности полуавтоматов и свойства 6.6, [(s01, s02>]п = {(s1, s2>}, [s01 ]п = {s1},[ S02 L = {S2 } , [Ooi > Z02 )]л = > ?2 )} , [t01 ]„ =и [t02 ]n = {t2 } . З^шета^ что автома-ты F^1, F^2 и FBLl n i7/2 строятся таким образом, что, каково бы ни было состояние t такого автомата, in(t) эе, , поскольку в порождающем его состоянии полуавтомата s либо определён переход по некоторому выходному символу o е O и соответственно в автомате появляется переход по паре е,./о, либо состояние s устойчивое, а значит, в автомате определён переход, помеченный парой е,./8. Отсюда out(sj) = out(?j, s,.) и out((sl,s2>) = out((tj,t2>, s,.), что ввиду условия «для любого i е ia(t2) верно out((tj,t2>, i) = out(?j, i) » позволяет заключить, чтоout((Sj, s2>) = out(sj). Последнее завершает доказательство, так как состояние(S, s2 > было выбрано произвольно. ■3. Модели неисправности и полные проверяющие тесты3.1. Проверяющие тесты и модель неисправности для входо-выходных полуавтоматовОпределение 10. Для заданого детерминированного полуавтомата L = (S, I, O, X, s0 > L через Ls обозначим полуавтомат (S, I, Os, Xs, s0 >L, у которогоXs = Xu«s,5,s>|5(s)}.То есть полуавтомат Ls отличается от L добавлением петель с пометкой 5 в устойчивых состояниях. Известно [2], что s - traces(L) = traces(Ls).Определение 11. Под тестовым примером в теории входо-выходных полуавтоматов будем понимаеть полуавтомат C = {V, I, Os,XC,v0>L, удовлетворяющий следующим требованиям:1..V 3 {pass, fail}.2..Граф переходов полуавтомата C - ациклический.3..Для всякого v е V \ {pass, fail} либо init(v) = Os, либо init(v) = {i}, i е I.4..init(pass) = init(fail) = 0 .Конечное множество тестовых примеров назовём конечным проверяющим тестом.Отметим, что с практической точки зрения нас интересуют только конечные проверяющие тесты, поэтому только их и будем рассматривать далее.Определение 12. Говорят, что полуавтомат L = (S, I, O, X, s0 > L согласуется стестовым примером C = {V, I, Os, XC, v0 > L, если и только если ни одна последовательность сте s - traces (L) не переводит полуавтомат C из начального состояния в состояние fail, то есть (Sх {fail}) n der(Ls n C) = 0 .Определение 13. Под моделью неисправности в теории полуавтоматов будем понимать следующую тройку (LM, ioco , EL >, где LM - полуавтомат-спецификация (или просто спецификация), EL - множество полностью определённых полуавтоматов с входным алфавитом I и выходным алфавитом O, которое называется областью неисправности, причём для всякого полуавтомата L' е EL выполняетсяL io/o Lm .Иными словами, в модели неисправности спецификация описывает допустимое поведение проверяемой системы, область неисправности описывает допустимые в системе ошибки, при этом система считается безошибочной, если она (точнее полуавтомат, описывающий её) находится в отношении ioco со спецификацией.Определение 14. Полный проверяющий тест относительно модели неисправности (LM, ioco , EL > есть такой (конечный) проверяющий тест T, что спецификация LM согласуется с любым тестовым примером из T, а для всякого полуавтомата L' из EL в множестве T найдётся такой тестовый пример C, что полуавтомат L' не согласуется с ним.Неформально, если полуавтомат L', который описывает поведение проверяемой системы, не находится в отношении ioco с LM, то в полном проверяющем тесте должен существовать тестовый пример, который обнаружит этот факт. В этой работе мы не обсуждаем, каким образом входные воздействия подаются на проверяемую систему и как наблюдатель убеждается в том, что система согласуется или не согласуется с тестовым примером. Заметим только, что поскольку в проверяемой системе в каком-то из её состояний может быть определено несколько выходных реакций, то тестовые примеры при анализе системы подаются несколько раз, чтобы пронаблюдать все возможные выходные реакции системы.3.2. Проверяющие тесты и модель неисправности для автоматовОпределеине 15. Под тестовым примером в теории автоматов будем понимать такой автомат C = {V, I, O, цс, v0>F, для которого справедливы следующие условия:1..V э {pass, fail}.2..Граф переходов автомата C - ациклический.3.Для всякого v eV \ {pass, fail} выполняется | in(v)|=1 и out(v, i) = O, гдеm(v) = .4.init(pass) = init(fail) = 0 .Конечное множество тестовых примеров назовём конечным проверяющим тестом.Аналогично случаю для полуавтоматов здесь нас интересуют только конечные тесты.Определение 16. Говорят, что автомат F = {T, I, O, ц, s0 > F согласуется с тестовым примером C = {V, I, O, цс, v0 > F, если и только если никакая последовательность r\e Tr(F) не переводит автомат C в состояние fail, то есть (Tх {fail}) n der(F n C) = 0 .Определение 17. Моделью неисправности в теории автоматов будем называть тройку (FM, 77 EF >, где FM - автомат-спецификация (или просто спецификация), EF - множество полностью определённых автоматов с входным алфавитом I и выходным алфавитом O, которое называется областью неисправности, причём для всякого автомата F' из EF выполняется F' ^ FM .Определение 18. Полный проверяющий тест относительно модели неисправности (FM, 77 EF > есть такой (конечный) проверяющий тест T, что спецификация FM согласуется с любым тестовым примером из T, а для всякого F' из EFв множестве T найдётся такой тестовый пример C, что автомат F' не согласуется с C .3.3. Построение полного проверяющего теста для входо-выходных полуавтоматов на основе проверяющего теста для автоматовВ теории входо-выходных полуавтоматов неизвестно как построить (конечный) полный проверяющий тест относительно модели неиспрвности (L, ioco, EL)для случая, когда EL - конечное множество полуавтоматов, однако в теории автоматов известен метод [1] построения полного проверяющего теста относительно модели неисправности (F, Т3, EF), EF - множество всех автоматов, число состояний в которых не превышает наперёд заданного числа, или EF - множество всех подавтоматов специального мутационного автомата.В этом разделе, на основе результатов раздела 3, мы показываем, что если при тестировании системы есть возможность наблюдать молчание и если число состояний в каждом полуавтомате из EL не превышает наперёд заданного числа, то полный проверяющий тест относительно модели неисправности (L, ioco, EL)можно построить на основе полного проверяющего теста для соответствующей автоматной модели неисправности.Пусть задана модель неисправности ML = {L,ioco,EL>, EL ={L1,L2,...} для полуавтоматов, по ней построена автоматная модель неисправности MF = (FBL, r, EF ={F^1, F^2,...} и для модели MF построен полный проверяющий тест TF. Рассмотрим произвольный тестовый пример CF из TF. Согласно определению тестового примера, в любом из его состоянии v, таком, что v Ф pass и v Ф fail, будет определён переход под действием всех пар из {/} х OSs, где i е /в. Причём, если i е I (то есть i ^s,), то для любого o е Os имеет место v -^-» fail, так как автомат-спецификация FBL не допускает подобных переходов, ввиду правил построения этого автомата. Более того, переходы этого вида в тесте бессмысленны, поскольку, по правилам построения, в проверяемых автоматах, то есть автоматах из множества EF, принципиально невозможны переходывида t --- t', а следовательно, подобные переходы невозможны и в пересечении этих автоматов с тестовыми примерами, а значит, такие переходы никак не отразятся на вердикте «согласуется/не согласуется». Если же in(v) = {е,.}, то(согласно тем же соображениям) бессмысленным будет переход по паре е, 1г0.Опираясь на приведённые выше рассуждения, можно ввести следующее преобразование тестовых примеров из полного проверяющего теста TF для автоматноймодели неисправности MF = {FEL, г, EF = {F^1, F^2,...}, построенной по полуавтоматной модели неисправности ML = {L, ioco, EL >, EL = {L1, L2,...}.Пусть задан автоматный тестовый пример CF = {V, /Е, Os, v0 >, CF e TF, TF -Б Бполный проверяющий тест относительно модели неисправности MF = {FEL, ~

Скачать электронную версию публикации