ПРОГРАММИРОВАНИЕ, 2012, No 3, с. 36-44
ТЕСТИРОВАНИЕ, ВЕРИФИКАЦИЯ И ВАЛИДАЦИЯ ПРОГРАММ
УДК 519.713.1; 519.718.7
К ПОСТРОЕНИЮ ПРОВЕРЯЮЩИХ ТЕСТОВ ДЛЯ НЕДЕТЕРМИНИРОВАННЫХ АВТОМАТОВ С ТАЙМ-АУТАМИ
© 2012 г. Н.В. Шабалдина, Р.Ф. Галимуллин
ГТЛ "1 е^
Томский государственный университет 634050 г. Томск, пр-т,. Ленина, 36 E-mail: NataliaMailBox@mail.ru, nihilkhaos@gmail.com Поступила в редакцию 01.11.2011 г.
В статье исследуется отношение неразделимости для недетерминированных автоматов с тайм-аутами. Особенностью таких автоматов являются целочисленные задержки, или тайм-ауты, определяющие, как долго автомат будет находиться в том или ином состоянии при отсутствии входных воздействий. Если тайм-аут заканчивается, и на автомат не было подано ни одного входного символа, то состояние автомата изменяется согласно переходу по временной задержке. В статье излагается алгоритм построения разделяющей последовательности для таких автоматов, т.е. такой временной входной последовательности, для которой множества выходных последовательностей автоматов не пересекаются, и соответственно достаточно подать разделяющую последовательность на эти автоматы один раз, чтобы по выходной реакции различить их. На основе этого алгоритма предлагается алгоритм построения проверяющих тестов относительно неразделимости для случая, когда область неисправности задается при помощи мутационного автомата. Обсуждается построение тестов относительно неразделимости путем перехода к классическим конечным автоматам.
1. ВВЕДЕНИЕ
В статье рассматривается одна из модификаций классической модели конечного автомата [1], а именно, модель с тайм-аутами [2-4], которую в рамках данной работы мы будем также называть временным автоматом. В этой модели, как и в модели конечного автомата, есть конечные множества состояний, входных и выходных символов; переходы из состояния в состояние могут осуществляться при подаче входного символа и сопровождаются выдачей выходного символа, и, кроме того, возможны переходы по временным задержкам (тайм-аутам), т.е. по прошествии некоторого времени, если в течение этого времени на автомат не поступил ни один входной символ. Наличие переходов по тайм-аутам позволяет более полно описать поведение многих современных технических систем. В качестве примера можно привести сотовый телефон, у которого по
истечению некоторого времени гаснет экран, тр3-плеер и другие системы.
Для временных автоматов только начаты исследования различных отношений конформности [3]. Эти отношения и их свойства во многом заимствуются из теории конечных автоматов. Отношение неразделимости [5-7], исследуемое в данной статье, также было введено изначально для конечных автоматов, а именно, для автоматов с недетерминированным поведением. Данное отношение замечательно тем, что при тестировании не требуется выполнения "всех погодных условий", т.е. необходимости подавать каждую тестовую последовательность до тех пор и при таких условиях, чтобы пронаблюдать все выходные последовательности системы на поданную входную последовательность. На практике затруднительно обеспечить выполнение такого предположения, и поэтому построение тестов с использованием отношения неразделимости
актуально для моделей недетерминированных конечных автоматов [5-7] и их модификаций [3, 4]. В данной работе предлагается алгоритм построения разделяющей последовательности для временных автоматов с тайм-аутами, а также предлагается алгоритм построения исчерпывающего проверяющего теста относительно неразделимости при задании области неисправностей при помощи мутационного автомата. Обсуждается возможность построения разделяющей последовательности и теста относительно неразделимости путем перехода к классическим автоматам.
2. ОСНОВНЫЕ ОПРЕДЕЛЕНИЯ И ОБОЗНАЧЕНИЯ
В данной работе временным автоматом (автоматом с тайм-аутами) называется шестерка А = (5,/, О, «о, Аа, Да), где 5 -конечное непустое множество состояний с выделенным начальным состоянием «о, / и О -конечные непересекающиеся входной и выходной алфавиты, Аа Q 5 х / х О х 5 - отношение переходов. Функция Да : 5 ^ 5 х (Ж и {то}), где N множество натуральных чисел, есть функция задержки, определяющая для каждого состояния тайм-аут, т.е. время ожидания входного символа без изменения состояния, причём если для некоторого состояния « имеет место Да(«) = (в', то), то в = в'. Таким образом, классический конечный автомат [1], в том числе недетерминированный [5, 6], можно рассматривать как временной автомат, в котором для всех состояний в € 5 имеет место Да(«) = (в, то), т.е. конечный автомат, в отличии от временного, сколь угодно долго ожидает входного символа, не изменяя при этом текущее состояние.
Временному автомату ставится в соответствие внутренняя переменная (часы), принимающая целые неотрицательные значения и указывающая время, прошедшее с момента достижения текущего состояния [2-4] (или с момента выдачи последнего выходного символа). Если (в, г, в', о) € Аа, то автомат А в состоянии 8 на входной символ г может выдать выходной символ о и изменить своё состояние на в', причем после этого соответствующая
временная переменная принимает значение 0. В данной работе мы не рассматриваем задержки выходных символов, т.е. полагаем, что временной автомат выдаёт выходной символ в тот же самый момент, когда принимает входной символ, и возможно, меняет своё состояние.
Если для каждой пары (в, г) € 5 х / существует не более одной пары (о, в') € О х 5 такой, что (в, г, о, в') € Аа, то временной автомат А называется детерминированным; иначе временной автомат называется недетерминированным. Если для каждой пары (в, г) € 5 х / существует, по крайней мере, одна пара (о, в') € О х 5 такая, что (в, г, о, в') € Аа, то 5 называется полностью определенным. Временной автомат А называется наблюдаемым, если для любой тройки (в, г, о) € 5 х / х О существует не более одного состояния, такого, что (в, г, о, в') € Аа.
Временной входной символ есть пара (г,Ь) € / х где Z + - множество целых неотрицательных чисел; временной входной символ (г, ¿) показывает, что входной символ г подается в момент, когда значение временной переменной равно ¿. Последовательность (¿1, й)(&2, ¿2 ... (гг, ¿г) временных входных символов называется временной входной последовательностью длины I.
Для того чтобы расширить отношение переходов временного автомата на временные входные символы, введем специальную функцию ЫтвА : 5 х Z+ ^ 5, позволяющую определить по текущему состоянию автомата состояние автомата в момент времени, когда значение временной переменной равно Ь [4]. Для определения значения функции Ьгтва(в,Ь) рассмотрим последовательность тайм-аутов
Да (в) = (в1,Т1), А(в1) = (в2, Т 2),..., Да(«р_1) = (вр,Тр)
такую, что Т1 + Т2 + ■ ■ ■ + Тр-11еЬ, но Т1 + Т2 + ••• + Тр > Ь. В этом случае Ьгтеа(«,Ь) = «р-1. Если Да (в) = (в, то), то Ьгтеа(«,Ь) = в для каждого значения переменной ¿. Для каждого временного входного символа (г,Ь) к отношению А добавляется переход (в, (г,Ь,)«', о), если и только если (Ьгтеа(в,¿), г,«', о) € Аа.
Множество всех входных временных последовательностей обозначается I.f. Для полностью определенного временного автомата A функция outs, отображающая множество S х If во множество выходных последовательностей, т.е. outA(s,) : S х If ^ O*, вводится следующим образом. Для состояния s и временной входной последовательности а = (ii,ti)... {k,ti) последовательность oi .. .oi G outs (s, а), если существуют состояния s1 = s, ...,si+i, такие, что для каждого j G {1,...,1} временной автомат A имеет временной переход (sj, (ij,tj),oj,sj+i), и будем говорить в этом случае, что пара (а, outA(s, а)) может перевести автомат A из состояния s в состояние si+i. Пара "временная_входная_по-следовательность_ а/выходная _последователь-ность_в" называется временной входо-выходной последовательностью временного автомата A в состоянии s, если в G outA^,а). Множество всех временных входо-выходных последовательностей в начальном состоянии автомата A обозначим TTta.
Состояние s' называется (i,t)/о преемником состояния s, если (s, (i,t),s',o) G \a. Состояние s в этом случае называется (i,t)/о предшественником состояния s'. Соответственно любой (i,t)/о преемник состояния s((i,t)/о предшественник состояния s') можно рассматривать как просто (i, t) преемник состояния s((i, t)предшественник состояния s'). Множество всех (i,t)/о преемников состояния s будем обозначать suca(s, (i,t),o), множество всех (i, t)преемников состояния s будем обозначать suca(s, (i,t)), и в обоих случаях для краткости символ (i, 0) будем заменять символом i.
Если временной автомат A детерминированный, то для каждого состояния s и каждой временной входной последовательности а множество outA(s, а) содержит не более одного элемента. Для полностью определенного временного автомата A множество outA(s^) не является пустым для любых s G S, а G Itf .
Пусть A = (S,I,O,so,Xa, Aa) и B = (P, I,O,po, Xb, Ab) - полностью определенные автоматы с тайм-аутами. Автомат B называется редукцией автомата A, если TTtb ^ TTta] если TTtb £ TTta, то автомат B не является редукцией автомата A. Временные автоматы A
и В называются неразделимыми, если выходные реакции автоматов на любую временную входную последовательность а пересекаются, т.е. оЫА(в0,а) П оЫв(р0,а) = 0; в противном случае автоматы называются разделимыми. Временная входная последовательность а, такая, что оЫА(в0,а) П оЫв(ро,а) = 0 называется разделяющей последовательностью для временных автоматов А и В.
Пересечением А П В называется наибольший связный подавтомат С = ((^,1,0, до, Ас, Ас) автомата (К,1,О,д0,Ас, Ас), в котором К = Б х К х Р х К, где К = {0,...,к}, к = шги(шахАА(в), тахАв(р)), начальное состояние есть четверка («о, 0,ро, 0), и отношение переходов Ас и функция Ас определены по следующим правилам [3]:
1. Отношение переходов Ас содержит четверку [(в, кг,р, к2),г, о, (в, 0,р, 0)], если и только если (в, г, о, в) с Аа и (р,г,о,р') е Ав.
2. Ас((в,кг,р,к2)) = [(в',к[,р',к'2),к], где к = тги(АА(в)^м — кг, Ав(р)±м — к2). Состояние (в', к',,р',к2) = (АА(в)^, 0, Ав(р)ц>, 0), если (Аа(«)^м
Для дальнейшего прочтения статьи необходимо приобрести полный текст. Статьи высылаются в формате PDF на указанную при оплате почту. Время доставки составляет менее 10 минут. Стоимость одной статьи — 150 рублей.