Test generation is an important issue when checking functional and nonfunctional requirements for components of distributed systems and formal models are utilized in order to derive test suites with guaranteed fault coverage, i.e., test suites which detect critical component faults. Finite transition systems are often used as such formal models and there are a number of methods for deriving complete test suites for Finite State Machines (FSMs) where each input is followed by an output. However, the FSM model is not always appropriate, as sequences of inputs can be applied before obtaining any output response or a sequence of output responses from a system under test, while this situation can be adequately handled using Input/Output (I/O) automata. When critical faults are enumerated, a test suite can be derived as a set of sequences distinguishing the specification I/O automaton from each considered mutant, and thus, techniques for deriving sequences which distinguish two I/O automata have to be elaborated. There are different notions of distinguishability and in this paper, we consider a so-called (adaptive) separability relation. If two automata which possibly have the nondeterministic behavior are (adaptively) separable then they can be distinguished by applying a corresponding (adaptive) input sequence only once differently from the quasi-equivalence and quasi-reduction relations where each test case has to be applied appropriate number of times under the so-called “all weather conditions” assumption. In this paper, we introduce the notion of a (adaptive) separating sequence for two I/O automata and propose a technique for deriving such a sequence for I/O automata of a special class where at each state, transitions under only inputs or under only outputs are specified. The length of a separating sequence if it exists is also briefly evaluated.
Deriving test suites with guaranteed fault coverage for various kinds of reactive
discrete and hybrid control systems is not possible without the use of formal models [
The rest of the paper is structured as follows. Section 2 contains the preliminaries. In Section 3, the features of I/O automata are discussed for which an (adaptive) separating sequence can be constructed using the well known FSM based methods; the length of such sequences is briefly evaluated when they exist. The conclusion presents some avenues for the future work. 2
The section has the necessary definitions for trace models and the notion of a
separating sequence for I/O automata is introduced. In this paper, a finite I/O automaton,
automaton for short, is a 4-tuple S = (S, s0, I, O, hS) where S is a finite nonempty set
of states with the designated initial state s0, I is a finite nonempty set of input actions
while O is a finite nonempty set of output actions, I O = , and hS S (I O })
S is a transition relation. There is a transition from state s to state s under action а if
and only if the triple (s, а, s) hS. The automaton is deterministic if at each state,
there is at most one transition under each action. An automaton can be considered as a
trace model where a trace is a sequence of actions of the alphabet I O permissible at
the initial state. When testing, only finite traces can be observed and correspondingly,
we assume that the automaton has no cycles labeled only with output actions.
Moreover, in order to avoid races at the automaton states, we consider automata where at
each state either only inputs or only outputs are specified. In other words, in this
paper, an I/O automaton is a deterministic automaton S = (S, s0, I, O, hS), where S is
partitioned into three pairwise disjoint sets S1, S2 and S3: at states of S1 only transitions
under input actions are defined (and there exists at least one such transition), at states
of S2 only transitions under output actions are defined (and there exists at least one
such transition). At states of the set S3 there are no defined outgoing transitions, i.e.,
these states are deadlock states. In general, any of these sets can be empty. A trace at
the initial state is complete if the trace takes the automaton to a state where no outputs
are defined. In order to be able to observe such traces a proper “silent output” I
O (quiescence) is added to the automaton [
If the initial state of the automaton is in the set S1, the input i I is strictly defined at the initial state if there is a defined transition at the initial state under this input. If the initial state of the automaton is in the set S2, the input i I is strictly defined at the initial state if there is a defined transition under this input at each state reachable from the initial state under a trace where actions are labeled with outputs of O. A sequence i of inputs is strictly defined if is strictly defined at the initial state and at each state that is reachable from the initial state via a complete trace with the projection , a transition under input i is defined. 3
Given I/O automata S = (S, s0, I, O, hS) and P = (P, p0, I, O, hP) of the considered set, S и P are called nonseparable if for each input sequence that is strictly defined at the initial states of S и P , the sets of output projections of complete traces with the input projection of S и P are not disjoint. Otherwise, the automata are separable and an input sequence that is strictly defined at the initial states of S и P such that the sets of output projections of complete traces with the input projection of S и P do not intersect is a separating sequence for the automata.
When distinguishing a faulty implementation P from the specification S , if S и P
are separable then after applying a separating input sequence to an automaton under
experiment and observing a corresponding output response we could uniquely
conclude which automaton is under experiment when the hypothesis of applying input
sequences holds [
Finite State machine or simply an FSM is a 5-tuple S = S, X, Y, hS, s0 where S is a finite nonempty set of states with the designated initial state s0, X and Y are finite nonempty alphabets, X Y = , and hS S X Y S is a transition relation. There is a transition from state s S to state s S for an input/output pair x/y (xy) if and only if (s, x, y, s) hS. FSM S is observable, if for each two transitions (s, x, y, s), (s, x, y, s) hS it holds that s = s. If FSM S is observable, x X and y Y, then state s is called the xy-successor of state s, if (s, x, y, s) hS. The set of all non-empty xy-successors of state s for all outputs y is the x-successor of state s. The notions of xy- and x-successors can be defined for a pair of different states s1 and s2, if an input x is a specified input at each of these states. In this case, the xy-successor is defined as a pair of xy-successors of these states. If xy-successors of these states coincide or the xysuccessor exists only for one state of s1 и s2 then the xy-successor of the pair {s1, s2} is a corresponding singleton. The set of all non-empty xy-successors of the pair {s1, s2} is the x-successor of this state pair.
In usual way, the transition relation is extended to input and output sequences. By
default, for each state s S the 4-tuple (s, , , s) is in the transition relation of S
where is the empty sequence. The extended transition relation is denoted by the
same symbol hS. A sequence of input/output pairs which can be successively traversed
starting from the initial state, is called an input/output sequence or a trace of the FSM
(at the initial state). An input x is a defined input at state s if (s, x, y, s) hS for some
y and s. Input sequence х is a defined input sequence for the FSM if is a defined
input sequence at the initial state, and input х is defined at each state that is reachable
from the initial state by a trace with the input projection . Two FSMs over the same
input and output alphabets are separable, if there exists an input sequence defined
for each FSM such that the sets of traces with this input projection are disjoint.
Otherwise, the FSMs are non-separable. There are techniques how the separability
relation can be checked for complete and partial, for observable and non-observable
FSMs and these techniques can be used when checking whether two I/O automata are
separable. Given an automaton S of the considered class, we construct possibly a
nondeterministic FSM using a technique of the paper [
Input: a deterministic I/O automata S = (S, s0, I, O, hS), where S is the union of three pairwise disjoint sets S1, S2 и S3.
Construct FSM MS = (S1 S3, I {null_in}, O O2 … Ons {}, TMS), null_in I, with the empty transition set, i.e. TMS = , where ns is the maximum length of a trace labeled only with outputs in S:
- for each state s S1 such that (s, i, s) TS, s S1 S3, add to TMS the transition (s, i, , s);
- for each state s S1, such that (s, i, s) TS, s S2, add to TMS the transition (s, i, o1 o2. . . ok, s), k ns, where s S1 S3 is the o1 o2. . . ok-successor of state s.
If the initial state of the automaton S is in S2, then add to TMS the transition (s0, null_in, o1 o2. . . ok, s), where s S1 S3 s S1, and s is the non-empty o1 o2. . . oksuccessor of state s0. If the initial state of the automaton S is in S3, then the FSM transition set TMS is empty, and thus, the set of FSM traces has only the empty sequence .
By constructing the FSM MS, the following statements hold.
Proposition 1. Given a deterministic I/O automaton S of the considered class, if the initial state is in the set S1, then an input sequence is strictly defined in S, if and only if is a defined input sequence of the FSM MS. If the initial state of S is in the set S2, then an input sequence is strictly defined in S if and only if the sequence null_in is a defined input sequence of the FSM MS.
Proposition 2. Given a deterministic I/O automaton S of the considered class, if at the initial state of the automaton is in the set S1 then the set of traces of S and FSM MS coincide. If at the initial state of the automaton is in the set S2 then for each trace of S there is the trace null_in in MS, and vice versa.
Given two automata S and P of the considered class, corresponding FSMs MS and MР can be derived. As a corollary to Propositions 1 and 2, the following statement holds.
Theorem 3. Automata S and P are separable if and only if FSMs MS и MР are separable. Moreover, if the initial states of S and P are states of S1 and P1, then a sequence is a separating sequence for S and P if and only is a separating sequence for MS and MР. If the initial states of MS and MР are states of S2 and P2 then a sequence is a separating sequence of S and P, if and only null_in is a separating sequence for MS and MР. If the initial states of MS and MР are states of S1 and P2, or S2 and P1, then the empty sequence is a separating sequence for automata S и P.
When deriving a separating sequence for FSMs MS и MР we use a technique of the
paper [
Algorithm 2 for deriving a separating sequence for two observable possibly partial FSMs
Input: two observable possibly partial FSMs MS и MР over input alphabet X Output: A separating sequence for MS и MР, if FSMs are separable, or the message «The FSMs are non-separable»
Step 1. Drive the intersection of MS and MР. If the intersection is complete then Return the message «The FSMs are non-separable».
Step 2. If the intersection of MS и MР is partial then derive a truncated successor tree for the initial state of the intersection. The root is labeled by the pair of the initial states; other nodes are labeled by subsets of states of the intersection. Let j levels of the tree, j 0, are already constructed and an intermediate (non-terminal) node of the jth level is labeled by a subset P of states of the intersection. There exists an outgoing edge from the node labeled with an input x to the node labeled with the set of xsuccessors of states of P if x is defined at each state of each pair of P. A current node Current at the pth level, p 0, labeled by the set P is a leaf if and only if one of the below conditions holds.
There exists an input x such that for each state (s, p) of P, x is a defined input at both states s and p and the non-empty x-successors are singletons.
There exists a node at the jth level, j < p, labeled with the set R such that P contains each pair of different states of the set R.
separable. Return the message «The FSMs are non-separable».
If there exists a leaf obtained by applying Rule 1, i.e. there exists an input x such that for each state (s, p) of P, x is defined at both states s and p and the non-empty successors of (s, p) are singletons, then the input sequence x is a separating sequence for FSMs MS and MР where sequence labels the path to this leaf. Return the sequence x.
Notice that if a truncated successor tree is completely derived or a width tree search is used when using Algorithm 2 then for separable FSMs MS and MР a shortest separating sequence can be derived.
Therefore, the following technique for checking whether two automata are separable can be proposed.
Algorithm 3 for checking whether two automata are separable and deriving a separating sequence when they are separable
Output: A separating sequence or the message «The automata S and P are nonseparable»
Step 1. If the initial state of S (Р) is in the set S1 S3 (Р1 Р3), while the initial state of Р (S) is in S2 (Р2), then the empty sequence separates automata S and P. If the initial state of S (Р) is in S3 (Р3), while the initial state of Р (S) is in S1 (Р1), then Return he message «The automata are non-separable»
Step 2. Let the initial states of S and P be in the sets S1 S3 and Р1 Р3 or S2 and Р2. Call Algorithm 1 to derive FSMs MS and MP.
Step 3. Call Algorithm 2 to check if there exists a separating sequence for FSMs MS and MP. If FSMs MS and MP are not separable then Return he message «The automata are non-separable».
If there exists a separating sequence for FSMs MS и MР then Return , if is headed by an input of alphabet X. If = null_in , then Return .
Evaluating the length of a separating sequence. For complete observable FSMs the
tight lower bound on the length of a shortest separating sequence with respect to the
number of FSMs’ states is known [
If automata S и Р have the above features but can be nondeterministic then the
corresponding FSMs MS и MР can be non-observable. In the paper [
Another interesting question is related to the adaptive separability
(distinguishability). An adaptive separating sequence is represented by a so-called test case that is an
acyclic FSM and there are techniques how such test cases can be derived [
In this paper, we study the (adaptive) distinguishability relation for Input/Output automata of a special class which often are used as specifications for complex control systems. When deriving tests some mutations are injected into the specification and when testing, such mutations have to be detected. When each pair “specification, mutant” has an (adaptive) separating sequence there is no need for assuming the all weather conditions and thus, each test case is applied only once. On the other hand, this affects the length of a separating sequence and in the future, we plan to study other distinguishability relations for I/O automata of the considered class as well as the extensions of this class.