Elektrotehniški vestnik 83(3): 115-121, 2016 Original scientific paper
An Improved State-Counting-Based Construction of Complete Test Suites for FSM Implementations
Monika Kapus-Kolar
Jozef Stefan Institute, Department of Communication Systems, Jamova 39, SI-1111 Ljubljana, Slovenia E-mail: monika.kapus-kolar@ijs.si
Abstract. The paper addresses black-box conformance testing of objects specified as an arbitrary observable finite-state machine. It proposes a new state-counting-based method for the construction of complete test suites. The method brings new options for the definition of conformance, for assumptions on the object under test and for test preambles, and a strategy against harmfully redundant members of the employed preamble sets. Compared to similar methods, it is more widely applicable and customizable and in many cases able to produce a much shorter test suite.
Keywords: finite-state machine, conformance testing, conformance relation, complete test suite, state counting
Izboljšano na štetju stanj temelječe snovanje popolnih nizov preizkusov za izvedbe končnih avtomatov
Clanek obravnava preizkušanje skladnosti po principu črne škatle za objekte, specificirane kot poljuben končni avtomat. Predlaga novo na štetju stanj temelječo metodo za snovanje popolnih nizov preizkusov. Metoda prinaša nove moZnosti za definicijo skladnosti, za predpostavke o preizkusšanem objektu in za uvodne dele preizkusov ter strategijo proti škodljivo odvečnim članom uporabljenih mnozic uvodnih delov preizkusov. V primerjavi s podobnimi je širše uporabna, bolj prilagodljiva in v mnogih primerih sposobna zasnovati dosti krajši niz preizkusov.
1 Introduction
Observable finite-state machines (OFSMs) are abstract machines that to each input specified in their current state reply with an output and the corresponding change of the state. In model-based black-box testing, they are widely employed both as models of what the object under test is supposed to be and as models of what it might be in the reality. in this paper, we propose a new complete test suite (CTS) construction method that is able to handle any specification OFSM and for the OFSM under test assumes only that it has at most a given number of reachable states and never refuses a relevant input without previously producing an erroneous output. Currently, the only such method is the state-counting-based method of [1] (with a slight improvement proposed in [2]), for which theoretical foundations are laid in [3]. in the following, the method of [1] improved as suggested in [2] is called 'the old method'.
Received 22 January 2016 Accepted 23 March 2016
In the old method, the only two conformance relations foreseen are quasi-equivalence and quasi-reduction, and they are covered with two separate procedures. The new method covers a much wider class of the conformance relation, with a single procedure. Besides, it is able to exploit additional assumptions on the extent to which the specified input/output sequences (IOSs) diverge (i.e., lead the OFSM to different states) in the implementation. As a third generalization, it is no longer assumed that the members of the initially constructed sets of test preambles must be IOSs taking the specification OFSM to a definitely reachable state. Unlike the old method, the new one also has a strategy against harmfully redundant elements of the preamble sets.
The new method was developed in [4], as an efficient specialization of our there proposed and formally proved new generic CTS construction method. It is presented in Section 3, after Section 2 presents our notation and definitions. In Section 3, we formally specify also the old method, by specifying its virtually only differences from the new one. Section 4 provides examples showing how useful the novelties of our method can be. Section 5 comprises a discussion and conclusions.
2 Notation and definitions
Definitions 1-5 introduce the basics of our notation. Definition 1.
•	X denotes the universe of inputs.
•	An IO is a sequence of an input and an output.
•	Q, s, x, X, y, U, 2 and Z, possibly decorated, denote, respectively, an OFSM, a state, an input, an input set, an output, an IO set, an IOS and an IOS set.
Definition 2. For each OFSM Q:
116
KAPUS-KOLAR
•	st(Q) denotes the set of all its reachable states.
•	init(Q) denotes the initial state.
•	For each state s e st(Q), ios(s) denotes the set of all IOSs executable from s.
•	ios (Q) denotes ios (init (Q)).
•	For each IOS z e ios(Q), ios(Q, z) denotes the IOS set [z'\zz' e ios(Q)}.
•	For each IOS set Z C ios(Q), ioss(Q,Z) denotes the IOS set set {ios(Q, z)\z e Z}.
•	For each IOS z e ios(Q), in(Q, z) denotes the input set {x\By : (zxy e ios(Q))}.
•	For each IOS z e ios(Q) and input x, out(Q,z,x) denotes the output set {y\zxy e ios(Q)}.
•	For each IOS set Z C ios(Q), end(Q, Z) denotes the set of all states in which Q can be immediately after executing from init(Q) a member of Z.
Definition 3. For each IOS z = xiyix2y2 ■ ■ ■ xkyk:
•	In(z) denotes its length k, with e denoting an IOS of the length 0.
•	pf (z) denotes the set of all IOSs that are its prefix.
•	For each IOS z', z' < z iff (i.e. if and only if) z' e (pf (z) \ {z}).
Definition 4. For each IOS set Z:
•	max (Z) denotes the set
{z\(z e Z) A -Bz' e Z : (z < z')} of all its maximal members.
•	pf (Z) denotes the IOS set {z\Bz' e Z :(z e pf (z'))}.
•	For each IOS z e pf (Z), io(Z, z) denotes the IO set {xy\zxy e pf (Z)}.
Definition 5. For each IO set U:
•	in(U) denotes the input set {x\By : (xy e U)}.
•	For each input x, out(U,x) denotes the output set {y\xy e U}.
•	For each input x, io(U,x) denotes the IO set {xy\xy e U}.
Definitions 6-9 gradually introduce our candidates for the conformance relation.
Definition 6. A well-formed binary relation for IO sets (WBRIO) is such a set R of IO set pairs that for each IO set pair (U,U'), all the following is true:
(1)	(U, U') e R iff (io(U, x), io(U', x)) e R for each input x e in(U').
(2)	(U, U') e R only if out(U,x) C out(U',x) for each input x e in(U').
(3)	If out(U,x) = out(U',x) for each input x e in(U'), then (U,U') e R.
(4)	(U,U'') e R for each IO set U' ' with ((U,U') e R) A ((U',u'') e R).
Definition 7. For each input set X, br (X) denotes the WBRIO consisting of all IO set pairs (U,U') that for each input x e in(U') satisfy all the following:
(1)	0 C out(U,x) C out(U' , x)
(2)	If x e X then out(U,x) = out(U',x).
Definition 8. For each IOS set pair (Z, Z') and WBRIO R:
•	For each IOS z e pf (Z'), Z Z' iff for each
IOS z ' with (z' < z) A (z' e pf (z)), (io(Z,z'), io(Z',z')) e R.
•	For each IOS set Z '' C pf (Z '), Z	Z' iff Z 3r , z Z' for each IOS z e Z''.
•	Z uR Z' iff Z 3r ,z' Z '.
Definition 9. For each OFSM pair (Q, Q'):
•	For each WBRIO R and IOS z e ios (Q'), Q Ur,z Q' iff ios(Q) Ur,z ios(Q').
•	For each WBRIO R and IOS set Z C ios(Q'), Q Ur,z Q' iff ios(Q) Ur,z ios(Q').
•	For each WBRIO R, Q Ur Q' iff Q URiOS(Q') Q'.
•	Q is quasi-equivalent to Q' iff Q Ubr(x) Q'.
•	Q is a quasi-reduction of Q' iff Q Ubr(0) Q'. Definitions 10-15 introduce concepts related to the
CTS construction.
Definition 10.
•	M denotes the specification OFSM.
•	N denotes the OFSM under test.
•	Ua denotes the conformance relation, with A presumably a given WBRIO.
•	I denotes the set of all candidates for N, presumably the set of all OFSMs Q that satisfy all the following:
(1)	For each IOS z C (ios(M) n ios(Q)), in(M,z) C in(Q,z).
(2)	\st(Q)\ is not more than a given upper bound m, presumably a non-zero natural.
(3)	For each IOS set Z C (ios(M) n ios(Q)),
\ end(Q, Z)\ is not more than a given upper bound ub(Z), presumably a natural with 1 < ub(Z) < m whose default value is m.
Definition 11. For each OFSM Q:
•	For each IOS z = xiyix2y2 ■ ■ ■ xuyu, imp(Q, z) denotes the set of all IOSs in ios(Q) that are of the form xiyix2y2 ■ ■ ■ x—iyi-ixiyi with 0 < i < k, i.e., the set representing the implementation of z in Q.
•	For each IOS set Z, imp(Q, Z) denotes the IOS set {z\Bz' e Z : (z e imp(Q,z'))}.
Definition 12.
•	A test is a member of ios(M).
•	A test suite is a set of tests.
•	A given OFSM Q passes a given test suite Z iff
Q UA,Z M, iff Q UA,max(imp(M,Z))\{e} M.
•	Accordingly, we define the length len(Z) of a given
test suite Z as £ze(max (imp(M,Z))\{s})(1 + ln(z)),
counting also the resets that are assumed to precede each test in max (imp (M, Z)) \ {e}.
AN IMPROVED STATE-COUNTING-BASED CONSTRUCTION OF COMPLETE TEST SUITES
117
•	A given test suite Z is complete iff Q □A M for each OFSM Q el with Q 3a,z M.
Definition 13. A given state s e st(M) is definitely reachable if there exists an IOS set Z C ios (M) satisfying all the following:
(1)	end(M,Z) = {s}
(2)	Z n Z ' = 0 for each IOS set Z ' C imp(M, Z) with (Z' imp(M,Z)) A (pf (Z') = Z').
Definition 14. For each IOS set Z and IOS pair
{z, z'} C pf (Z), a (Z, z, z ')-distinguisher is a pair (z'', x) satisfying all the following:
(1)	z '' e (ios(Z,z) n ios(Z,z'))
(2)	x e (;nn(Z, zz'') n in(Z, z'z''))
(3)	out(Z,zz'',x) = out(Z,z'z'',x)
Definition 15. For each IOS pair {z,z'} C ios(M), a {z, z'}-separator is a set D satisfying all the following:
(1)	Every member of D is an
(ios(M), z, z')-distinguisher.
(2)	For the IOS set
Z = {z''z' '' xy\(z'' e {z, z'}) A ((z''', x) e D)A
(y e out(M,z''z''',x))} and each IOS set Z C imp(M, Z) with (Z' imp(M, Z)) A (pf (Z') = Z')A ({z,z'}C Z'), at least one of the following is true:
•	D comprises a (Z , z, z )-distinguisher.
•	D comprises a (z xyz , x ) with (z , x) a (Z', z, z')-distinguisher.
3 The new method
The new method is specified in Fig. 1. The constructed CTS is the T' conceived in Step 6. In Steps 1-5, one constructs an IOS set T C ios (M) and a set D of IOS pairs {z,z'} C ios(M) with a {z,z'}-separator. For each IOS z e T, T' is supposed to check N 0A,z M. For each pair {z, z'} e D, T' is supposed to check that in the case of {z, z'} C ios(N), z and z ' diverge in N. (T,D), hence, defines a set of very simple test goals, the goals into which Steps 1-5 decompose the goal that T' should check N □A M. In Step 6, each of the simple goals is satisfied in a most simple way.
The contributors of the elements of T and D are the IOS sets K collected in the set K constructed in Steps 13. The sets in K are subsets of ios(M) and we call their elements preambles, because the tests in T are constructed by their extension. For the optimality of K, there are conflicting criteria:
•	It is desirable that it is small, but one must secure that in the case of N 3A M, there is a K e K with K C ios (N). If there are multiple ways for implementing ios (M) correctly, one might prefer a K with more than one element. In any case, for each
1.	With the Fig. 2 procedure, obtain a K.
2.	K' ^0
3.	While one exists, take an IOS set K e (K\ K') for which there is no IOS set K' e (K\ K') with
ioss(M, K) c ioss(M, K') and do the following:
i.	With the Fig. 3 procedure, obtain the relevant part K' of K and a plan (V,W) for it.
ii.	VK' ^ V; WK' ^ W
iii.	While one exists, delete from K an IOS set K'' e (K\ K') with
ioss (M, K') C ioss (M, K'' ) C ioss(M,K) and do the following:
a.	K''' ^ {z\(z e K'')A
3z' e K' : (ios(M,z) = ios(M, z'))}
b.	k(K''') ^ K'; K ^ (KU {K'''})
c.	K^ {Z\(Z eK) A —3Z' eK :(Z' c Z)}
d.	K' ^ (K' U {K'''})
4.	T ^ {aft\3K e K, (a', /3) e Vk(K) :
(ios(M, a) = ios(M, a'))}
5.	D ^ {{aiz, a2z'}
\3K e K, (a'1,z, a'2,z') e Wk(K) : (({ai,a2} C K)A (ios(M, a1) = ios(M, a[))A (ios(M, a2) = ios(M, a2)))}
6.	Let T' ^ T and then for each IOS pair {z, z'} e D:
1.	Choose a {z, z'}-separator.
2.	For each member (z , x) of the separator:
i.	Choose an output y e out(M, zz'', x) and an output y e out(M, z z , x).
ii.	T' ^ (T' U {zz''xy, z'z''xy'})
Figure 1. The new method
IOS set pair {K, K'} C K with K c K', K' is a redundant member of K.
•	For each K e K, it is desirable that it is small, but it must comprise at least e and it can be helpful if it has at least one large subset K' with a {z, z'}-separator for each {z, z'} C K' with z = z'. In any case, for each subset {z, z'} of a K eK with (z = z') A (z' = e) A (ios(M,z) □A ios(M,z')), z' is a redundant member of K.
•	The optimality of K also depends on the exact nature of the available separators, but this is not considered in the method.
In Step 1, the method constructs the initial version of K, with the Fig. 2 procedure. Its strategy in the step is to make K small, but still sufficient, and its individual members K small, but still possessing a promising end(M,K). Unlike in the old method, those IOSs in ios(M) that do not lead M to a definitely reachable state are also considered for inclusion into the elements of K.
In Step 3 of the method, one forms a plan how
118
KAPUS-KOLAR
1.	S ^ st(M)
2.	While one exists, take a state pair {s, s'} C S with
(s = init(M)) A (s' = s) A (ios(s') ios(s)) and delete s from S.
3.	For each state s e S, choose a test set Zs satisfying all the following:
(1)	s e end(M,Zs)
(2)	Z n Zs = 0 for each IOS Z C imp(M, Zs) with (Z ^a imp(M,Zs)) A (pf (Z) = Z).
(3)	If s = init(M) then Zs = {e}.
The default is to minimize, in the given order, \end(M, Zs)\, \Zs\ and len(Zs).
4.	P ^ {z\3s e S : (z e Zs)}
5.	K^ {(P n Z)\(Z C imp(M, P)) A (pf (Z) = Z)A
(Z imp(M, P))A
6.	K^ {Z\(Z eK) A —3Z' eK :(Z' C Z)}
7.	For each IOS set K eK:
i.	K^ (K\{K})
ii.	While one exists, take an IOS pair {z, z } C K with (z = e) A (z = z)A
(ios(M,z') 3a ios(M,z)) and delete z from K.
iii.	K ^ (KU{K})
8.	K^ {Z\(Z eK) A -3Z' eK :(Z' C Z)}_
Figure 2. Construction of the initial version of K
to accommodate individual K e K, i.e., what their contributions to T and D should be. Actually, for each IOS set set Y e {ioss(M, K)\K e K}, one forms a plan for just one K e K with ioss (M, K) = Y, whereas for the remaining K' eK with ioss (M, K') = Y, one just sets k(K') to K, thereby deciding that they will be accommodated analogously. k(K) is also set to K.
Whenever the Fig. 1 procedure decides to construct a plan for a K e K, it calls the Fig. 3 procedure. The procedure constructs the plan and possibly detects some redundant members of K, so that the plan is actually for K , the computed relevant part of K. After K and its plan are computed, the Fig. 1 procedure reduces K to K , analogously reduces the remaining K e K with ioss(M, K') C ioss(M, K'') C ioss(M, K) and deletes every member of K that consequently becomes redundant.
In the Fig. 3 procedure, one builds the relevant part K' of the given K and a plan (V,W) for it gradually. Initially, K' comprises just e, whereas V and W are empty sets. For each IOS a e K already in K', giving priority to the maximal ones among the yet unconsid-ered current members of K , one then constructs the following:
1. A set B comprising each IOS ¡3 e ios(M,a) that is just enough long that ios (M,a3) = 0 or one can construct for it a specifically formed triplet (L, C, W') (the conditions which the triplet is sup-
17V^ 2. While one exists, add to K an IOS a e max(K' \ K'') and do the following:
i.	B ^ {e};
ii.	While B = 0, delete from B an IOS 3 and then
if ios(M, a3) = 0 then let V ^ (V U {(a, 3)}) else if there is a triplet (L, C, W ) satisfying all the following:
(1)	L C K
(2)	0C C C pf (a3) \ pf (a)
(3)	\C\ > ub(L U C) - \L\
(4)	W is a set of 4-tuples (a , z, a , z ) satisfying all the following:
(a)	{a', a''} C (L U {a})
(b)	{a'z, a''z'} C (L U C)
(c)	There is an {a'z, a'' z'}-separator.
(5)	{a', e, a'', e} e W' for each IOS pair { a , a } C L with a = a .
(6)	{a, z, a, z'} e W' for each IOS pair { az, az } C C with
(z < z') A (ios(M, az) ios(M, az')).
(7)	{a', e, a, z} e W' for each IOS pair {a', az} with (a' e L) A (az e C)A (ios(M, a') ios(M, az)).
then do all the following:
a.	Choose such a triplet (L, C, W'). The default is to minimize, in the given order, \L \ K'\ and \W' \ W\.
b.	K' ^ (K' U L)
c.	V ^ (V U {(a, 3)}); W ^ (W U W') else B ^ (B U {3xy\xy e io(M, a3)})
Figure 3. Computation of the relevant part K' of a K and conception of a plan (V, W) for its contributions to (T, D)
posed to satisfy originate in a state-counting-based conformance testing principle suggested in [3] and improved and generalized in [4]). For each 3 e B, (a, 3) is added to V, where it specifies that a3 is to be included into T.
2. For each 3 e B with ios (M, a3) = 0, the required (L, C, W'). Note the following:
i.	L is a subset of K and each of its members is added to K .
ii.	C is a subset of pf (a3) with \C\ > ub(LU C) -\L\ . Unlike the old method, we foresee also the possibility of ub (L U C) < m. In such a case, 3 can be shorter and C smaller.
iii.	W' is a set of 4-tuples (a', z, a'', z'') with ({a ', a ''} C (L U {a})) A ({a'z, a''z'} C {L U C} and an {a'z, a''z'}-separator. Each such 4-tuple is added to W, where it specifies that {a z, a z } is to be included into D.
Note that the plan (V, W) constructed for the final K ,
AN IMPROVED STATE-COUNTING-BASED CONSTRUCTION OF COMPLETE TEST SUITES
119
subsequently called (VK',WK'), explicitly refers to individual members of K'. This is to make it possible that the remaining K'' e K with ioss(M,K') C ioss(M,K'') C ioss(M,K) are handled analogously to K. Like the relevant part of K, their relevant parts contribute to T and D only if they are not subsequently deleted from K. In the old method, there is no optimization of K beyond its initial version.
The ways in which the old method differs from the new one are virtually just the following (plus the consequently possible procedural simplifications):
1.	For the conformance relation one assumes A e {br(0), br(X)}.
2.	For each IOS set Z C ios(M), one assumes ub(Z) =

x,/y, x3/y4	r/tj, ^ r/ti2	a/0
-rrs^—»rs:^ y b/Q
x2/y3 (a)
Figure 4. Three example OFSMs
c/0 (c)
3.	In Step 1 of the Fig. 2 procedure, S is initialized not to st(M), but to the set of all definitely reachable states of M.
4.	In Step 1 of the Fig. 3 procedure, K' is initialized not to {e}, but to K.
4 Examples showing how useful the
novelties can be
Each of the example OFSMs Q will be presented in the usual way, as a rooted directed graph in which each state of Q is represented as a vertex, the initial state of Q is represented as the root vertex and each transition of Q, executing an IO xy and leading from a state s to a state s', is represent as an edge labelled with x/y and leading from the s vertex to the s vertex.
Example 1. The common property of quasi-equivalence and quasi-reduction is that for each of the specified inputs, the legal responses are only the specified alternative outputs. The difference is that in the first case, all the alternatives need to be implemented in the OFSM under test, whereas in the second case, it suffices to implement just one. We observe that to instead prescribe 'all or at least three', for example, would also be a practically interesting option. This conformance relation also belongs to the class that the new method can handle.
Example 2. Suppose that M is the OFSM in Fig. 4(a), A = br(0), m = 2 and the IOSs starting with xiyi are considered more important than those starting with x1y2, for example because y1 is an alarm, whereas y2 is not. The old method cannot be instructed to check the implementation of the less important IOSs to a desired extent less thoroughly, whereas the new method can. For this, one would for each such IOS z set ub(pf (z)) to an appropriate value of less than m, let's say to 1. The best T that one can obtain with the new method is then {xiyix2y3x2y3,xiy2x3y4}, whereas with ub(Z) = m for each IOS set Z C ios(M), the best possible T' is
{xiyix2y3x2y3, xiy2x3y4x3y4}.
Example 3. Suppose that M is the OFSM depicted in Fig. 4(b), with q a given non-zero natural. The OFSM specifies, for example, an agent selling vouchers for transactions of types 1 to q and acting as follows:
•	For each 1 < i < q, the agent can in the initial state accept a request n for a voucher for a type i transaction.
•	For each voucher request ri, the agent first returns its terms of sale, by an unknown algorithm choosing between tiji and tij2. By consequently changing its state to si i or sij2, respectively, it records the offer and waits for an input a indicating that the client accepts the terms or an input c indicating that the client cancels the request.
•	Upon receiving a in a state sij, the agent issues a voucher vij for a type i transaction under terms tij and returns to the initial state.
•	Upon receiving c in a state sitj, the agent issues n, to indicate its readiness for the next request, and returns to the initial state.
Suppose that A = br (0) and m > 2q +1. If one executes the new method optimally, one makes the following choices:
•	K^ {K |({e} C K C ios (M)) A (\K | = q +1)A
yi < i < q : 3ritiJ e K}
•	T ^ {z\(z e ios(M)) A (In(z) = 2(m - q) + 3)}
•	D ^ {{z,z'}\({z,z'}C pf (T))A
(\end(M, {z,z'})| = 2)A (s0 e end(M, {z,z'}))}
•	For each IOS pair {z, z } e D, the selected {z, z }-separator is {(e, a)}.
•	T' ^ {zavi}j Kzav.i j e ios(M))A
(In(z) = 2(m - q) + 3)}
The CTS T' is of the length (2(m - q) + 5)q(4q)m-q+i. For a comparison, if Step 1 of the Fig. 2 procedure is executed as in the old method, the best choices that one can make are the following:
•	K^{{e}}
•	T ^ {z\(z e ios(M)) A (In(z) = 2m)}
•	D ^0
•	T' ^ T
Now len(T') is (2m +1)(4q)m. Note that for any fixed m - 2q,
(2(m - q) + 5)q(4q)m-q+1 q-1^	(2m + l)(4q)m
21-2q q2-q
m
120
KAPUS-KOLAR
meaning that for any given percentage p, there are infinitely many pairs (q, m) for which the savings in the CTS length thanks to the additional freedom for preambles can be at least p.
Example 4. Suppose that M is the OFSM in Fig. 4(c), A = br (0) and m = 2. If one executes the new method optimally, one makes the following choices:
•	K^ {{e,a0}}
•	T' ^ {a0b0d0b0d0}
For a comparison, if Step 1 of the Fig. 3 procedure is executed as in the old method, the best choices that one can make are the following:
•	K^ {{e, a0, a0b0}}
•	T' ^ {a0b0c0b0c0b0}
Obviously, a0b0 should better not be present in the only member of K. Unlike the old method, the new one is able to detect that.
5 Discussion and conclusions
The current CTS construction methods similar to ours, hereby called 'the current methods', are those of papers [1]-[3], [5]-[24]. Here it is necessary to note that papers [9], [11], [19], [24] describe an adaptive testing process, in which CTS construction is interspersed with applications of the already constructed part. For each of the papers, what we call 'the method of the paper' is the method that it virtually proposes for test suite completion, where we assume that the method is given an empty test suite.
Unlike our method, the current ones are unable to handle conformance relations other than quasi-equivalence and quasi-reduction or exploit arbitrary upper bounds given on the extent to which individual sets of the specified IOSs diverge in the implementation. What they do have in common with our method is that they consist, at least implicitly, of two phases: decomposition of the initial test goal into a set of simple test goals and satisfaction of each of the simple goals. The initial goal is to test the conformance, while each of the simple goals is either to test the implementation of a given IOS or to test the divergence of a given pair of IOSs.
The way in which the current methods decompose the intial goal is virtually the same as in our method, except that the latter does not restrict preambles to IOSs leading the specification OFSM to a definitely reachable state and has a strategy against harmfully redundant members of the employed preamble sets. With the constraint relaxation and the strategy, our method potentially decomposes the initial goal into a simple goal set that can be satisfied by a shorter test suite.
While our method has a more advanced goal-decomposition procedure, its goal-satisfaction procedure is the simplest possible. Many current methods have a much better one, as they support also indirect goal
satisfaction [14]-[16], [18], [21], [23], [24]. In [25], we proposed and proved an advanced goal-satisfaction method that generalizes the goal-satisfaction procedures of all current methods and can be easily combined with our new goal-decomposition procedure. The method is generic, but we are developing for it also an efficient specialization. Another item for further study is how the goal-decomposition phase of the CTS construction could take into account the exact nature of the available separators.
References
[1]	A. Petrenko, N. Yevtushenko, "Conformance tests as checking experiments for partial nondeterministic FSM," in: Proc. FATES 2006 (Lecture Notes in Computer Science, vol. 3997), Springer, Berlin, 2006, pp. 118-133.
[2]	A. Petrenko, N. Yevtushenko, "Adaptive testing of nondetermin-istic systems with FSM," in: Proc. HASE 2014, IEEE CS, 2014, pp. 224-228.
[3]	A. Petrenko, N. Yevtushenko, "Testing from partial deterministic FSM specifications," IEEE T. Comput., vol. 54, no. 9, pp. 11541165, 2005.
[4]	M. Kapus-Kolar, Three Generalizations and a Better Implementation of the State Counting Method for the Construction of Complete Test Suites for FSM Implementations, JoZef Stefan Institute technical report #12039, 2016.
[5]	T.S. Chow, "Testing software design modeled by finite-state machines," IEEE T. Software Eng., vol. 4, no. 5, pp. 178-187, 1978.
[6]	S. Fujiwara, G. von Bochmann, F. Khendek, M. Amalou, "Test selection based on finite state models," IEEE T. Software Eng., vol. 17, no. 6, pp. 591-603, 1991.
[7]	G. Luo, G. von Bochmann, A. Petrenko, "Test selection based on communicating nondeterministic finite-state machines using a generalized Wp-method," IEEE T. Software Eng., vol. 20, no. 2, pp. 149-161, 1994.
[8]	A. Petrenko, N. Yevtushenko, G. von Bochmann, "Testing deterministic implementations from their nondeterministic specifications," in: Proc. IWTCS'96 (IFIP Advances in Information and Communication Technology, vol. 21), Chapman&Hall, London, 1996, pp. 125-140.
[9]	R.M. Hierons, "Adaptive testing of deterministic implementation against a nondeterministic finite state machine," Comput. J., vol. 41, no. 5, pp. 349-355, 1998.
[10]	I. Koufareva, A. Petrenko, N. Yevtushenko, "Test generation driven by user-defined fault models," in: Proc. IWTCS'99 (IFIP Advances in Information and Communication Technology, vol. 21), Springer, 1999, pp. 213-233.
[11]	R.M. Hierons, "Testing from a nondeterministic finite state machine using adaptive state counting," IEEE T. Comput., vol. 53, no. 10, pp. 1330-1342, 2004.
[12]	R. Dorofeeva, K. El-Fakih, N. Yevtushenko, "An improved conformance testing method," in: Proc. FORTE 2005 (Lecture Notes in Computer Science, vol. 3731), Springer, Berlin, 2005, pp. 204-218.
[13]	A.L. Bonifacio, A. Vieira Moura, A. da Silva Simao, "A generalized model-based test generation method," in: Proc. SEFM 2008, IEEE CS, 2008, pp. 139-148.
[14]	A. Simao, A. Petrenko, "Generating checking sequences for partial reduced finite state machines," in: Proc. TestCom/FATES 2008 (Lecture Notes in Computer Science, vol. 5047), Springer, Berlin, 2008, pp. 153-168.
[15]	A. Simao, A. Petrenko, "Checking sequence generation using state distinguishing subsequences," in: Proc. ICSTW 2009, IEEE CS, 2009, pp. 48-56.
[16]	M.E. Dincttirk, A Two Phase Approach for Checking Sequence Generation, M.Sc. Thesis, SabanciUniversity, August 2009.
AN IMPROVED STATE-COUNTING-BASED CONSTRUCTION OF COMPLETE TEST SUITES
121
[17]	L.L. Chaves Pedrosa, A. Vieira Moura, "Generalized partial test case generation method," in: Proc. SSIRI-C 2010, IEEE CS, 2010, pp. 70-77.
[18]	A. Simao, A. Petrenko, "Fault coverage-driven incremental test generation," Comput. J., vol. 53, no. 9, pp. 1508-1522, 2010.
[19]	A. Petrenko, N. Yevtushenko, "Adaptive testing of deterministic implementations specified by nondeterministic FSMs," in: Proc. ICTSS 2011 (Lecture Notes in Computer Science, vol. 7019), Springer, Berlin, 2011, pp. 162-178.
[20]	A.L. Bonifacio, A. Vieira Moura, A. Simao, "Model partitions and compact test case suites," Int. J. Found. Comput. S., vol. 23, no. 1, pp. 147-172, 2012.
[21]	A. Simao, A. Petrenko, N. Yevtushenko, "On reducing test length for FSMs with extra states," Softw. Test. Verif. Rel., vol. 22, no. 6, pp. 435-454, 2012.
[22]	L.L. Chaves Pedrosa, A. Vieira Moura, "Incremental testing of finite state machines," Softw. Test. Verif. Rel., vol. 23, no. 8, pp. 585-612, 2012.
[23]	A. Petrenko, A. Simao, N. Yevtushenko, "Generating checking sequences for nondeterministic finite state machines," in: Proc. ICST 2012, IEEE CS, 2012, pp. 310-319.
[24]	A. Petrenko, A. Simao, "Generalizing the DS-methods for testing non-deterministic FSMs," Comput. J., vol. 58, no. 7, pp. 16561672, 2015.
[25]	M. Kapus-Kolar, Incremental Construction of Complete Test Suites for Finite State Machine Implementations - Principles Behind the Current Methods and Beyond, Jozef Stefan Institute technical report #11855, 2015.
Monika Kapus-Kolar received her B.Sc. degree in electrical engineering from the University of Maribor, Slovenia, and her M.Sc. and Ph.D. degrees in computer science from the University of Ljubljana, Slovenia. Since 1981 she has been with the Jozef Stefan Institute, Ljubljana, where she is currently a researcher at the Department of Communication Systems. Her current research interests include formal specification techniques and methods for the development of real-time, concurrent and reactive systems.