Аннотация. В статье рассматривается задача синтеза тестов с гарантированной полнотой для синхронной композиции конечных автоматов. Конечные автоматы и их композиции широко используются при синтезе тестов для различных систем, включая сервисные системы, и операция синхронной композиции описывает поведение многомодульных систем при одновременной работе всех каналов композиции. Без ограничения общности мы делаем предположение о том, что выходной порт любой компоненты может быть соединен не более чем с одним входным портом другой компоненты, и предлагаем упрощенный способ построения синхронной композиции полностью определенных детерминированных автоматов, используя хорошо известные операции над автоматами. Мы также расширяем известные условия для проверки замкнутости операции синхронной композиции в множестве полностью определенных детерминированных автоматов, показывая, что для замкнутости операции достаточно, чтобы каждый цикл в композиции содержал Муровскую пару, т.е. пару <входной порт, выходной порт> некоторой компоненты, для которой значения в выходном порту не зависят от значений в соответствующем входном порту (Муровское условие в композиции). Если в проверяемых системах структура композиции не меняется, и ошибки в компонентах не нарушают Муровское условие, то обход графа переходов автомата, построенного по эталонной композиции, является достаточно качественным тестом, при условии наблюдения состояний компонент (тестирование с открытым состоянием). Мы также предлагаем способ построения теста с гарантированной полнотой для выбранной компоненты при тестировании с закрытым состоянием, т.е. когда нет возможности наблюдать состояния компонент, при условии, что входные и выходные порты тестируемой компоненты доступны для наблюдения.
Ключевые слова: проверяющий тест конечный автомат, синхронная
композиция, Deriving tests for the synchronous composition of deterministic complete Finite State Machines I.B. Burdonov, N.V. Evtushenko, A.S. Kossatchev
Ivannikov Institute for System Programming
of the Russian Academy of Sciences
Abstract. The paper is devoted to deriving tests with guaranteed fault coverage
for Finite State Machines (FSM). FSMs and their compositions are widely used when
deriving tests for various systems, including interactive services, and the synchronous
composition describes the behavior of a multi modular system when all the channels
are active at each time instance. Without loss of generality, we assume that an output
port of each FSM component is connected with at most one input port of another
FSM component and propose a simplified approach for deriving the synchronous
composition of deterministic complete FSMs using well known operators over FSMs.
We also extend the sufficient conditions for checking the closure of the synchronous
composition operator with respect to deterministic complete FSMs showing that for
the operator closure it is sufficient that each composition cycle contains a Moore pair,
i.e., a pair <input port, output port> of some component FSM such that outputs do not
significantly depend on inputs (Moore condition). If a system under test has the same
structure as the reference composition and faults of component FSMs do not break
the Moore condition, then a transition tour of the composed FSM is a good quality
test when component states can be observed (testing with open state). We also
propose how to derive a test with guaranteed fault coverage for a component FSM of
our interest when states cannot be observed under the condition that input and output
ports of a component under test can still be observed.
1. Введение
Автоматизация синтеза тестов с гарантированной полнотой для различных
сложных систем, включая сервисные системы, была и остается одной из
актуальных задач, и широко используемыми моделями при синтезе тестов для
таких систем являются так называемые трассовые модели. Одной из таких
моделей является конечный автомат, описывающий поведение тестируемой
системы на входных последовательностях, т.е. отображение
последовательностей действий в одном (входном) алфавите в
последовательности в другом (выходном) алфавите. Несмотря на большое
количество публикаций в области синтеза тестов по конечно-автоматной
модели [см., например, 1], задачи генерации проверяющих тестов с
гарантированной полнотой для композиций конечных автоматов были и
остаются актуальными. В большинстве работ [
Следует отметить, что тесты, построенные для композиции автоматов,
оказываются слишком длинными, и поэтому особый интерес представляет
синтез тестов для проверки наиболее критических компонент композиции.
Однако в этом случае возникает ряд хорошо известных проблем, для которых в
настоящее время отсутствуют масштабируемые решения. Во-первых,
попрежнему, стоит вопрос о том, при каких условиях поведение синхронной
композиции полностью определенных детерминированных автоматов, т.е.
автоматов, которые отображают каждую входную последовательность в
единственную выходную последовательность, и поведение композиции
вычисляется за один такт для каждого входного символа, описывается
автоматом этого же класса; в этом случае достаточно качественные тесты
можно строить непосредственно по автомату композиции. Во-вторых, каким
образом описать поведение компоненты, которое является существенным для
функционирования композиции, т.е. то поведение, которое, вообще говоря,
можно проверить, не «выдергивая» данный компонент из композиции;
известно, что для описания такого поведения можно использовать решение
соответствующего автоматного уравнения [
В настоящей работе мы расширяем известные условия для проверки
замкнутости операции синхронной композиции в множестве полностью
определенных детерминированных автоматов. Показывается, что для того
чтобы это было возможным, каждый цикл в композиции должен содержать
Муровскую пару, т.е. пару <входной порт, выходной порт> некоторой
компоненты, для которой значения в выходном порту не зависят от значений в
соответствующем входном порту (Муровское условие в композиции). Если
далее предположить, что в проверяемых системах структура композиции не
меняется, и ошибки в компонентах не нарушают Муровское условие, то обход
графа переходов автомата, построенного по эталонной композиции, является
достаточно качественным тестом, при условии наблюдения состояний
компонент (тестирование с открытым состоянием [
Статья структурирована следующим образом. Раздел 2 содержит необходимые определения из теории автоматов. В разделе 3 представлен эффективный алгоритм построения автоматной композиции (без перехода к полуавтоматам); здесь же формулируется новое условие замкнутости операции синхронной композиции в множестве полностью определенных детерминированных автоматов. В разделе 4 рассматриваются два случая синтеза тестов: обход графа переходов композиции при тестировании с открытым состоянием и алгоритм построения теста для выбранной (критической) компоненты с заданной полнотой при тестировании с закрытым состоянием.
2. Определения и обозначения Напомним необходимые определения из теории автоматов. Конечные автоматы используются для описания поведения реактивных систем типа «запрос-ответ»: системы переходят из состояния в состояние под воздействием входных символов (воздействий), производя при этом реакции (выходные символы). Конечный автомат, часто называемый просто автоматом, есть пятерка S = 〈S, X, Y, hS, s0〉, где S есть непустое конечное множество состояний с выделенным начальным состоянием s0, X и Y суть непустые конечные входной и выходной алфавиты, и hS ⊆ S × X × Y × S есть отношение переходов. Мы говорим, что существует переход из состояния s ∈ S в состояние s'∈ S по входвыходной паре x/y, если и только если четверка (s, x, y, s') принадлежит отношению переходов hS. Автомат S детерминированный и полностью определенный, если для каждого состояния s ∈ S и каждого входного символа x ∈ X существует в точности одна пара (y, s'), такая что (s, x, y, s') ∈ hS. Детерминированный полностью определенный автомат часто рассматривается как шестерка S = 〈S, X, Y, δ, λ, s0〉, где δ: S × X → S есть функция переходов, и λ: S × X → Y есть функция выходов; для детерминированного полностью определенного автомата (s, x, y, s') ∈ hS, если и только если δ(s, x) = s' и λ(s, x) = y. В данной статье рассматриваются автоматы детерминированные и полностью определенные, если явно не сказано иное. Как обычно, функции переходов и выходов автомата S расширяются на последовательности в алфавитах X и Y. Расширенные функции обозначаются теми же символами. По определению, для каждого s ∈ S четверка (s, ε, ε, s), где ε – пустая последовательность, находится в множестве переходов автомата S.
Рассмотрим автомат, в котором входной и выходной алфавиты являются декартовыми произведениями других алфавитов, X = × Xj (i ∈ I), Y = × Yj (j ∈ J), и каждый алфавит соответствует некотором входному (или выходному) порту, причем множества входных и выходных портов не пересекаются. Пусть С (D) – непустое подмножество входных (выходных) портов автомата S. Автомат S↓C,D = (S, X↓C, Y↓D, hS↓C,D, s0), где X↓C и Y↓D суть соответствующие проекции алфавитов X и Y, есть проекция автомата S на C и D, если отношение hS↓C,D есть соответствующая проекция отношения hS, т.е. в каждой четверке (s, x, y, s′) все символы, не относящиеся к портам множеств C и D, удалены.
Пара <входной_порт_a, выходной_порт_b> называется Муровской парой, если в каждом состоянии s для любых входных векторов (β, xa, γ) и ( β, x′a, γ), которые являются соседними по сигналу на входном порте a, сигналы на выходном порте b совпадают, т.е. имеет место:
(s, (β, xa, γ), (β', yb, γ'), s'), (s, (β, x'a, γ), (β'', y'b, γ''), s'') ∈ hS ⇒ yb = y'b. 3. Синхронная композиция автоматов Рассмотрим систему взаимодействующих автоматов A1, …., An, такую, что множества состояний, входных и выходных портов компонент попарно не пересекаются. Автоматы-компоненты взаимодействуют между собой и с внешней средой, причем выходной порт компоненты может быть соединен только с одним входным портом другой компоненты, и входной порт компоненты может быть соединен только с одним выходным портом другой компоненты. Пара соединённых портов <выходной_порт, входной_порт> называется каналом, и б ез ограничения общности, мы полагаем, что алфавиты портов, соединенных каналом, совпадают. Входные (выходные) порты, не связанные каналом с портами других компонент, называются внешними входными (выходными) портами, и множества θ1 (θ2) внешних входных (выходных) портов не являются пустыми. Внешние порты соединены с внешней средой. Входные воздействия поступают на композицию через внешние входные порты; на внешних выходных портах композиция выдает выходные реакции. Через Γ1 и Γ2, Γ1 ∪ Γ2 = Γ, обозначается множество всех входных и выходных портов компонент.
Известны различные способы построения автомата, описывающего
поведение синхронной композиции автоматов A1, …., An. В одной из первых
работ такая композиция строилась на основе построения дерева преемников [
Алгоритм построения синхронной композиции Вход: система полностью определенных детерминированных взаимодействующих автоматов A1, …., An. Выход: автомат, описывающий поведение композиции на внешних входных и выходных портах. Шаг 1. Отношение переходов каждой компоненты расширяется на все порты, которых нет в компоненте, (Aj)↑Γ, j = 1, …, n, причем значения сигналов, на портах, соединенных каналом, совпадают. Шаг 2. Строится пересечение (A1)↑Γ ∩ … ∩ (An)↑Γ. Шаг 3. Автомат •(A1, …, An), называемый синхронной композицией автоматов A1, …., An, есть проекция автомата (A1)↑Γ ∩ … ∩ (An)↑Γ на множество внешних входных и выходных портов композиции.
Рассмотрим композицию автоматов A and B на рис. 1 с начальными состояниями а и 1. Автомат A имеет входной порт, являющийся внешним входным портом композиции, с алфавитом X = {x1, x2} и внутренний входной порт VA с алфавитом V = {v1, v2}; выходной порт, являющийся внешним выходным портом композиции, с алфавитом Y = {y1, y2} и внутренний выходной порт UA с алфавитом U = {u1, u2}. Автомат B является автоматом Мура и имеет входной порт UB с алфавитом U и выходной порт VB с алфавитом V. Порты VA и VB (UA и UB) соединены каналами. Таким образом, Γ1 = {X, VA, UB} и Γ2 = {UA, Y, VB}, Γ1 ∪ Γ2 = Γ, θ1 = {X} и θ2 = {Y}.
x1v2/u2y2 x2v2/u2y2 a x1v1/u1y1 x2v1/u1y1 x1v1/u2y1 x1v2/u2y1 x2v1/u1y1 x2v2/u1y2 b u2/v1 На рис. 2 представлено расширение автоматов A и B на все входные и выходные порты. Входными символами являются значения сигналов на входных портах X, VA и UB; выходными символами – значения на выходных портах UA, Y и VB. Соответствующее пересечение расширенных автоматов показано на рис. 3. x1v2u2/u2y2v2 x2v2u2/u2y2v2
a x1v1u2/u2y1v1 b1 a1 x2/y2 x2/y1 x1/y1 x2/y1 b2 Рис 2. Расширенные автоматы A и B Рис. 3. Автомат-пересечение (A)↑Γ и (B)↑Γ Рис. 4. Синхронная композиция A•B Далее строится XY-проекция, которая описывает поведение композиции на внешних входном и выходном портах (рис. 4).
Рассмотрим синхронную композицию полностью определенных детерминированных автоматов A1, …, An. Можно показать, что если в каждом цикле, проходящем через порты автоматов-компонентов есть Муровская пара, то автомат-композиция •(A1, …, An) есть полностью определенный детерминированный автомат. Для доказательства этого утверждения можно построить граф зависимостей Gdep. Вершинами графа являются порты автоматов-компонент композиции и вершины, соответствующие текущему состоянию sk каждой компоненты Ak, k = 1..n.
Граф содержит следующие дуги.
1) Если пара < выходной_порт, входной_порт > соединена каналом, то существует дуга из выходного порта во входной порт.
2) Если пара < входной_порт, выходной_порт > принадлежит одной компоненте Ak и не является Муровской в Ak, существует дуга из входного порта в выходной порт.
3) Из вершины sk, соответствующей текущему состоянию компоненты Ak, в графе существует дугав каждый выходной порт компоненты Ak.
По определению графа Gdep, никакой цикл в графе не может проходить через вершины, соответствующие текущим состояниям компонент, и поскольку граф Gdep не содержит дуг, соответствующих Муровским парам, то построенный граф является ациклическим, и значение сигнала в каждом выходном порту однозначно определяется значениями сигналов на внешних входных портах и текущими состояниям автоматов-компонентов. Композиция A • B автоматов A и B на рис. 4 есть полностью определенный детерминированный автомат, поскольку B является автоматом Мура. 4. Синтез тестов для синхронной композиции полностью
определенных детерминированных автоматов Мы предполагаем, что в рассматриваемой композиции полностью определенных детерминированных автоматов в каждом цикле, проходящем через порты автоматов-компонентов, есть Муровская пара, следовательно, композиция •(A1, …, An) есть полностью определенный детерминированный автомат.
Тестирование с открытым состоянием. Пусть в тестируемой композиции сохранена структура композиции-спецификации, входные и выходные порты компонент и состояния компонент доступны для наблюдения. Композиция полагается «исправной», если тестируемый автомат равен автоматуспецификации •(A1, …, An). Таким образом, рассматривается модель неисправности (FM) <•(A1, …, An), =, FD>, где область неисправности FD содержит композиции автоматов, в которых сохранена структура композицииспецификации, компоненты имеют те же входные и выходные порты и в тестируемой композиция каждый цикл содержит Муровскую пару. В этом случае тестируемая композиция также является полностью определенным детерминированным автоматом. В этом случае обход графа переходов автомата •(A1, …, An) будет полным проверяющим тестом относительно модели <•(A1, …, An), =, FD>, поскольку будет о бнаруживать любую композицию из области неисправности, не равную композиции-спецификации.
Предположим теперь, что в композиции неисправной может быть только
одна компонента, причем не нарушается Муровское условие, т.е. в композиции
с неисправной компонентой в каждом цикле по-прежнему есть Муровская пара.
В этом случае, обход графа переходов композиции можно отфильтровать, т.к.
достаточно пройти все переходы в автомате-компоненте, т.е. оставить в тесте
такое множество последовательностей, которые пересекают каждый переход в
каждой компоненте [
Тестирование компоненты с закрытым состоянием. Рассмотрим синхронную композицию автоматов A1, …, An и предположим, что неисправной может быть одна компонента Aj. Муровское условие при неисправной компоненте в композиции сохраняется, и для наблюдения доступны все входные и выходные порты компоненты Aj, однако ее состояния недоступны для наблюдения.
Алгоритм построения полного проверяющего теста для компоненты Aj при сформулированных выше условиях включает следующие шаги. Шаг 1. Автомат Spec есть автомат •(A1, …, An), который, в качестве выходных содержит символы, являющиеся входными символами для компоненты Aj.
Шаг 2. Строится последовательная композиция автоматов Spec и Аj, по которой строится частичный детерминированный автомат ЕЕ(Аj), квазиэквивалентный Аj и содержащий для компоненты Аj только входные последовательности, которые могут поступить на компоненту Аj в композиции автоматов A1, …, An.
Шаг 3. Для автомата ЕЕ(Аj) строится полный проверяющий тест TSint относительно заданной модели неисправности в алфавитах компоненты Аj.
Шаг 4. Строится «обратный автомат» для Spec, по которому «вычисляются» внешние входные символы для композиции, обеспечивающие поступление последовательностей теста TS на компоненту Аj, т.е. строится полный проверяющий тест TSext для компоненты Аj во внешнем входном алфавите.
Рассмотрим автомат Spec, о котором говорится на первом шаге. По построению, множество выходных последовательностей автомата Spec совпадает с множеством входных последовательностей компоненты Аj в композиции автоматов A1, …, An (свойство 1).
Поскольку композиция автоматов последовательная, то только выходные
последовательности автомата являются входными последовательностями
компоненты в композиции; соответствующий частичный автомат, поведение
которого определено только на этих входных последовательностях, и который
имеет на них такое же поведение как компонента Аj, т.е. квази-эквивалентен
компоненте Аj, обозначим ЕЕ(Аj) (embedded equivalent of [
Утверждение 1. Полный проверяющий тест относительно модели неисправности <ЕЕ(Аj), =q, FD>, где =q отношение квази-эквивалентности, обнаруживает любую реализацию компоненты Аj из множества FD, такую, что в композиции не нарушается Муровское условие и выходной символ на одном из каналов компоненты Аj не совпадает с эталонным выходным символом композиции на этом канале.
Для трансляции полученного внутреннего теста на внешние входные каналы композиции введем понятие обратного автомата inverse(Spec), в котором меняются местами входной и выходной алфавиты, т.е. для автомата Spec = (Q, X, Y, h, q0), автомат inverse(Spec) = (Q, Y, X, H, q0), где H совпадает с h с точностью до перестановки входных и выходных символов. Соответственно, inverse(Spec) может оказаться недетерминированным автоматом, однако при трансляции внутреннего теста во внешний происходит только вычисление выходных реакций по заданной входной последовательности, т.е. трансляция имеет полиномиальную сложность. Если «стереть» выходные символы в автомате inverse(Spec), то этот соответствующий полуавтомат будет представлять множество входных последовательностей, которые могут поступить на компоненту Аj в композиции.
Утверждение 2. Множество последовательностей, на которых определено поведение автомата inverse(Spec), есть множество входных последовательностей, которые могут поступить на компоненту Аj в композиции.
Если задано некоторое множество входных последовательностей для компоненты P, то по автомату inverse(Spec) можно определить необходимое множество внешних входных последовательностей.
Рассмотрим композицию автоматов A and B на рис. 1. Автомат Spec в качестве выходных символов содержит только символы из алфавита U, получен из пересечения на рис. 3 и приведен на рис. 5.
b1 x1/u2 a1
x1/u2 x2/u1 x2/u1 x1,x2/u1
b2 Рис. 5. Автомат Spec.
Если ошибки не увеличивают число состояний компоненты, то можно построить тест TSint = {u1u1u2u1; u1u2u1}, который можно транслировать во внешний тест с использованием обратного автомата для Spec. Получим TSext = {x1x2x1x1; x1x1x1}. Если возможно наблюдение всех каналов композиции (Uchannels), то этот тест будет полным относительно неисправностей компоненты B, которые не увеличивают число состояний в этой компоненте.
Работа выполнена при поддержке Российского фонда фундаментальных исследований, проекты 16-07-01106-а и 17-07-00682-а, и Российского научного фонда, проект 16-49-03012.