В статье исследуется отношение неразделимости для недетерминированных автоматов, в которых каждое состояние может обладать целочисленной задержкой (тайм-аутом). Если тайм-аут заканчивается и на автомат не было подано ни одного входного символа, то автомат изменяет свое состояние согласно переходу по этой временной задержке. Предлагается алгоритм построения разделяющей последовательности для таких автоматов, т.е. такой временной входной последовательности, на которую множества выходных последовательностей автоматов не пересекаются, и соответственно достаточно подать разделяющую последовательность на эти автоматы один раз, чтобы по выходной реакции различить их.
Studing non-separability relation for non-deterministic finite statemachines with time-outs.pdf В статье рассматривается одна из модификаций классической модели конечно-го автомата [1] - модель с тайм-аутами [2 - 4], которую в рамках данной работымы будем называть временным автоматом. В этой модели, как и в модели конеч-ного автомата, есть состояния, входные символы, выходные символы; переходыиз состояния в состояние могут осуществляться при подаче входного символа исопровождаются выдачей выходного символа и, кроме того, возможны переходыпо временным задержкам (тайм-аутам), т.е. по прошествии некоторого времени,если в течение этого времени на автомат не поступил ни один входной символ.При переходе по тайм-ауту на автомат не поступают внешние воздействия, и этадополнительная возможность позволяет более полно описать поведение многихсовременных технических систем. В качестве примера можно привести сотовыйтелефон, у которого по истечению некоторого времени гаснет экран, mp3-плеер идругие системы.Для временных автоматов только начаты исследования различных отношенийконформности [3]. Эти отношения и их свойства во многом заимствуются из тео-рии конечных автоматов. Отношение неразделимости [5, 6], исследуемое в дан-ной статье, также было введено изначально для конечных автоматов, а именно,для автоматов с недетерминированным поведением. Данное отношение замеча-тельно тем, что при тестировании не требуется выполнения «всех погодных усло-вий», т.е. необходимости подавать каждую тестовую последовательность до техпор и при таких условиях, чтобы пронаблюдать все выходные последовательно-сти системы на поданную входную последовательность. На практике затрудни-тельно обеспечить выполнение такого предположения, и поэтому построение тес-тов с использованием отношения неразделимости актуально для моделей неде-терминированных конечных автоматов [5, 6] и их модификаций [3, 4]. В даннойработе предлагается алгоритм построения разделяющей последовательности длявременных автоматов с тайм-аутами, на основе которого можно построить пол-ный проверяющий тест относительно неразделимости при явном перечислениивсех неисправностей.1. Основные определения и обозначенияВ данной работе временным автоматом (автоматом с тайм-аутами) называет-ся шестерка A = (S, I, O, s0, A, A), где S - конечное непустое множество состоя-ний с выделенным начальным состоянием s0, I и O - конечные непересекающиесявходной и выходной алфавиты, A S I O S - отношение переходов. Функ-ция A: S S ( {}), где − множество натуральных чисел, есть функциязадержки, определяющая для каждого состояния тайм-аут, т.е. время ожиданиявходного символа без изменения состояния, причём если для некоторого со-стояния s имеет место A(s) = (s', ), то s = s'. Таким образом, классический ко-нечный автомат [1], в том числе недетерминированный [5, 6], можно рассматри-вать как временной автомат, в котором для всех состояний s S имеет местоA(s) = (s, ), т.е. конечный автомат, в отличии от временного, сколь угодно долгоожидает входного символа, не изменяя при этом текущее состояние.Временному автомату ставится в соответствие внутренняя переменная (часы),принимающая целые неотрицательные значения и указывающая время, прошед-шее с момента достижения текущего состояния [2 - 4] (или с момента выдачи по-следнего выходного символа). Если (s, i, s', o) A, то автомат A в состоянии sна входной символ i может выдать выходной символ o и изменить своё состоя-ние на s', причем после этого соответствующая временная переменная прини-мает значение 0. В данной работе мы не рассматриваем задержки выходныхсимволов, т.е. полагаем, что временной автомат выдаёт выходной символ в тотже самый момент, когда принимает входной символ и, возможно, меняет своёсостояние.Если для каждой пары (s, i) S I существует не более одной пары(o, s) O S, такой, что (s, i, o, s) A, то временной автомат A называется де-терминированным; иначе временной автомат называется недетерминированным.Если для каждой пары (s, i) S I существует, по крайней мере, одна пара(o, s) O S, такая, что (s, i, o, s) A, то S называется полностью определен-ным. Временной автомат A называется наблюдаемым, если для любой тройки(s, i, o) S I O существует не более одного состояния, такого, что(s, i, o, s) A.Временной входной символ есть пара 〈i, t〉 I 0+ , где 0+ - множество це-лых неотрицательных чисел; временной входной символ 〈i, t〉 показывает, чтовходной символ i подается в момент, когда значение временной переменнойравно t. Последовательность 〈i1, t1〉〈i2, t2〉…〈il, tl〉 временных входных символовназывается временной входной последовательностью длины l.Для того чтобы расширить отношение переходов временного автомата навременные входные символы, введем специальную функцию timeA: S 0+ S,позволяющую определить по текущему состоянию автомата состояние автомата вмомент времени, когда значение временной переменной равно t [4]. Для опреде-ления значения функции timeA(s, t) рассмотрим последовательность тайм-аутовA(s) = (s1, T1), A(s1) = (s2, T2), …, A(sp-1) = (sp, Tp), такую, что T1 + T2 +…+ Tp-1 ≤ t,но T1 + T2 + … + Tp > t. В этом случае timeA(s, t) = sp-1. Если A(s) = (s, ), тоtimeA(s, t) = s для каждого значения переменной t. Для каждого временного вход-ного символа 〈i, t〉 к отношению A добавляется переход (s, 〈i, t〉, s', o), если итолько если (timeA(s, t), i, s', o) A.Множество всех входных временных последовательностей обозначается It*.Для полностью определенного временного автомата A функция outS, отображаю-щая множество S It* во множество выходных последовательностей, т.е.outA(s, ): S It* O*, вводится следующим образом. Для состояния s и времен-ной входной последовательности = 〈i1, t1〉 … 〈il, tl〉 последовательностьo1 … ol outS(s, ), если существуют состояния s1 = s, …, sl+1, такие, что для каж-дого j {1, …, l} временной автомат A имеет временной переход (sj, 〈ij, tj〉, oj, sj+1),и будем говорить в этом случае, что пара (, outA(s, )) может перевести автоматA из состояния s в состояние sl+1. Пара «временная_входная_последователь-ность_ / выходная_последовательность_» называется временной входо-выход-ной последовательностью или временной трассой временного автомата A в со-стоянии s, если outA(s, ). Можно сказать, что временные трассы характери-зуют функциональное поведение временного автомата (относительно временныхвходных последовательностей).1 Множество всех функциональных трасс в на-чальном состоянии автомата A обозначим TTrA.Состояние s' называется 〈i, t〉/o-преемником состояния s, если (s, 〈i, t〉, s', o) A. Состояние s в этом случае называется 〈i, t〉/o-предшественником состоянияs'. Соответственно любой 〈i, t〉/o-преемник состояния s (〈i, t〉/o-предшественниксостояния s') можно рассматривать как просто 〈i, t〉-преемник состояния s(〈i, t〉-предшественник состояния s'). Множество всех 〈i, t〉/o-преемников состоянияs будем обозначать sucA(s, 〈i, t〉, o), множество всех 〈i, t〉-преемников состояния sбудем обозначать sucA(s, 〈i, t〉), и в обоих случаях для краткости символ 〈i, 0〉 бу-дем заменять символом i.Если временной автомат A детерминированный, то для каждого состояния s икаждой временной входной последовательности множество outA(s, ) содержитне более одного элемента. Для полностью определенного временного автомата Aмножество outA(s, ) не является пустым для любых s S, It*.Пусть A = (S, I, O, s0, A, A) и B = (P, I, O, p0, B, B) - полностью определен-ные автоматы с тайм-аутами. Автомат B называется редукцией автомата A, еслиTTrB TTrA; если TTrB ⊄ TTrA, то автомат B не является редукцией автомата A.Временные автоматы A и B называются неразделимыми, если выходные реакцииавтоматов на любую временную входную последовательность пересекаются,т.е. outA(s0, ) outB(p0, ) ∅; в противном случае автоматы называются разде-лимыми. Временная входная последовательность , такая, что outA(s0, ) outB(p0, ) = ∅, называется разделяющей последовательностью для временных ав-томатов A и B.Пересечением A B называется наибольший связный подавтомат C = (Q, I, O,q0, C, C) автомата (R, I, O, q0, C, C), в котором R = S K P K, гдеK = {0, …, k}, k = min(maxA(s), maxB(p)), начальное состояние есть четверка(s0, 0, p0, 0) и отношение переходов C и функция C определены по следующимправилам [3]:1. Отношение переходов C содержит четверку [(s, k1, p, k2), i, o, (s, 0, p, 0)],если и только если (s, i, o, s) A и (p, i, o, p) B.1 В данной статье при определении временных трасс мы опускаем слово «функциональная», посколькуне рассматриваем задержки выходных символов.2. C((s, k1, p, k2)) = [(s, k1, p, k2), k], где k = min( A(s) k1 − , B(p) k2 − ).Состояние (s, k1, p, k2) = (A(s)S, 0, B(p)P, 0), если ( A(s) = илиB(p) = , или ( A(s) k1 − ) = ( B(p) k2 − )). Если ( A(s) k1 − ) ,( B(p) k2 − ) Z+ и ( A(s) k1 − ) < ( B(p) k2 − ), то состояние(s, k1, p, k2) = (A(s)S, 0, p, k2 + k).Если ( A(s) k1 − ) , ( B(p) k2 − ) Z+ и ( A(s) k1 − ) > ( B(p) k2 − ),то состояние (s, k1, p, k2) = (s, k1 + k, B(p)P, 0).А л г о р и т м 1П остроение пересечения двух полностью определенных временных автоматовВход: Временные автоматы A = (S, I, O, s0, A, A) и B = (P, I, O, p0, B, B).Выход: Пересечение C = (Q, I, O, q0, C, C).1: Добавить в первоначально пустое множество Q состояние q0 = (s0, 0, p0, 0);2: Пока во множестве Q есть нерассмотренные состояния;3: Для каждого нерассмотренного состояния q=(s, k1, p, k2) из множества Q;4: Для каждой пары i/o определить множество состояний Q' и пополнить множе-ство переходов C, добавляя состояние q'=(s', 0, p', 0) в Q' и переход [(s, k1, p,k2), i, o, (s', 0, p', 0)] в C ( s , i , s', o) A и (p, i , p ', o) B ;5: Q := Q Q' ;6: Если ( A(s)( N {}) или B(p)( N {}) ), то выполнять:k := min( A(s) k1 − , B(p) k2 − );7: Если (A(s)( N {}) = или B(p)( N {}) = или( A(s) k1 − ) = ( B(p) k2 − ) ),8: то q' := (ΔA (s), 0, ΔB (p), 0);9: Иначе10: если ( A(s) k1 − ) < ( B(p) k2 − ),то q' := (A(s)S, 0, p, k2 + k);11: если ( A(s) k1 − ) > ( B(p) k2 − ),то q' := (s, k1 + k, B(p)P, 0);12: Доопределить функцию C: C(q) = (q', k); Q := Q { q'};13: Автомат C = (Q, I, O, q0, C, C) - искомый автомат A B; Конец.На рис. 1 приведены два временных автомата A и B, на рис. 2 - автомат-пересечение A B.Рис. 1. Временные автоматы A и BРис. 2. Автомат A B2. Построение разделяющей последовательностидля полностью определенных временных автоматовРазделяющая последовательность для временных автоматов A и B строится наоснове дерева преемников пересечения A B . Если автоматы A и B не являютсяразделимыми, то на выходе алгоритма выдается соответствующее сообщение.А л г о р и т м 2Построение разделяющей последовательностидля двух полностью определенных временных автоматовВход: Полностью определенные временные автоматыA = (S, I, O, s0, A, A) и B = (P, I, O, p0, B, B).Выход: Разделяющая последовательность для автоматов A и B (если автоматы A и B раз-делимы) или сообщение, что автоматы A и B неразделимы.1: Построить пересечение C = A B;2: Если C - полностью определенный автомат, товыдать сообщение «автоматы A и B неразделимы»; Конец.3: k: = 0; Edge: = ∅; Qk 0 : = {〈q0, 0〉}; Qk : = {Qk 0 };4: Пока не выполнится одно из следующих правил усечения дерева преемников:5: Правило 1: для некоторого множества Qk j Qk, j ≥ 0, существует входной символ isepтакой, что для каждого состояния q, 〈q, t〉 Qk j, переход из q по входному символуi-sep не определен;6: Или7: Правило 2: для каждого множества Qk j Qk существует Qam Qa, a < k, такое, чтоQk j Qam;8: выполнять:9: Qk+1: = ∅;10: Для каждого подмножества Qk j Qk, j = 0, ..., |Qk |-1, для которого не существуетQam Qa, a < k, такого, что Qk j Qam, выполнять:11: Для каждого входного символа i12: Построить множество M : = ( , ) {0}kjC Qq Qsuc q i ∪ ;13: Qk+1= Qk+1 M; добавить тройку (Qk j, i, M) во множество Edge;14: Если не для всех q, 〈q, t〉 Qkj, (C(q))( N {}) = , то определить для мно-жества Qk j = {〈q1, t1〉, 〈q2, t2〉,…,〈qr, tr〉} минимальную задержку T и множествопреемников R по этой задержке следующим образом:15:1: min{ u r{ u u}T T t≤ ≤= − , где Tu = (C(qu))( N {});16: R := {〈q1', t1'〉, 〈q2', t2'〉,…,〈qr', tr'〉},где для всех u {1, …, r}qu' = timeC(qu, tu + T);Если (Tu = или Tu = tu + T), то tu' = 0;Если (Tu > tu + T), то tu' = tu + T;17: Qk+1= Qk+1 R; добавить тройку (Qk j, T, R) во множество Edge;18: k:=k+1;19: Если выполнилось Правило 2 усечения дерева преемников, то выдать сообщение «ав-томаты A и B неразделимы», Конец.20: Построить последовательность ребер (Q0 0, g1, Q1 j1 ), ( Q1 j1 , g2, Q2 j2 ), …, ( 1 ( 1)k Qk j− − ,gk, Qk jk ), такую, что для множества Qk jk выполнилось Правило 1 усечения деревапреемников, ( 1 ( 1)l Ql j− − , gl, Ql jl ) Edge для каждого l {1, …, k}, и gl {I }.21: По построенной последовательности ребер выписать последовательность g1g2…gk извходных символов и временных задержек.22: Построить временную входную последовательность = … следующимобразом:23: j := 0; Tj := 0; r := 0;24: Пока (j ≤ k)25: Если gj I, то ir := gj , tr := Tj , r := r+1, Tj := 0;26: иначе Tj := Tj + gj ;27: j := j+1;28: m := r; ir := i-sep , tr := Tj ;29: Последовательность = … − искомая разделяющей последовательно-стью для автоматов A и B, Конец.Теорема. Если алгоритм 2 возвращает входную последовательность , то есть разделяющаяляется минимальная временная задержка. Вычисление множества преемников поэтой задержке осуществляется так же, как при построении пересечения автоматов.Внесение данного дополнения в алгоритм связано с тем, что пара временных ав-томатов может быть разделима по временной входной последовательности, т.е.прежде, чем подать входной символ, необходимо выждать некоторое время, длятого, чтобы автомат-пересечение достиг нужного подмножества состояний. При-чем дуге, помеченной входным символом, может предшествовать последователь-ность из нескольких дуг, помеченных временными задержками.Согласно алгоритму, если для некоторой вершины, помеченной множествомQk jk , выполнилось Правило 2 усечения дерева преемников, то это означает, чтонет нераскрытых вершин, не объявленных листьями, и множество пар в каждой усеченной вершине дерева содержат в себе множество парнекоторой вершины на одном из предшествующих ярусов дерева, а значит, из та-кой вершины не может быть построена ветвь, соответствующая разделяющей по-следовательности.Если же для некоторой вершины, помеченной множеством Qk jk , выполняетсяПравило 1 усечения дерева преемников, то в строках 22 - 28 последовательность собирается по ветви дерева, ведущей из корня в данную вершину. При этомвременной входной символ формируется в результате суммирования всех задер-жек до очередного входного символа. Поскольку Правило 1 усечения дерева пре-емников перешло из алгоритма работы [6] без изменений, а переходы по времен-ным задержкам из множеств пар формируются согласно пра-вилам, регламентированным при определении совместного поведения временныхсистем (а именно, при построении пересечения), то последовательность будетразделяющей последовательностью для автоматов A и B. Пример. Для иллюстрации алгоритма 2 рассмотрим автоматы A и B на рис. 1.Автомат A B показан на рис. 2. По определению, множество Q0 = {Q00}, гдеQ00 = { 〈 (a, 0, c, 0), 0〉 }. При k = 0 мы получаем Q1 = {Q10 = { 〈 (a, 0, c, 0), 0〉}, Q11 = { 〈 (b, 0, c, 0), 0〉 } , Q12 = { 〈 (a, 0, d, 0), 0〉 } }, множество Edge = {(Q00, i1, Q10 ), (Q00, i2, Q11 ), (Q00, 3, Q12 ) }. При k = 1 мы получаемQ2 = {Q20 = { 〈 (b, 0, c, 0), 0〉 }, Q21 = { 〈 (a, 0, c, 0), 0〉 } , Q22 = { 〈 (b, 3, d,0), 0〉 }, Q23 = { 〈 (b, 0, c, 0), 0〉, 〈 (b, 0, d, 0), 0〉} , Q24 = { 〈 (a, 0, c, 0), 0〉,〈 (b, 0, d, 0), 0〉 } }, множество Edge = {(Q00, i1, Q10 ), (Q00, i2, Q11), (Q00, 3, Q12),(Q11, i1, Q20 ), (Q11, i2, Q21), (Q11, 3, Q22), (Q12, i1, Q23 ), (Q12, i2, Q24)}.Можно видеть, что поведение автомата A B не определено в каждом состоя-нии множества Q22 по входному символу i-sep = i1. Таким образом, временнаявходная последовательность разделяет автоматы A и B.В связи с тем, что при существовании разделяющей последовательности по-строение дерева прекращается, как только допустимо усечение по Правилу 1, по-следовательность (если существует) не обязательно будет кратчайшей по числувременных входных символов. Может оказаться, что если продолжать «тянуть»другие ветки дерева и вновь дойти до усечения по Правилу 1, то получимболее длинную последовательность дуг (Q00, g1, Q1 j1 ), ( Q1 j1 , g2, Q2 j2 ), …,( 1 ( 1)k Qk j− − , gk, Qk jk ), но ей будет соответствовать более короткая временная по-следовательность (по числу входных символов), поскольку большее число дугбыло помечено временными задержками.ЗаключениеВ работе представлено исследование отношения неразделимости для автома-тов с тайм-аутами и предлагается алгоритм построения разделяющей последова-тельности для двух таких автоматов. Следует заметить, что построенная по дан-ному алгоритму разделяющая последовательность не обязательно будет разде-ляющей последовательностью минимальной длины (по числу временных входныхсимволов) для данной пары автоматов. Для нахождения разделяющей последова-тельности минимальной длины нужно при усечении дерева преемников по Пра-вилу 1 запоминать построенную последовательность, но не прекращать дальней-ших построений; затем выбрать самую короткую из множества построенных по-следовательностей.Рассмотренная в работе модель временного автомата является упрощеннымвариантом модели временного автомата, введенной в [2 ], поскольку в ней отсут-ствуют задержки по выходным символам. Однако предложенный алгоритм по-строения разделяющей последовательности может служить основой при анализеотношения неразделимости для «полноценного» варианта временного автомата.Развитием данного исследования может также стать разработка методов построе-ния полных проверяющих тестов для временных автоматов относительно нераз-делимости.
Гилл А. Введение в теорию конечных автоматов. М.: Наука, 1966. 272 с.
Merayo M.G. Formal testing from timed finite state machines // Computer Networks. 2008. V. 52 Nо. 2. P. 432−460.
Громов М.Л., Евтушенко Н.В. Синтез различающих экспериментов для временных автоматов // Программирование. 2010. № 4. С. 1−11.
Zhigulin M., Maag S., Cavalli A, Yevtushenko N. FSM-based test derivation strategies for systems with time-outs // Proc. conf. QSIC'2011. 2011.
Starke P. Abstract automata. American Elsevier, 1972. 419 p.
Spitsyna N., El-Fakih K., Yevtushenko N. Studying the Separability Relation between Finite State Machines // Software Testing, Verification and Reliability. 2007. V. 17(4). P. 227−241.
Вы можете добавить статью