Adaptive test generation from a nondeterministic fsm

Тип работы:

Узнать стоимость новой

Детальная информация о работе

Выдержка из работы

UDC 519. 713. 4
VETROVA M. V., YEVTUSHENKO N. V. ____________
In the paper, we propose a test derivation method from a nondeterministic specification Finite State Machine (FSM). Each Implementation Under Test (IUT) is assumed to be a deterministic FSM over the same input and output alphabets. Moreover, a test suite is adaptive, i.e., the next test case depends on the response of an IUT to the previous test cases.
1. Introduction
The problem of test derivation against a nondeterministic specification Finite State Machine (FSM) is well known [1−3]. In the papers, the authors propose methods that return a test suite with the guaranteed fault coverage. However, the performed experiments [4] clearly show that the length ofa preset complete test suite is huge even for small FSM. The reason is when deriving a preset test suite we count on the worst case of an implementation. In this paper, similar to [3], we discuss how a complete adaptive test suite can be derived from a nondeterministic specification FSM. In adaptive testing the next test case depends on the output responses of an implementation to the previous test cases, i.e., a test suite significantly depends on an implementation at hand. In this paper, each Implementation Under Test (IUT) is assumed to be a deterministic FSM over the same input and output alphabets as the specification FSM. The conformance relation that has to be checked through testing is the reduction relation. An implementation conforms to its specification if the implementation behavior is contained in that of the specification.
The paper is structured as follows. Section 2 comprises preliminaries. In Section 3, we introduce the notion of an adaptive test suite. The method for a complete test suite derivation with an application example is described in Section 4.
2. Definitions
Given alphabet Z, let 2Z denote the set of all subsets of Z. A Finite State Machine A is a 5-tuple (S, s0, I, O, h), where S is a finite set of states with the initial state sq, I and O are finite non-empty sets of inputs and outputs, respectively, which satisfy the condition I n O = 0 — h is a behavior function h: S x I ^ 2SxO. If h (s, a)0 for all (s, a) є S x I then the FSM is complete- otherwise, the FSM is partial. FSM A is deterministic if |h (s, a) & lt- 1 for all (s, a) є S x I, otherwise A is nondeterministic. Given (s, a) є S x I, the set out (s, a) denotes the output projection of the set h (s, a).
FSM A is said to be observable if the underlying automaton Ax = (S, sq, I x 0,5) is deterministic [5]. In the automaton A, 5(s, (a, o)) = s'- iff (so) є h (s, a). In
this paper, we only consider observable machines- one could use a standard procedure for automata determinization to convert a given FS M into observable one.
A word a of the automaton Ax at state s is a trace of A at state s — TrA (s) denotes the set of all traces of A at state s and TrA denotes the set of traces of A at the initial state. Given sequence, а є (I x O)*, the input projection of a, denoted, is a sequence obtained from a by erasing symbols o є O — similarly, the output projection a^O is defined. An input sequence p є I* is a defined input sequence at state s of A if there exists a є TrA (s) such that P = a^. Given a trace P є TrA (s), s — after — p denotes the state reached by A when it executes the trace p at state s. If 5 is the initial state sq then instead of sq — after -p we write A — after — p.
State t of в is said to be a reduction of state s of a, written t & lt- s, if
{p є TrB (t)|Рн = а}є {p є TrA (s)|P^I = a)
for all ає I.
The above relation is also defined for machines, in other words, given FSM B and A, B is a reduction of A, written в & lt- A, if the reduction relation holds between the initial states of the machines, i.e., if to & lt- sq — otherwise в is not a reduction of A, written B? A.
3. FSM Testing
In this paper, we assume that the specification FSM a from which we generate tests is a complete observable FSM that is not necessarily deterministic, while an implementation is a complete deterministic FSM. In addition, we assume that a reliable reset operation is available in any implementation. The conformance relation is the reduction relation.
Let 3(A) be a set of complete deterministic implementation machines over the input alphabet of A, called a fault domain. FSM B є 3(A) is a conforming implementation of A if B & lt- A.
Given FSM A = (S, s0, I, O, h) and U = (P, p0, I, O, f), U is said to be an unfolding of the FSM a if the following conditions are satisfied:
U & lt- A,
Tru is finite (i.e., U has no cycles),
U — after -a = U — after -p implies a=p for all а, рє TrU (i.e., U is a tree).
Here we notice that according to the second assumption, each unfolding of FSM a is a partial machine. An unfolding can be obtained by transforming the graph ofA into a tree, while skipping some traces of A. The tree structure of an unfolding is fully determined by the
РИ, 2004, № 3
set of its traces, so we can always use Try to refer to the unfolding U.
Given FSM U = (P, p0, I, O, f), the FSM Comu = (Pu {DNC}, p0, I, O, F) is the complete form of the machine a if the behavior function f is obtained by using the following rules
(p'-, o) є F (p, i), if (p'-, o) є f (p, i)
(DNC, o) є F, if f (p, i) = 0 (DNC, o) є F (DNC, i).
An FSM U is said to be a test of a if U is an unfolding of a. A test may have transitions with different inputs from a same state. We assume, therefore, that a particular tester executing such test selects one among alternative inputs during a particular test.
Given a test U of the specification FSM A and an implementation FSM B є 3(A), we say that an implementation FSM b passes the test U, if B & lt- ComU, otherwise в fails the test U.
A test U is said to be complete for a in the fault domain 3(A) if any B є 3(A), which is not a conforming implementation of A, fails the test U. The set 3(A) that contains all complete deterministic FSM with at most m states is denoted 3 m (A). A test is said to be m -complete if it is complete in the fault domain 3 m (A). Clearly, an m -complete test is also k -complete for any k & lt- m •
Next we consider test generation for the reduction relation.
4. Test Generation
In this section, we propose how a test suite w.r.t. the reduction relation can be generated.
4.1. Preliminaries
State s of FSM A = (S, s0, I, O, h) and state t of B = (T, t0, I, O, g) are said to be r (1) -distinguishable if there exists input a such that at these states the sets of output responses to input a do not intersect, i.e. out (t, a) nout (s, a) = 0. The set of traces {p є TrA (s)|P^i = a) represents the r -distinguishingtraces of s w.r.t. t, denoted p (s, t) — while jp є TrB (t)|p^ = a] represents the r -distinguishing traces of t w.r.t. s, denoted p (t, s). Given k & gt- 1, state s of FSM A and state t of в are said to be r (k) -distinguishable, if the states are r (k -1) -distinguishable or there exists an input a such that for each trace P є TrA (s) n TrB (t) n {(a, o): o є O}, states s — after — p and t — after — p are r (k -1) -distinguishable. The set of traces
P (s, t)
P є TrA (s)n TrB (t) n{(a, o): o є O} л yep (s — after — p, t — after — P)
represents the r -distinguishing traces ofs w.r.t. t and
p (t, s)
P є TrA (s)n TrB (t) n{(a, o): o є O} л у ep (t — after — p, s — after — P)
represents those of t w.r.t. s. State s of FSM a and state t of в are said to be r -distinguishable, denoted s 4−1, if there exists k & gt- 0 such that states s and t are r (k) -distinguishable [1]. FSM a and в are r -distinguishable, denoted A 4- B, if their initial states are r -distinguishable.
Proposition 4.1. Given complete FSM A = (S, s0, I, O, h) and FSM B = (T, G, I, O, g), let states s and s'- of FSM A be r -distinguishable. Then for any state t of FSM B it holds that t? s or t? s'-.
As a corollary to Proposition 4. 1, the following statement holds.
Proposition 4.2. Given complete FSM A = (S, s0, I, O, h) and B = (T, t0, I, O, g), let two states A — after -a and A — after-p be r -distinguishable. Then B — after-a= B — after-p implies that B? A.
Given FSM A = (S, s0, I, O, h) and FSM B = (T, t0, I, O, g), the FSM AnB = (Q, q0, I, O, ці) is the intersection of A and B if Q c Sx T, q0 = s0t0 and the behavior function у is obtained by using the following rule
(s'-t'-, o) є & lt-p (st, i) «(s'-, o) є h (s, i) л (t'-, o) є g (t, i).
Let a be a specification FSM, B = (T, G, I, O, g) be an implementation FSM, B e3m (A), and
A n B = (Q, q0, I, O, ф). We define the r -distinguishing machine of A and в, denoted Va, b, as an FSM (Q u {Fail}, q0, I, O u {fail}, ф), where
y ((s, t,), a) = 9((s, t), a) if out (t, a) є out (s, a) — and V ((s, t), a) = {Fail, fail} if out (t, a) g out (s, a). When it is clear from the context, we use V instead of V a, b.
For a given implementation machine B such that B? A, a test Ua = (P, p0, I, O, f) to «kill» B should have a trace рє TrB such that for input a defined at state U — after — p it holds that
out (B — after — P, a)? out (A — after -p, a) —
in this case, we say that the test U covers a fail-transition (a transition with the output fail) in V a, b.
If FSM в is not a reduction of a then any input sequence, that applied at the initial state of V, covers a fail-transition distinguishes в from a and can be used as a test case to detect faults modeled by B.
Proposition 4.3. Given two complete FSM, A = (S, s0, I, O, h) with n states and B = (T, t0, I, O, g) with m states,
let VA, B = (Q u{Fail}, q0, I, O u{fail}, ф) be the r -distinguishing machine of a and в. Then
РИ, 2004, № 3
— |Q| & lt- nm-
— If (s, t), (s'-, t) є Q and s f s'- then a fail-transition is covered either from state (s, t) or from state (s'-, t) by r -distinguishing traces of s or t.
— Let (s'-, t) and (s, t) be states of VA, B such that s'- & lt- s, if a fail-transition is covered from (s, t) by some trace then a fail-transition is also covered from state (s'-, t) by the same trace.
Proposition 4. 3(a) indicates the upper bound on tests that are m -complete. The upper bound is tight [1], since for each n and m there exist the specification machine A with n states and an implementation machine в with m states such that the shortest sequence that distinguishes в from a has length mn. As a corollary, the following statement holds.
Proposition 4.4 [1]. Given the complete specification FSM A = (S, sq, I, O, h) with n states, the unfolding U of FSM A that has each trace ofFSM A with length mn, is an m -complete test suite for the FSM a.
4.2. Test Generation Method
Given a deterministic FSM B є 3m (A), в? A, certain states in Va, b have to have fail-transitions [2]. In particular, according to Proposition 4. 3(b), r -distinguishable states ofFSM A may create such states. States (s, t) and (s'-, t) of Va, b are said to be r -conflicting if s 4 s'-. Therefore, if a test Ua has traces P and у such that V A, B — after — p = (s, t) and
V A, B — after -y = (s'-, t) then a fail-transition would be covered if Ua also contains the concatenation of p with the distinguishing traces p (s, s'-), as well as the concatenation of у with the distinguishing traces p (s'-, s). The following statement is a direct corollary to Proposition 4. 3(b).
Lemma 4.1. Given B є 3m (A), let (s'-, t) and (s, t) be r -conflicting states of V a, b. If for a test U there exist P, ye TrU such that V A, B — after -p = (s, t),
V a, b — after -y = (s'-, t), Pp (s, s'-) c TrU, and
yp (s'-, s) c TrU then U covers a fail-transition in Va, b.
Similar to the SC-method [6], we introduce a designated r -countingfunction, denoted p, which for given states s, p є S of FSM A and a trace, а є Тга (s), returns a maximal length of a sequence of states, traversed by a, applied at state s, each of which is a reduction of all subsequent states in the sequence, including state p. Therefore, ps (p, a) = l, where l is the maximal
number of prefixes alv., a l of a such that 1 & lt-|a^ & lt-… & lt-|al|, and
s — after-a! & lt-… & lt- s — after-a l & lt- p.
It holds that |a|& gt-ps (p, a) & gt- 0 andps (p, a) = 0 if a is the empty sequence or none of the states traversed by
a non-empty sequence a is a reduction of p. We extend the counting function to sets of pairwise r -distinguishable states of a. Given state s є S, a trace p є Тга (p) and a set of pairwise г -distinguishable states R c S, let ps (R, P) denote Zps (p, P). We also use P (P, R) to
denote the set of traces (Pi,…, P i} for l = Ps (R, P).
We next introduce the notion of a deterministic core of FSM. State s є S of FSM A is deterministically reachable, (d -reachable, for short) if there exists an input sequence a such that (A — after — P|PtI = a} = (s}. A minimal set of d -reachable states that contains the initial state and, for each d -reachable state s є S, a state that is a reduction of s is called a d -core of FSM A. A minimal unfolding к of a is said to be a d -core cover of A if for each d -reachable state s in the d -core, к has a trace that deterministically takes a from the initial state to state s. Intuitively, if a state of a does not have a reduction that is d -reachable then it may not be «implemented» even in a conforming implementation machine B є 3m (A).
A trace v є Trva b is said to be reduction-acyclic (г -acyclic, for short) in V a, b if, for any two non-empty prefixes a and p of v, |a| & lt- |p|, it holds that if V A, B — after-a = (s, t), V A, B — after-p = (s'-, t'-), and s'- & lt- s, then t ф t'-. We will use the r -counting function to determine r -acyclic traces when unfolding FSM a. In particular, if l = pp (R, P) & gt- m — |Rd|, where Rd is the subset of states of r that have a reduction in the d -core, then by definition of the function p, p has l prefixes Pi,…, Pi, 0 & lt-|Pi| & lt-… & lt-|p, such that in any r -distinguishing machine the trace p either traverses г -conflicting states or is r -acyclic.
Proposition 4.5. Let к be a set of traces that deterministically reach states of a subset m in FSM a
and G be an unfolding of a, such that тГо = и a- N-,
where N- =0 if the number of pairwise r -distinguishable states in the set M is more than m, otherwise N- comprises each shortest trace Рє TrA-after-a, such that
PA-after-Oj (R, P) _ m _ |Rd| +1
for some set R of pairwise r -distinguishable states where Rd is a subset of states ofR that have a reduction in the set m. The following statements hold.
— If FSM a has no г -distinguishable states then the test G covers a fail-transition in each V a, b such that B є 3m (A) and B? A.
— If the number of pairwise r -distinguishable states in the set M is more than m then the set
РИ, 2004, № 3
(V А, в — after — а|а є K} contains conflicting states in each V А, в such that B e3m (A) and в? A.
— Let B e3m (A), в? A and в passes the test G. Then there exist а- є K, p є N- and R (a- P) such that the set
(vA, B-after-& lt-x|a6 K or a = a- y, ai є K and ye P (P, R (a, P))}
contains conflicting states.
Combining the results of Proposition 4.5 with Lemma 4. 1, we obtain a preset method for generating tests for the reduction relation.
In this paper, we abandon preset strategy of test generation and alternate between test generation and execution, so we generate a test that is not m -complete, but declares the fail verdict if a given IUT is not a reduction of the specification.
Algorithm for deriving an adaptive test suite.
Input: FSM A over the input set I and the output set O, and an unknown FSM B є 3m (A) ?.
Output: The verdict fail if в? A- the verdict pass if B & lt- A and the test which в passes.
1. Determine the d -core cover k of a and unfold FSM a into the test U that represents all the traces of the d -corecover.
2. Execute the test U against FSM в. If B does not pass the test then produce the verdict fail. END. If в passes the test, delete from U each trace that was not observed in в, i.e., derive the FSM U n B and its complete form G (U, в) (a plausible implementation machine that passes the test U).
3. Determine the FSM A := G (U, B) n A, ad -core m and a d -core cover к of the restricted specification FSM A. Determine all the maximal sets of pairwise r -distinguishable states Rb…, Rf of the FSM A.
4. If for each trace ар є TrU^B, where, а є K, there exists i, 1 & lt- i & lt- f, such that
PG (U, B)-after-a (RbP) = m_|Rd | +1
where R d is a subset of states ofR that have a reduction in the d -core m, then go to Step 5. Otherwise, determine the unfolding U of the machine a by extending the set oftraces TrU^B as follows. For a trace ар є TrU^B such that, а є K and
PG (U, B)-after-a (Rb P) & lt- m_|Rd| +1 for all i, 1 & lt- i & lt- f, include aP (i, o) into the set TrU for each (i, o) є I x O such that aP (i, o) є TrA, and go to Step 2.
5. Determine r -distinguishing traces for each pair of r -distinguishable states of a. Derive the set
T1 = {ар (A — after -a, s), ає K, s є S}.
For each trace ар є TrU^B, where, а є K, determine a set R of pairwise distinguishable states such that PG (U, B)-after-a (R, P) = m — |R '-| +1, and derive the set
Tap = {ayp (A — after — ay, s), у є P (R, P), s є S}.
Denote T2 the union of Tap over all ар є TrU^B.
6. If в passes the test suite TS = T u T2 produce the verdict pass, as в & lt- A, and the test TS which в passes. If в does not pass the test suite TS produce the verdict fail, as в? A, and the test TS which в does not pass.
As an example, consider a nondeterministic FSM in Figure 1 and assume that an implementation FSM has at most two states. Let an FSM in Figure 2 be an implementation FSM.
a P/0,Q/1 P/0
b Q/0,P/1 P/0,1
Fig. 1. The specification FSM A
1 2
a 2/1 1/0
b 1/1 1/1
Fig. 2. An implementation FSM B
The specification FSM has the only deterministically reachable state, namely, the initial state. According to Step 4, we unfold the specification FSM for each input.
The unfolding U has traces (a / 0, a /1, b / 0, b /1}.
The complete form G (U, B) of the machine U n B is shown in Figure 3.
1 2
a 2/1 2/0,1
b 2/1 2/0,1
Fig. 3. The complete form G (U, B)
We restrict the specification FSM according to our observations, i.e. A := G (U, B) n A (Figure 4).
a R/1 Q/0, R/1 Q/0
b Q/1 Q/1, R/0 Q/0,1
Fig. 4. A := G (U, B) n A
After counting states via each trace we assure that none of the traces of U satisfies the conditions of Step 4. Therefore, we append the input a with each possible input and obtain the unfolding U with the set (aa /10, aa /11, ab /10, ab /11} of traces. The complete form G (U, B) of the machine U n B is shown in Fig. 5.
РИ, 2004, № 3
1 2 3
a 2/1 3/0 3/0,1
b 3/1 3/1 3/0,1
Fig. 5. The second complete form G (U, B)
We intersect the machine in Fig. 5 with a and obtain the next machine A shown in Fig. 6.
a Q/1 R/0 S/1 R/0 T/0, S/1
b R/1 T/1 R/1 T/0,1 S/0,T/1
Fig. 6. FSM A := G (U, B) n A
By direct inspection, one can assure that for the FSM in Figure 6 it holds that P f Q, Q f R, R у S, P f S. Input a r -distinguishes p and Q, Q and r, r and S and p and S. Moreover, it holds that p & lt- r, r & lt- t, Q & lt- S, Q & lt- T. For this reason, when counting states via
the traces aa/10, ab/10 the condition of Step 4 is satisfied. However, the condition is not satisfied for the trace b /1. Similar to the previous case, we append the input b with each possible input, obtain the unfolding U with the set {ba/10,ba/11,bb/10,bb/11} of traces and perform the same sequence of actions. Each trace of the next specification machine A satisfies the condition of Step 4. Thus, we append traces aa/10 and ba /11 with the r -distinguishing traces a /1 and a / 0, respectively, since these traces traverse r -distinguishable states, and assure that the implementation passes the obtained test suite, i.e., the implementation in Figure 2 is a reduction of the specification FSM in Figure 1. This fact was established using the adaptive test suite {a /1, aa /10, ab /11, bb /11, aaa /101, baa /110}. The length of the test suite including the reset input is 24, while the length of a preset test suite returned by the method in [1] is 32. On the other hand, let an implementation FSM be a machine d shown in Figure 7. By direct inspection, one can assure that D is not a reduction of A. The machine d has a trace aa/11 that is not a trace of a. We first unfold the FSM a for inputs a and b. The next specification FSM A := G (U, D) n A coincides with the machine in Figure 4. We append the input a with each possible input and the implementation d fails the obtained test suite. Then the adaptive test suite returned be the above method has the total length 7.
5. Conclusion
In this paper, we have proposed a method for deriving an adaptive test suite from a nondeterministic specification FSM w.r.t. the reduction relation. Simple application examples clearly show that an adaptive test suite is usually shorter than a preset test suite, since the latter is counted on the worst case of an implementation FSM. Moreover, differently from [3] we take into account the reduction relation between states of the specification- thus, our method performs better than [3].
References: 1. Petrenko A., Yevtushenko N., Bochmann G.V. Testing deterministic implementations from their nondeterministic specifications // In: Proc. of the IFIP 9th International Workshop on Testing of Communicating Systems, Germany, 1996. P. 125−140. 2. KoufarevaI.B. Test suite derevation from nondeterministic FSM // PhD Thesis, Tomsk State University, 2000. 154 p. (in Russian).
3. Hieron R.M. Adaptive testing of a deterministic implementation against a nondeterministic finite state machine // The computer journal, 1998. V. 41. P. 349−355.
4. Vetrova M. V. Elaborating FSM-based strategies for the compensator design and testing // PhD Thesis, Tomsk State University, 2004, 152 p. (in Russian). 5. Starke P.H. Abstract Automata. North-Holland/American Elsevier, 1972, 419 p. 6. Petrenko A., Yevtushenko N. On test derivation from partial specifications // In: Proc. of the IFIP Joint Internationl conference FoRtE/PSTV, Italy, 2000. P. 85 102.
Поступила в редколлегию 14. 08. 2004
Рецензент: д-р техн. наук, проф. Хаханов В. И.
Dorofeeva Margarita Yurievna. Tomsk State University, Ph.D. Student. Test Derivation, Automata Theory. Tomsk State University, 634 050, 36 Lenin Street, (3822) 41−39−84.
Petrenko Alexander Fedorovich. Professor, Senior Researcher of CRIM, Montreal, Canada. Automata Theory, Test Derivation, Model Checking.
Vetrova Maria Viktorovna. Tomsk State University, Ph.D. Controller Design, Digital System Optimization, Test Derivation. Tomsk State University, 634 050, 36 Lenin Street, (3822) 41−39−84.
Yevtushenko Nina Vladimirovna. Professor of Tomsk State University. Automata Theory, Test Derivation, Model Checking. Tomsk State University, 634 050, 36 Lenin Street, (3822) 41−39−84.
a Q/1 P/1
b P/1 P/0
Fig. 7. Implementation FSM D
РИ, 2004, № 3

Показать Свернуть
Заполнить форму текущей работой