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

2008

ВЕСТНИК ТОМСКОГО ГОСУДАРСТВЕННОГО УНИВЕРСИТЕТА Управление, вычислительная техника и информатика

№ 3

ПРОЕКТИРОВАНИЕ И ДИАГНОСТИКА ВЫЧИСЛИТЕЛЬНЫХ СИСТЕМ

УДК 618.5:519.68

М.Л. Громов

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

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

Ключевые слова: полуавтомат, автомат, тест, полный проверяющий тест, пересечение полуавтоматов, пересечение автоматов.

При построении проверяющих тестов для дискретных реактивных систем наиболее активно используются две модели с конечным числом переходов: конечные автоматы [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. Отношение переходов Àc 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^sa'> , если и только если для всех s' е S не выполняется s ——->s'.

В теории входо-выходных полуавтоматов понятие молчания [2] вводится следующим образом:

Определение 2. Состояние s е S полуавтомата L = {S, I, O, X, s0 )L назовём молчащим (устойчивым), если и только если для всякого a из O справедливо

я> . Для удобства дальнейших рассуждений введём предикат 8(^), принимающий значение «истина», если и только если состояние я - молчащее.

Неформально, полуавтомат, находясь в устойчивом состоянии, «отказывается» произвести какой-либо выходной сигнал. На практике наблюдаемость «молчания» обеспечивается введением определенного промежутка времени, в течение которого система «обязана» произвести выходной сигнал, если таковой возможен в текущем состоянии. Если в течение этого промежутка времени выходной сигнал от системы не поступает, то предполагается, что система достигла своего устойчивого состояния. Пусть 8й А - новый выходной символ, обозначающий возможность наблюдать молчание; А5 - сокращённая запись для А и {8}. Пусть ае А*, а е Аъ и 5, s, , я" е 5 . Тогда, расширяя отношение переходов на последовательности, можно ввести новое отношение 5 х А* х 5

как наименьшее множество, удовлетворяющее следующим правилам:

5 ^ 5 'Л 5 '-— Я " Я ^ Я 'л8

£ ’ О.й ’ 0.5

S ^ S S ^ S'' S ^ S'

а

Здесь s - пустая последовательность. Будем писать s ^s' тогда и только тогда,

когда (s, а, s') ; s^ тогда и только тогда, когда для всех s'e T выполняется

(s,а,s") , где ае As*

Для формализации описания мы вводим следующие операторы и функции (здесь S 'с S, s, s'e S , а е Aj*):

def а

1. [s]a = {s' e S | s ^ s'} - множество состояний, достижимых из состояния s по последовательности а . Поскольку здесь мы рассматриваем детерминированные полуавтоматы, то это множество состоит не более чем из одного элемента.

def

Соответственно для S' полагаем [S']а = ^ s^s, [s]a.

def

2. out(s) ={a e O | s ——-^} u {8 | 8(s)} - множество выходных символов, включая специальный символ 8, определённых в состоянии s. Для S' полагаем

def

out(S') = U ,out(s).

def

3. in(s)={i e I | s ——} - множество входных символов, определённых в со-

def

стоянии s. Для S' полагаем in(S') = ^ s^s in(s).

def а

4. s - traces(s) = {а e A* | s - язык полуавтомата с учётом молчащего символа 8.

def

5. traces(s) = s - traces(s) n A* - язык полуавтомата без учёта молчащего символа 8.

def

6. der(s) = ^ /Иа - множество состояний, достижимых из состояния s.

ж*

7. тй(,у)={а е Аъ | я ——} - множество всех действий, включая 8, определённых в состоянии я.

В этой работе мы рассматриваем только связные полуавтоматы, то есть такие полуавтоматы Ь = (5,1,О, X, я0) 1, для которых верно Дег(.?0 ) = 5, то есть всякое состояние достижимо из начального.

Утверждение 1. Введённые операторы обладают следующими свойствами:

1.1. Для всех состояний я полуавтомата верно ои!;(.?) Ф 0 .

1.2. Если для некоторого состояния я полуавтомата и некоторой последова-

* / тельности а е А выполняется $^ , то [^]п = 0 .

1.3. 0^(0) = 0 .

1.4. [0]а = 0 для любого а е Л5.

Общие свойства двух полуавтоматов удобно характеризовать с помощью пересечения [3]:

Определение 3. Пусть Ь1 = {Б1,1,0, Х1, я01 >ь и Ь2 = {Б2,1,0, Х2, ^02) 1 - два (детерминированных) входо-выходных полуавтомата. Пересечением полуавтоматов Ь1 и Ь2 назовём полуавтомат Ц_ п Ь2 = {Б, I, О, X, (я01, ^02»1, где 5 с 5 х 52 - минимальное множество, полученное с использованием следующего правила для X:

5---—5,' А 5 ----— 5 . „ ,

—----------й , ГДе 5, ^ 52 , 52 € ^ .

Согласно [3], пересечение обладает следующими свойствами:

Утверждение 2. Пусть Ь1 п Ь2 = {Б, I, О, X, {я01, ^02»1 - пересечение заданных полуавтоматов Ь1 = {Б1,1,0, Х1, я01 > 1 и Ь2 = {Б2,1,0, Х2, ^02)ь. Тогда справедливо следующее:

2.1. ,^2» = ) п тй(,у2), где ^ е 51, ^2 е Б2 и ,.?2> е 5 .

2.2. я - 1гасея((я1, я2)) = я -1гасея(я1) п я - 1гасея(я2).

2.3. Xи ^X^ тогда и только тогда, когда <^>Х< , ^> , где Я, я е 5, *?2, х2 е 52 и О € Ад .

2.4. Ь1 п Ь2 - связный автомат.

Определение 4. Пусть Ь = (5,1,0, X, я0)ь. Состояние я е 5 называется полностью определённым по входам или просто полностью определённым, если в нём и во всех состояниях, достижимых из него, определены переходы по всем входным символам. Если начальное состояние полуавтомата Ь полностью определено, то сам полуавтомат назовём полностью определённым.

Определение 5. Пусть Ц = {,1,0, Хх, %) ь и Ь2 = (Б2,1,0, X2, ^02 > ь. Полуавтомат ¿1 находится в отношении шсо с Ь2 (обозначение Ь шсо Ь2) тогда и только тогда, когда Ь1 - полностью определённый полуавтомат и для всякой последовательности ст из я - (гасея(я02) справедливо оиОДх^]п) с оиЩ^ ]п).

Утверждение 3. Пусть Ц = (51,1,0, Х1, я01) 1 и Ь2 = {Б2,1,0, Х2, ^02 > 1 - два за-даных детерминированных связных полуавтомата, причём Ь1 - полностью опре-

делённый полуавтомат, и пусть L1 n L2 = (S, I, O, X, {s01, s02 » L. Тогда Lj ioco L2, если и только если для всякого состояния (s, s2 ) е S перечечения Ll n L2 справедливо out({sj, s2 >) = out(sj ), где sj e Sj, а s2 e S2.

Доказательство. Необходимость. Пусть Lj ioco L2.

Рассмотрим в пересечении полуавтоматов состояние {sj, s2 >, достижимое из начального состояния {s0j, s02 > по последовательности ст . Из свойства пересечения 2.2 следует, что s0last и s02as2, то есть aes -traces( s0j ) и aes -traces( s02 ), а так как L1 и L2 - детерминированные полуавтоматы, то [s01 ]п = (sj} и [s02 ]п ={s2}. По определению ioco имеем out([s0j ]п) ç out([s02 ]п ),

то есть out(sj ) n out(s2 ) = out(sj ), а из свойства 2.2 следует, что, out((sj, s2 » = out(sj ) n out(s2 ). Отсюда out({sj, s2 >) = out(sj ).

Достаточность. Пусть для всякого состояния (s, s2 ) e S пересечения Ll n L2 верно out({sj, s2 >) = out(sj ). Рассмотрим произвольную последовательность

V

aes-traces( s02 ). Если s01 ^ , то тривиально out([s0j ]n ) ç out([s02 ]п ). Пусть

s01 ^ и пусть (помним, что Ll и L2 - детерменированные полуавтоматы) [SoiL = {Si} и [s02]п = (s2}. Тогда, согласно свойству 2.2, [<s01,s02>]п = {<s,s2>}. Из свойства пересечения 2.2 следует, что out(( s, s2 » = out(s ) n out(s2 ), откуда, ввиду условия теоремы, вытекает, что out(sj ) = out(sj ) n out(s2 ). Последнее означает, что OUt(Sj ) ç out(s2 ).

Таким образом, для произвольной последовательности ae s -traces(s02 ) справедливо out([s0j]п ) ç out([s02 ]n).

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 и всех выходных действий о мы пишем t ——^ t', если и только если {t, i, o, t'> e p. ; t ——^ , если и только если существует такое состояние t' e T , что t ——^ t' ; и t, если и только если для всех t ' e T не выполняется t ——^ t'. Отношение p расширяется на входо-выходные последовательности следующим образом: T х (I х O)* х T - наименьшее множество, удовлетворяющее следующим правилам:

t ^ t'A t ' ,7° > t ''

Б ’ Пл / О

г^г ,? ^ ,?' '

Здесь, так же как и ранее, е обозначает пустую входо-выходную последователь-п п

ность. Будем писать г^г' тогда и только тогда, когда (г,п,г') е^ , I^ - тогда и

только тогда, когда существует такое г' е Т , что (г, п, г') е^ , и г- тогда и только тогда, когда для всех г ' е Т выполняется (г, ц,г') , где п е (Iх О)*.

Аналогично полуавтоматам введём следующие операторы и функции (здесь г е Т, Т 'с Т , г е I пе (I хО)*):

def П ¿еГ

1. = {*'е Т | /^/'} . Соответственно для Т - [Т']п = Мп .

^ аег.

2. out(t, г) ={o е O | г —}. Для T' - out(Tг) = ^tTr,out(t, г).

def def

3. in(t) ={i e I | 3o e O : t ——^-}. Для T' - in(T') = ^ ^in(t).

def n

4. Tr(t)=(ne(I xO)’ | t .

5. der(0 = UпЕ(/х0)*[^]П .

def

6. init(t)={(/, o) e I x O 11 ——^-} .

В этой работе мы рассматриваем только связные автоматы, то есть такие автоматы F = {T, I, O, р, t0)F , для которых верно der(t0) = T, то есть всякое состояние достижимо из начального.

Определение 7. Автомат F = {T, I, O, р, t0 )F назовём полностью определённым, если в каждом состоянии t e T определен переход по каждому входному символу i e I, то есть найдутся такие o e O и t' e T , что t ——^ t'.

Определение 8. Пусть заданы автоматы F = {Тг, I, O, р1, t01 > F и

F2 = {T2,1,0, p2, t02)F . Пересечением автоматов Fl и F2 назовём автомат F n F2 = {T, I, O, p, {t01, t02»F , где T ç T x T2 - минимальное множество, полученное с использованием следующего правила для р :

t —— t! A t2 —— Û , „ , „

-----------^----------, где t, t, e T t2, t2 e T2.

(t,, t2 >——Mi t2 > 12 2

Утверждение 4. Пусть F = <T}, I, O, Pi, toi > f , F = (T>, 1, O, ^2, to2 ) f и

F П F2 = {T, I, O, X, {t0l,t02»F . Тогда справедливо следующее:

4.1. init((tj, t2 » = init(?j ) n init(t2 ), где tl e T, t2 e T2 и , t2 )e T.

4.2. Tr«?i,?2>) = Tr(ti ) n Tr(t2 ).

n n n

4.3. t1 ^t[ и t2 ^тогда и только тогда, когда {tl, t2t'2), где tx, t/e T,

t2, t2 e T2 и ne ( Ix O)*.

4.4. Пересечение F n F2 - связный автомат.

Определение 9. Пусть ^ = (Т, I, О, р1, /01 >р и ^2 = (Г2,1,О, р2, г02 >^ - наблюдаемые автоматы. Автомат ^ называется квази-редукцией автомата Г2 (обозначение ^1 ^ ^2), если ^ - полностью определённый автомат и для всякой последовательности п из Тт(г02) и для всякого входного символа г из т([г02]п) справедливо оиЩ^ ]л, г) с оиЩ^]л, г) .

Отметим, что данное выше определение расширяет понятие квази-редукции, известное ранее (см., например, [1]), на наблюдаемые автоматы с так называемыми негармонизированными трассами.

Утверждение 5. Пусть ^ = <Т|, I, О, р1,г01 >Р и ^2 = {Т2,1, О, р2,г02>Р - два автомата, ^ - полностью определённый автомат, и пусть

^ п Р2 = {Т, I, О, р, {г01,г02»^ . Тогда, ^ ^ К,, если и только если для любого состояния <г1, г2 > пересечения Р2 и для любого входного действия г е ш(/2) выполняется ои^, /2 >, г) = ои^, г), где ?1 е Т1 , г2 е Т2.

Доказательство. Необходимость. Пусть ^ ^ ^2, то есть для всякой последовательности цеТг (г02) и всякого входного действия г е 1п([/02 ]п) выполняется ои^[/01 ]п, г) с оц1([г02]п, г) . Рассмотрим в пересечении ^ п ^2 состояние (г1, г2),

достижимое из начального состояния (г01, г02) по последовательности п .

п п

Согласно свойству пересечения 4.4, г01 ^ г1 и г02 ^ г2, то есть пеТт (г01) и Пе Тг(г02). Так как ^ и ^2 - наблюдаемые автоматы, то [г01 ]п ={/1} и [?02 ]п = (?2}. Из свойства 4.4 следует, что для всякого г е I, а значит, и для всякого г е т(г2), верно out«í1,/2), г) = out(г1, г) п out(г2, г), а это, совместно с условием теоремы, означает, что для любого г е т(г2) справедливо out((t1,/2),г) = out(г1,г), что, ввиду произвольности выбора состояния {¡х, г2 > е Т, завершает доказательство.

Достаточность. Пусть для всякого состояния {^, ?2 >е Т и любого г е ш(/2) верно out«í1, /2), г) = out(t1, г). Рассмотрим произвольную последовательность

П е Тг(г02). Если г01 /=>, то, поскольку пустое множество - подмножество любого множества, для всякого г е ш([г02]п ) верно ои1([г01 ]п, г) с ои1([г02]п, г) . Пусть

п

г01 ^ и пусть (помним, что ^ и ^2 - наблюдаемые автоматы) [г01 ]п = (г1} и [г02 ]п = {г2}. Тогда, согласно свойству 4.4, [{г01, г02 )]п = {{^, г2 >}. Из свойства 4.4 пересечения следует, что для всякого г е I, а соответственно и для любого г е т(г2), выполняется ои^^,/2), г) = ои^, г) п ои;(г2, г). Условие теоремы позволяет заключить, что для любого г е т(г2) верно ои^, г) с ои^г2, г). Таким образом, для произвольной последовательности п еТг(г02) и для всякого г е 1п(г2) справедливо ои1([г01 ]п, г) с ои1([г02]п, г).

2. Переход от полуавтомата к автомату

Пусть дан детерминированный связный полуавтомат L = (S, I, O, X, s0 )L. Для него построим автомат F/ = (Г, /Е, OeS , р, t0 >F, где s,., so ^ A - специальные новые входной и выходной символы (здесь и далее для удобства полагаем IB = I и {s,.}, ObS = O и (so, 8} ), а р определяется следующими правилами:

.s —— s' л a е I s ——-s' л a е O 8

a/s , ’ s .la , ’ s ./Ô

t---— t' t ! > t' t ! > t

При этом каждому состоянию автомата F/ соответствует состояние полуавтомата L и наоборот, то есть состояния в полуавтомате, как обычно, будем обозначать буквой s с индексами или без - s, s', sk и так далее, а в автомате буквой t с индексами или без - t, t', tk. Считаем, что состоянию t автомата соответствует состояние s полуавтомата, состоянию t ' - s' и так далее.

Новый входной символ s, определяет ситуацию «ожидания выхода от системы», то есть, когда система достигает момента, что в ней возможен переход под действием пустого входного символа и наблюдатель желает «задействовать» этот переход, то ему необходимо «подождать» выходной реакции системы, не подавая ничего на вход. Новый выходной символ so определяет обратное: система при-нимат входное действие, но наблюдатель не должен ожидать реакции от автомата (на данном переходе). Особо подчеркнём, что по постороению в автомате F/ от-сутсвуют переходы с пометками вида е,./е0, i1/i2, ol/o2, i1/o1, o,/i, , где i1, i2 e I,

o1,02 e .

Процесс построения автомата F/ позволяют говорит о следующих его свойствах:

Утверждение 6. Пусть L = (S, I, O, X, s0 ) L - заданный полуавтомат, а F/ = {T, /Е_, OE s, р, t0 >F - построенный по нему автомат. Тогда справедливы следующие утверждения:

6.1 Если L - полностью определённый по входам полуавтомат, то автомат F/ - полностью определённый автомат.

6.2 Если L - детерменированный полуавтомат, то F/ - наблюдаемый автомат.

6.3 Если L - пересечение некоторых полуавтоматов Ll и L2, то F/ - пересечение автоматов FL и Ff2 (то есть F/1 nL"2 = F/1 n F/2 ).

По построению автомата F/ справедлива следующая лемма. Напомним, что A = I и O и {8}, а операция iH - проекция на множество H.

Лемма 1. Пусть задан полуавтомат L = (S, I, O, X, s0 )L, по которому построен автомат F/ . Тогда Tr(F/ ) 4= s - traces (L) .

Следствие 1. Для любой последовательности ст из s - traces(L) и для любого действия a из As справедливо [L]a —— тогда и только тогда, когда

[FL ]_ ——^ , где A = а ; И° = £î/а, если a е Os, и i/o = a/so, если a e I.

n Ô

Теорема 1. Пусть L = {S1, I, O, Х1, s01 )L и L2 = (S2,1,0, X2, s02 )L - два полуавтомата, причём Ll - полностью определённый полуавтомат. Тогда Lj ioco L2,

если и только если FL ^ .

Доказательство. Утверждения 3 и 5 позволяют доказывать вместо истиности утверждения « L ioco L2, если и только если FL ^ FB2 » истинность утверждения «для произвольного состояния (Sj, s2 )е S пересечения L n L2 выполняется out((Sj, s2 » = out(Sj ), если и только если для произвольного состояния (tj, t2 > е T пересечения nFB2 и для произвольного входного действия i из in(t2) выполняется out((?j, t2>, i) = out(tj, i) », где S - множество состояний полуавтомата

L n L2, а T - множество состояний автомата Ff1 n F/2 .

Необходимость. Пусть для любого состояния (s, s2 )е S верно out((sj, s2>) = out(sj) .

Рассмотрим произвольное состояние (tj, t2 >е T пересечения n FB2, дос-

тижимое из начального по некоторой последовательности п . Свойство 6.6 и следствие 1 из леммы 1 позволяют заключить, что в этом случае в пересечении L n L2 достижимо состояние (sj, s2 > по последовательности а = , причем,

так как L1, L2 и L1 n L2 - детерменированные полуавтоматы, [s01 ]п ={sj}, [S02L ={S2 } , [<S01, S02 >]n ={<S, S2 >} . По условию OUt((Sj, S2 >) = out(Sj ) и,

следовательно, по построению F^, F/2 и F^ n F/2, справедливо out((tj, t2 >, e, ) = out(tj, e, ) или, что то же самое,

init«*!, t2» n

о 0

Напомним, что в автоматах отсутствуют переходы с пометками вида е,./so. Рассмотрим переход, определённый в состоянии t2 автомата F/2 , под действием произвольного входного символов i e in(t2 ) \ {s,}. Поскольку автомат F/1 (свойство 6.6 и условие теоремы) - полностью определённый, то в состоянии tj автомата F1 определён переход под действием входного символа i, причём, согласно правилам построения автоматов F^ и F/2 , в обоих случаях переход будет помечен парой Иг0. Последнее позволяет переписать (*) следующим образом:

init((tj, t2 >) n (in(t2) х °вЪ ) = mit(tj) n (in(t2) х О ),

о о

что в виду произвольности выбора состояния (tj, t2 > завершает доказательство.

Достаточность. Пусть для произвольнго состояния {t1, t2 ) e T и произвольного входного символа i e in(t2 ) выполняется out((tj, t2>, i) = out(tj, i).

Рассмотрим произвольное состояние (sj, s2 > пересечения L n L2, достижимое из начального состояния по последовательности ст = aj... an. Как и в случае дока-

зательства необходимости, это означает, что в автомате f/1 nFb2 достижимо состояние (tj,t2) по последовательности n = ¿'/о--Л¡°п, гДе ijloj = aj/£o, если и только если aj е I, и ijloj = s(/aj, если и только если aj е Os. Ввиду детерминированности полуавтоматов и свойства 6.6, [(s01,s02>]п = {(s1,s2)}, [s01 ]n ={sj}, [S02 L = {s2 } , [<^01 > *02 >]Л = {<*1 ’ *2 >} , [t01 = {t1} и [*02 ]n = {*2 } . ЗаMеTИM, Что автома-

ты FBl, FB2 и FBl n FB2 строятся таким образом, что, каково бы ни было состояние t такого автомата, in(t) э е,, поскольку в порождающем его состоянии полуавтомата s либо определён переход по некоторому выходному символу о е O и соответственно в автомате появляется переход по паре е,/о, либо состояние s устойчивое, а значит, в автомате определён переход, помеченный парой е,/8. Отсюда out(sj) = out(?j, s,) и out(<sj,s2>) = out(<^,t2>, s,), что ввиду условия «для любого i е in(t2 ) верно out((tj, t2 >, i) = out(?j, i)» позволяет заключить, что out(<sj, s2>) = out(sj). Последнее завершает доказательство, так как состояние <sj, s2 > было выбрано произвольно.

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

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

Определение 10. Для заданого детерминированного полуавтомата L = <S, I, O, X, s0 > L через Ls обозначим полуавтомат <S, I, Os, Xs, s0 >L, у которого Xs = Xu{<s,8,s> |S(s)>.

То есть полуавтомат Ls отличается от L добавлением петель с пометкой 8 в устойчивых состояниях. Известно [2], что s - traces(L) = traces(Ls).

Определение 11. Под тестовым примером в теории входо-выходных полуавтоматов будем понимаеть полуавтомат C = (V, I, Os,XC,v0)L, удовлетворяющий следующим требованиям:

1. V э {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, г) = O, где m(v) = {г}.

4. init(pass) = init(fail) = 0 .

Конечное множество тестовых примеров назовём конечным проверяющим тестом.

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

Определение 16. Говорят, что автомат F = {T, I, O, р, s0) F согласуется с тестовым примером C = (V, I, O, , v0) F, если и только если никакая последователь-

ность nе Tr(F) не переводит автомат C в состояние fail, то есть (Tх {fail}) n der(F n C) = 0 .

Определение 17. Моделью неисправности в теории автоматов будем называть тройку (FM, Ef ), где FM - автомат-спецификация (или просто спецификация), Ef - множество полностью определённых автоматов с входным алфавитом

I и выходным алфавитом O, которое называется областью неисправности, причём для всякого автомата F' из Ef выполняется F' ^ FM .

Определение 18. Полный проверяющий тест относительно модели неисправности (FM, Ef ) есть такой (конечный) проверяющий тест T, что спецификация FM согласуется с любым тестовым примером из T, а для всякого F' из Ef в множестве T найдётся такой тестовый пример C, что автомат F' не согласуется с C.

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

В теории входо-выходных полуавтоматов неизвестно как построить (конечный) полный проверяющий тест относительно модели неиспрвности (L, ioco, El ) для случая, когда EL - конечное множество полуавтоматов, однако в теории автоматов известен метод [1] построения полного проверяющего теста относительно модели неисправности (F, Ef ), Ef - множество всех автоматов, число состояний в которых не превышает наперёд заданного числа, или EF - множество всех подавтоматов специального мутационного автомата.

В этом разделе, на основе результатов раздела 3, мы показываем, что если при тестировании системы есть возможность наблюдать молчание и если число состояний в каждом полуавтомате из EL не превышает наперёд заданного числа, то полный проверяющий тест относительно модели неисправности

можно построить на основе полного проверяющего теста для соответствующей автоматной модели неисправности.

Пусть задана модель неисправности ML = {L,ioco,EL), EL = {L1,L2для полуавтоматов, по ней построена автоматная модель неисправности MF = (FeL, Ef ), Ef = [F^, Ff2 ,^} и для модели MF построен полный проверяющий тест TF. Рассмотрим произвольный тестовый пример CF из TF. Со-

S

гласно определению тестового примера, в любом из его состоянии v, таком, что v Ф pass и v Ф fail, будет определён переход под действием всех пар из {г} х OSs, где i е /в. Причём, если i е I (то есть i Ф s(), то для любого о е Оъ имеет место v —fail, так как автомат-спецификация F/ не допускает подобных переходов, ввиду правил построения этого автомата. Более того, переходы этого вида в тесте бессмысленны, поскольку, по правилам построения, в проверяемых автоматах, то есть автоматах из множества EF, принципиально невозможны переходы

вида t —'—^ t’, а следовательно, подобные переходы невозможны и в пересечении этих автоматов с тестовыми примерами, а значит, такие переходы никак не отразятся на вердикте «согласуется/не согласуется». Если же in(v) = {е,.}, то (согласно тем же соображениям) бессмысленным будет переход по паре е,./г0.

Опираясь на приведённые выше рассуждения, можно ввести следующее преобразование тестовых примеров из полного проверяющего теста TF для автоматной

модели неисправности MF = (Fel, EF), EF = {F/1, F/2,...}, построенной по по-луавтоматной модели неисправности ML = {L, ioco, EL), EL = {L1, L2,...}.

Пусть задан автоматный тестовый пример CF = {V, Is, Os, p, v0 >, CF e TF, TF -

s s

полный проверяющий тест относительно модели неисправности MF = {Fel , Ef ), Ef = [F/1, F/2,...}. Построим полуавтомат, V(CF ) = {Q, I, Os, X, q0), пользуясь

s

следующими правилами:

v = pass v = fail in(v) = {z} с I л v —— > v' in(v) = {s(} л v —— > v’л o q = pass’ q = fail’ q —q q —q'

Здесь, как и при преобразовании полуавтомата в автомат, множество состояний Q ничто иное как переименованное множество состояний V . Смысл приведённых правил таков: состояния pass и fail переносятся в полуавтомат без изменения. Если в автомате определён переход под действием входного действия i е I (то есть i Ф в,), то в полуавтомате появляется переход под действием этого символа в состояние, достижимое по паре Hz0, а остальные переходы автоматного тестового примера игнорируются. Если же определён переход по входу е,, то в полуавтомат переносятся все переходы, определяемые символами из Os в соот-ветсвующие состояния, а переход по паре е,/е0 игнорируется.

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

Утверждение 7. Пусть L - заданный полуавтомат, а F/ - построенный по

нему автомат. Тогда, если F/ согласуется с некоторым тестовым примером CF , то L согласуется с V(CF).

Утверждение 8. Пусть L - заданный полуавтомат, а F/ - построенный по нему автомат. Если в пересечении F с некоторым тестовым примером CF достижимо состояние (t,fail), то в пересечении L с V(CF) достижимо состояние (s, fail).

На основании утверждений 7 и 8 можно доказать следующую теорему (здесь, для множества P автоматных тестовых примеров, под V(P) будем понимать множество (V(C) | C е P}):

Теорема 2. Пусть задана полуавтоматная модель неисправности ML = {L,ioco,El), El = (Lj,L2,...} и по ней построена автоматная модель неисправности MF = (F/, Ef ) , Ef = [F^ , F/2,...}. Пусть найден полный проверяющий тест TF относительно модели неисправности MF . Тогда V(TF) - полный проверяющий тест для модели неисправности ML.

ЛИТЕРАТУРА

1. Petrenko A., Yevtushenko N. Conformance tests as checking experiments for partial nondeterministic FSM // Proceedings of the 5th International Workshop on Formal Approaches to Testing of Software in LNCS. 2005. P. 118 - 133.

2. Tretmans J. Test generation with inputs, outputs and repetitive quiescence // Software-Concepts and Tools. 1996. 17(3). P. 103 - 120.

3. Gromov M., Willemse T.A. Model-based testing techniques for diagnosis. Willemse: Testing and Model-Checking Techniques for Diagnosis // Proceedings of the Test Com in LNCS, 2007. P. 138 - 154.

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