Studying the separability relation between finite state machines

26

25

2010

Abstract: Many authors have studied relations between nondeterministic Finite State Machines (FSMs). These relations can be used, for example, for deriving conformance tests from specifications represented by FSMs. In this paper, the separability relation between FSMs is studied. In particular, an algorithm is presented that derives a shortest separating sequence of two nondeterministic FSMs. Given FSMs S with n states and T with m states it is shown that the upper bound on the length of a shortest separating sequence is 2^mn-1. Moreover, the upper bound is shown to be reachable. However, according to the conducted experiments, on average, the length of a shortest separating sequence of FSMs S and T states is less than mn and the existence of a separating sequence significantly depends on the number of nondeterministic transitions in these FSMs. The proposed algorithm can be also used for deriving a separating sequence of two different states of a single FSM or for deriving a separating sequence of three or more FSMs.

Index Terms: finite state machines, separability relation, conformance testing

1. INTRODUCTION

Finite State Machines (FSMs) are widely used in various application domains such as telecommunication systems, communication protocols and other reactive systems. In particular, FSMs are the underlying models for formal description techniques such as SDL and UML State Diagrams. Many conformance test derivation methods have been developed for deriving tests when the system specification and implementation are represented by deterministic FSMs. For related surveys, tools, and experiments a reader may refer to [1-5]. Moreover, many methods have been proposed for test derivation against nondeterministic FSM specifications [7-22]. Non-determinism in the specification occurs due to various reasons such as performance, flexibility, limited controllability, and abstraction [14] [17] [19] [23].

A number of methods have been proposed for test generation against nondeterministic FSM specifications with respect to various conformance relations. Some of these methods, as those given in [7, 8] [20], derive test suites with the unknown fault coverage. Many other methods derive test suites with the guaranteed fault coverage with respect to appropriate fault models. The methods given in [9] and [10] derive test suites with respect to the equivalence relation for a nondeterministic implementation against a nondeterministic specification while the methods given in [12], [14], [15], and [16] derive test suites for a complete deterministic implementation against a nondeterministic specification with respect to the reduction relation. Two FSMs are equivalent if they have the same input/output behavior and an FSM T is a reduction of FSM S if the input/output behavior of T is a subset of that of S. Hierons [17] presented a test derivation method with respect to the reduction relation when a system implementation can be nondeterministic. Petrenko et al. [21] generalize the work given in [24] and proposed a method that derives a test suite with respect to the reduction and equivalence relations for a nondeterministic implementation against possibly a partial specification.

When deriving test suites with respect to the reduction and equivalence relations with the guaranteed fault coverage the so-called complete testing assumption [9-10] (called "all weather conditions" by Milner in [25]) is assumed to be satisfied when testing a nondeterministic implementation. The assumption supposes that if an input sequence (a test case) is applied a number of times to a nondeterministic implementation, then all possible output sequences of the implementation can be observed. However, when an implementation under test has a limited controllability, as it happens, for instance, in remote testing, the complete testing assumption cannot be satisfied. In this case, the only relation that can be used for test derivation with the guaranteed fault coverage [26] [27] is the separability relation defined by Starke in [28]. Two FSMs are separable if there is an input sequence, called a separating sequence, such that the sets of output responses of these FSMs to the sequence do not intersect, i.e., the sets are disjoint. However, the separability relation is not properly studied yet. It is known [21] [27] that test suites derived with respect to the equivalence and reduction relations cannot be used for testing the separability relation. The fact that an FSM with m states is not equivalent (or is not a reduction) of an FSM with n states can always be established by an input sequence of length up to mn [21], while there exist two FSMs which can be separated only with an input sequence of exponential length [11].

Alur et al. [11] and Petrenko et al. [12] studied another relation, the so-called r-distinguishability relation. Petrenko et al. [12] employed this relation to reduce length of test suites derived with respect to the reduction relation. Two states s₁ and s₂ of a complete nondeterministic FSM are r-distinguishable if a state s of any complete FSM cannot be a reduction of both states s₁ and s₂ [21]. However, differently from the notion of state distinguishability for deterministic FSMs, in general, two r-distinguishable states can only be distinguished with a set of input sequences rather than with a single sequence. If states s₁ and s₂ are r-distinguishable with an r-distinguishablity set W then [21], given a state s of any complete FSM there always exists an input sequence in W such that the set of output responses at state s in response to this sequence is not a subset of that at state s₁ or at state s₂. Alur et al. [11] showed that a sequence in a shortest r-distinguishability set is of polynomial length and correspondingly, in an adaptive experiment, a state identification sequence of a nondeterministic FSM has polynomial length. However, when deriving a preset test suite against a nondeterministic specification FSM, the whole r-distinguishability set [12] [21] is needed for state identification. Separable states are r-distinguishable with a single sequence and therefore; separating sequences can be used for shortening test suites derived with respect to the reduction relation and separable states are r-distinguishable but the converse is not always true [11-12].

Alur et al. [11] proposed an algorithm for deriving a separating sequence for two separable states of an FSM with n states. At the first step of the algorithm, a finite automaton with states is derived. Based on this automaton a separating sequence can be derived when such a sequence exists. Moreover, as shown in Alur et al. [11], the upper bound on the length of a shortest separating sequence is exponential. However, Alur et al. do not give the exact upper bound and to the best of our knowledge no experiments are presented yet for estimating length of separating sequences.

In this paper, an algorithm is proposed that derives a shortest separating sequence of two given FSMs (if such a sequence exists) without the complete derivation of an automaton with exponential number of states as done in Alur et al. [11]. Moreover, some properties of a separating sequence are studied; in particular, it is shown that given FSMs S with n states and T with m states, the length of a shortest separating sequence is at most 2^mn-1. Given two arbitrary integers n and m, it is also shown that there always exist FSMs S with n states and T with m states such that length of a shortest separating sequence equals to 2^mn-1.

Experiments with the proposed algorithm show that on average, the length of a shortest separating sequence of two FSMs S with n states and T with m states is less than mn and the existence of a separating sequence significantly depends on the number of nondeterministic transitions in these FSMs. For all conducted experiments the upper bound 2^mn-1 on the length of a separating sequence was never reached.

This paper is organized as follows. Section 2 contains preliminaries related to FSMs. In Section 3, an algorithm is presented for deriving a shortest separating sequence of two separable FSMs. In addition, the upper bound on length of a separating sequence is determined and shown to be reachable. Section 4 contains an application example, Section 5 includes experimental results, and Section 6 concludes the paper.

2. PRELIMINARIES

A finite state machine (FSM) S, simply called a machine throughout the paper, is a 5-tuple S, I, O, h, s₁, where S is a finite nonempty set with s₁ as the initial state; I and O are finite input and output alphabets; and h S I O S is a behavior relation. The behavior relation defines all possible transitions of the machine. Given a current state s_j and an input symbol i, a 4-tuple (s_j,i,o,s_k) h represents a possible transition from state s_j under the input i to the next state s_k with the output o. A machine is deterministic if for each pair (s,i)SI there exists at most one pair (o,s)OS such that (s,i,o,s)h; otherwise, the machine is called nondeterministic. If for each pair (s,i)SI there exists (o,s)OS such that (s,i,o,s)h then FSM S is said to be complete; otherwise, the machine is called partial. Given FSMs S = S, I, O, h, s₁ and T =T,I,O,g,t₁, FSM T is a submachine of S if T S, t₁ = s₁ and g h.

Given FSM S = S, I, O, h, s₁, state s and an input i, state s is a successor of state s under the input i or simply an i-successor of state s if there exist o O such that the 4-tuple (s,i,o,s)h. Given a set of states M S and an input i, the set of states M is a successor of the set M under the input i or simply an i-successor of M if M is the set of all i-successors of states of the set M.

In a usual way, the behavior relation is extended to input and output sequences. Given states s,s S, an input sequence = i₁i₂…i_k I* and an output sequence = o₁o₂…o_k O*, there is a transition (s, , , s)h if there exist states s₁=s, s₂, … , s_k, s_k+1=s such that (s_i,i_i,o_i,s_i+1)h, i = 1, … , k. In this case, the input sequence is a defined input sequence at state s. Given states s and s, the defined input sequence can take (or simply takes) the FSM S from state s to state s if there exists an output sequence such that (s, , , s)h. The set successor(s, ) denotes the set of all states reachable from state s after applying the defined input sequence , i.e., successor(s, ) = {s: O^* [(s, , , s) h]}. The set out(s, ) denotes the set of all output sequences (responses) that the FSM S can produce at state s in response to a defined input sequence , i.e. out(s, ) = { : sS [(s, , , s) h]}. The pair /, out(s, ), is an Input/Output (I/O) sequence at state s; if s is the initial state s₁ then the pair / is an Input/Output (I/O) sequence of the FSM S. Given states s and s, the I/O sequence / can take (or simply takes) the FSM S from state s to state s if (s, , , s)h. A machine S is connected if for each s S there exists an input sequence that takes the FSM S from the initial state to state s. Given FSMs S = S, I, O, h, s₁ and T = T, I, O, g, t₁, the intersection S T is the largest connected submachine of FSM S T, I, O, f, s₁t₁ where (st,i,o,st) f (s,i,o,s) h (t,i,o,t) g.

Given two complete FSMs S = S, I, O, h, s₁ and T = T,I,O,g,t₁, state t of T and state s of S are non-separable, written t s, if for each input sequence I* it holds that out(t, ) out(s, ) , i.e., the sets of output responses to each input sequence at state t and at state s intersect; otherwise, states t and s are separable, written t ? s. For separable states t and s, there exists an input sequence I* such that out(t, ) out(s, ) = , i.e., the sets of output responses at states t and s to the input sequence are disjoint. In this case, is a separating sequence of states t and s, written t ? s, or simply separates t and s. The FSMs T and S are non-separable, written T S, if t₁ s₁. Otherwise, T and S are separable, written T ? S. If T and S are separable then a sequence that separates their initial states is a separating sequence of FSMs T and S, written T ? S. A separating sequence of the FSMs T and S is called shortest if any input sequence that separates T and S is not shorter than .

State t of the FSM T is a reduction of state s of the FSM S, written t s, if the set of I/O sequences of T at state t is a subset of that of S at state s; otherwise, t is not a reduction of state s, written t ? s. The FSM T is a reduction of FSM S if t₁ s₁, i.e., if the set of I/O sequences of T is a subset of that of S. If the sets of I/O sequences of the FSMs S and T coincide then these machines are equivalent. For deterministic complete FSMs, the reduction, equivalence, and non-separability relations coincide.

3. SEPERATING SEQUENCES: PROPERTIES, DERIVATION AND LENGTH

In this section some important properties of a separating sequence are established and an algorithm is proposed that derives a shortest separating sequence of two complete FSMs when such a sequence exists. Afterwards, the upper bound on the length of a shortest separating sequence is determined and shown to be reachable.

Let S = S, I, O, h, s₁ and T = T,I,O,g,t₁ be two complete separable FSMs. Given a shortest separating sequence i , i I, the sets of output responses of the FSMs S and T to intersect, while the sets of output responses of the FSMs S and T to i are disjoint. In other words, if S T = Q, I, O, f, q₁, q₁ = (s₁,t₁), then for every output sequence out(s₁, ) out(t₁, ) and for every state (s,t) where the I/O sequence / takes the intersection S T from the initial state, the transition under input i is not defined at the state (s,t). On the other hand, given a separating sequence i, if there exists an input sequence shorter than such that each state of the set successor(q₁, ) is a reduction of an appropriate state of the set successor(q₁, ), then i also separates the FSMs S and T, and thus, i is not a shortest separating sequence. Moreover, if is not the empty sequence and the set successor(q₁,) includes the initial state q₁ then i cannot be a shortest separating sequence, as the input i has to separate the initial states s₁ and t₁, and thus, i is a separating sequence of S and T. Based on the above observations, an algorithm is proposed that derives a shortest separating sequence of two separable FSMs (if such a sequence exists).

Algorithm 1 Deriving a Shortest Separating Sequence of Two Complete FSMs

Input: Complete FSMs S = S, I, O, h, s₁ and T = T, I, O, g, t₁

Output: A shortest separating sequence of FSMs S and T (if such a sequence exists)

Step 1. Derive the intersection S T. If the intersection is a complete FSM then the FSMs S and T are non-separable. END Algorithm 1.

Step 2. If the intersection S T is a partial FSM, then derive a truncated successor tree of the intersection S T. The root of this tree, which is at the 0^th level, is the initial state (s₁, t₁) of the intersection; the nodes of the tree are labeled with subsets of states of the intersection. Given already derived j tree levels, j 0, a non-leaf (intermediate) node of the j^th level labeled with a subset P of states of the intersection and an input i, there is an outgoing edge from this non-leaf node labeled with i to the node labeled with the subset of the i-successors of states of the subset P. A current node Current, at the k^th level, k 0, labeled with the subset P of states, is claimed as a leaf node if one of the following conditions holds:

Rule 1: There exists an input i such that each state of the set P has no i-successors in the intersection S T;

Rule 2: There exists a node at the j^th level, j < k, labeled with a subset R of states with the property: for each state (s',t') of R there exists a state (s,t) of P such that (s',t') (s,t).

Step 3. If none of the paths of the truncated tree derived at Step 2 is terminated using Rule 1 then FSMs S and T are non-separable. END Algorithm 1. Otherwise, if there is a leaf node, Leaf, labeled with the subset P of pairs of states such that for some input i, each pair of the set P has no i-successors, then a shortest sequence i where labels the path from the root of the tree to Leaf, is a shortest separating sequence of FSMs S and T.

Theorem 1. Given complete separable FSMs S and T over input alphabet I and output alphabet O, Algorithm 1 returns a shortest separating sequence of FSMs S and T.

Algorithm 1 can be used for deriving a separating sequence for two states s and s of a single FSM S = S, I, O, h, s₁. In this case, FSMs S, I, O, h, s and S, I, O, h, s are the input of the algorithm.

Proposition 1. Given two complete separable FSMs S and T, |S| = n and |T|= m, the length of a shortest separating sequence of S and T is at most 2^mn?1.

Proof: According to Algorithm 1, in the worst case, a path from the root to a leaf node Leaf, terminated using the termination Rule 1, contains each subset of states of the intersection except the initial state, since the set {q₁}, q₁ = (s₁, t₁), is at the 0^th level of the truncated successor tree. Therefore, the length of the path does not exceed 2^mn?1 - 1 and one more input is needed to separate states of the subset that labels the node Leaf, i.e., given two complete separable FSMs S and T, |S| = n and |T|= m, the length of a separating sequence of S and T is at most 2^mn?1.

In the following, the upper bound 2^mn?1 on length of a separating sequence is shown to be reachable. Given two integers n 1, m 1, the following algorithm, Algorithm 2, returns two complete separable FSMs S and T with n and m states which can be separated only with an input sequence of length 2^mn?1. The idea behind Algorithm 2 is close to that of deriving a Moore lock FSM where an (appropriate) input sequence traverses all the states of the FSM while all other sequences (except the prefixes of ) take the FSM to the initial state or traverse a loop. In our case, both machine S and T are nondeterministic, have 2^mn?1 inputs, and are derived in such a way that an appropriate input sequence of length 2^mn?1 - 1 when applied at the initial state of the intersection S T =Q, I, O, f, q₁, q₁ = (s₁, t₁), traverses all the non-empty subsets of the set Q\{q₁}. The last subset reached by the sequence contains a single state (s,t) where states s and t of machines S and T are separated with the tail 2^(mn?1)th input of the input sequence. Any other input sequence (except the prefixes of ) of length up to 2^(mn?1) -1 traverses a subset that contains the initial state of the intersection or traverses a superset of a set already traversed by a prefix of the input sequence and thus, is terminated according to Rule 2 of Algorithm 1 since there exists a node at the 0^th level labeled with the subset {q₁}.

Algorithm 2 Deriving Two FSMs S = S, I, O, h, s₁ and T = T, I, O, g, t₁, |S|= n and |T|=m, which can be separated only with an input sequence of length 2^mn?1

Input: The integers n and m, the state sets S and T, |S|= n and |T|=m, the input set I = {i₁, ..., i_k}, k = 2^mn?1 , and the output set O = {0, 1} Ч S Ч T

Output: Two complete FSMs S = S, I, O, h, s₁ and T = T, I, O, g, t₁, |S|= n and |T|=m, that can be separated only with an input sequence of length 2^mn?1

Step 1: Enumerate all non-empty subsets of the set S Ч T\{(s₁,t₁)}= {(s₁,t₂),..., (s_n,t_m)} in such a way that each subset M_k+1 has no more states than the subset M_k, k = 1, ..., 2^mn?1 - 1. The subset M₁ = S Ч T\{(s₁,t₁)} and subsets M_k, k = 2^mn?1 - mn, ..., 2^mn?1 -1, are singletons. The tail subset M_k, k = 2^mn?1 -1, is {(s_n,t_m)}.

Step 2: Build the transition relations h and g for both machines using the rules described below. Transitions with the inputs i₁ and i_k, k = 2^mn-1, are treated in a special way.

Transitions with the input i₁: Given an input i₁, the relation h has all transitions of the set {(s₁, i₁, (1,s,t), s): s S, t T, (s,t) (s₁,t₁)}, while the relation g has all transitions of the set {(t₁, i₁, (1,s,t), t): s S, t T, (s,t) (s₁,t₁)}. For each state s S\s₁ and t T\t₁, the relation h has transitions (s, i₁, (0,s₁,t₁), s₁) and (s, i₁, (1,s,t₁), s₁), while the relation g has transitions (t, i₁, (0,s₁,t₁), t₁) and (t, i₁, (1,s₁,t), t₁) .

Transitions with the input i_k, k = 2^mn?1: This input should separate states s_n and t_m; therefore, the relation h has the transition (s_n, i_k, (1,s₁,t₁), s₁), while the relation g has the transition (t_m, i_k, (0,s₁,t₁), t₁). For each state s S\s_n and t T\t_m, the relation h has transitions (s, i_k, (0,s₁,t₁), s₁) and (s, i_k, (1,s₁,t₁), s₁) while the relation g has transitions (t, i_k, (0,s₁,t₁), t₁) and (t, i_k, (1,s₁,t₁), t₁).

Transitions with an input i_k+1, 1 k 2^mn-1 - 2 : Given input i_k+1, 1 k 2^mn-1 - 2, transitions are added to the relations h and g based on the subsets M_k and M_k+1 derived by explicit enumeration of all non-empty subsets of the set S Ч T\{(s₁,t₁)}. For each state s S, if there exists state t T such that the pair (s,t) M_k, the relation h has all transitions of the set {(s, i_k+1, (1,s',t'), s'): (s',t') M_k+1}. If there exists state t T such that the pair (s,t) M_k, the relation h has all transitions of the set {(s, i_k+1, (0,s,t), s₁): (s,t) M_k}. In the same way, transitions of the FSM T under the input i_k+1 are derived. For each state t T, if there exists a state s S such that the pair (s,t) M_k, the relation g has all transitions of the set {(t, i_k+1, (1,s',t'), t'): (s',t') M_k+1}. If there exists a state s S such that the pair (s,t) M_k, the relation g has all transitions of the set {(t, i_k+1, (0,s,t), t₁): (s,t) M_k}.

In the following two propositions, some properties of the FSMs S and T returned by Algorithm 2 and of the intersection S T are established. Based on these properties Proposition 4 is provided that shows that S and T can only be separated with an input sequence of length 2^mn-1.

Proposition 2. Given FSMs S and T returned by Algorithm 2 and two different states (s,t) and (s',t') of the intersection S T, it holds that (s,t) ? (s',t') and (s',t') ? (s,t).

Proof: In order to prove Proposition 2, we consider the two possible cases: Case-1 where none of the states (s,t) and (s',t') is the initial state (s₁,t₁) of S T, and Case-2 where state (s,t) or state (s',t') is the initial state (s₁,t₁) of S T.

Case-1: Let (s, t) (s₁, t₁), (s', t') (s₁, t₁). In this case, there exists a subset M_k, k = 1, ..., 2^mn-1 - 2, that contains state (s,t) and does not contain state (s',t'). Therefore, by construction, (0,s',t') out((s',t'), i_k+1) and (0,s',t') out((s,t), i_k+1), i.e., the set of output responses at state (s',t') M_k to i_k+1 has (0,s',t') while the set of output responses at state (s,t) M_k to i_k+1 does not contain (0,s',t'). Thus, out((s',t'), i_k+1) is not a subset of out((s,t), i_k+1), i.e., (s',t') ?(s,t). Therefore, if (s,t) (s₁,t₁) and(s',t') (s₁,t₁), then (s',t') ? (s,t) and (s,t) ? (s',t').

Case-2: Let (s,t) (s₁,t₁) while (s',t') = (s₁,t₁). In this case, by construction, (0,s₁,t₁) out((s₁,t₁), i_k+1), while (0,s₁,t₁) out((s,t), i_k+1), k = 1, ..., 2^mn-1 - 2, i.e., there exists an input symbol i such that the set of output responses at state (s₁,t₁) to i includes (0,s₁,t₁) while the set of output responses at state (s,t) to i does not contain (0,s₁,t₁). Thus, out((s₁,t₁), i) is not a subset of out((s,t), i), i.e., (s₁,t₁) ? (s,t). Moreover, there exists a subset M_k, k = 1, ..., 2^mn-1 - 2, that does not contain state (s,t). Therefore, (0,s,t) out((s,t), i_k+1), while (0,s,t) out((s₁,t₁), i_k+1), i.e., the set of output responses at state (s,t) M_k to i_k+1 includes (0,s,t) while the set of output responses at state (s₁,t₁) to i_k+1 does not include (0,s,t). Thus, out((s,t), i_k+1) is not a subset of out((s₁,t₁), i_k+1), i.e., (s,t) ? (s₁,t₁).

Proposition 3. Given the intersection S T of FSMs S and T returned by Algorithm 2 and a subset M_j, j = 1, ..., 2^mn?1 - 2 it holds that: a) if p > j + 1 then the i_p-successor of M_j contains the initial state; b) if p = j + 1 then the i_p-successor of M_j equals M_j+1; c) if p < j + 1 then the i_p-successor of M_j contains the initial state or the subset M_p.

Proof:

(a): Let p > j + 1. Since p 1 > j, the subset M_p-1 has no more states than the subset M_j. Thus, there exists state (s,t) such that (s,t) M_j and (s,t)t M_p-1. By construction, given states s S and t T such that the pair (s,t) M_p-1, the relation h has a transition (s, i_p, (0,s,t), s₁) and the relation g has a transition (t, i_p, (0,s,t), t₁). Thus, in the intersection S T, there is transition from state (s,t) M_j to the initial state under input i_p. Therefore, the i_p-successor of M_j contains the initial state.

(b): Let p = j + 1. By construction, given states s S and t T such that the pair (s,t) M_j, the relation h contains all transitions of the set {(s, i_j+1, (1,s',t'), s'): (s', t') M_j+1}, while the relation g has all transitions of the set {(t, i _j+1, (1,s',t'), t'): (s', t') M_j+1}. Thus, the intersection S T has a transition from each state (s, t) M_j to each state (s', t') M_j+1 under input i_j+1. Therefore, the i_p-successor of M_j is M_j+1.

(c): Let p < j + 1. By construction, the i₁-successor of M_j is the initial state. Let p > 1. If M_j M_p-1 , then there exists state (s,t) such that (s,t) M_j and (s,t) M_p-1. By construction, given states s S and t T such that the pair (s,t) M_p-1, the relation h contains all transitions of the set {(s, i_p, (1,s',t'), s'): (s',t') M_p} while the relation g has all transitions of the set {(t, i_p, (1,s',t'), t'): (s',t') M_p}. Thus, the intersection S T has a transition from each state (s,t) M_p-1 to each state (s',t') M_p under input i_p. Therefore, if M_j M_p-1 , then the i_p-successor of M_j contains the subset M_p .

If M_j M_p-1 = , then there exists state (s,t) such that (s,t) M_j and (s,t) M_p-1. In this case, there is transition from state (s,t) M_j to the initial state under input i_p. Therefore, as it is shown in the proof of a), if M_j M_p-1 = then the i_p-successor of M_j contains the initial state.

Proposition 4. The length of a shortest separating sequence of FSMs S and T returned by Algorithm 2 equals 2^mn-1.

Proof. In order to prove Proposition 4, Algorithm 1 is applied for deriving a shortest separating sequence for the FSMs S and T returned by Algorithm 2, i.e., a truncated successor tree is derived for the intersection S T. The root of the tree that is at the 0^th level is the initial state (s₁,t₁) of the intersection. The i₁-successor of (s₁,t₁) is M₁ = S Ч T\s₁t₁. Each other i_j-successor of s₁t₁, j = 2, …,2^mn-1, contains the initial state (Proposition 3) and thus, there is the only intermediate node at the 1^st level labeled with M₁; the edge from the root to this node is labeled by the input sequence i₁.

By construction, each subset of the set S Ч T\{(s₁,t₁)} is reachable in the intersection from the initial state, and thus, the intersection is partial, since the transition under input i_k, k = 2^mn-1, is not defined at state (s_n,t_m). Moreover, according to Proposition 2, given two different states of the intersection S T, none of the states is a reduction of another state. Therefore, using Proposition 3 it can be shown by induction, that given j = 2, …, 2^mn-1 -1, at the j^th level there is the only non-leaf node labeled with the subset M_j, while all other nodes of the level are leaf nodes according to termination Rule 2. The path to the non-leaf node M_j at the j^th level is labeled with the input sequence i₁ i₂ ...i_j. Therefore, there exists the only non-leaf node of the truncated successor tree at the (2^mn?1-1)^th level labeled with the subset {s_nt_m} and the path from the root to this node is labeled by the input sequence i₁ i₂ ... i_k, k = 2^mn?1-1. According to Theorem 1, the sequence i₁ i₂ ... i_k-1 i_k, k = 2^mn?1, is a shortest separating sequence of FSMs S and T; the sequence has length 2^mn-1.

Propositions 1 to 4 imply the following theorem:

Theorem 2. Given two complete separable FSMs S and T, |S| = n and |T|= m, the length of a shortest separating sequence of S and T is at most 2^mn?1. Moreover, given integers n and m, n 1, m 1, there always exist separable FSMs S and T with n and m states which can be separated only with an input sequence of length 2^mn?1.

4. AN APPLICATION EXAMPLE

In this section, a simple application example of Algorithm 2 is given for deriving machines S = S, I, O, h, s₁ and T = T, I, O, g, t₁ with |S| = n = 2 and |T| = m = 2. Afterwards, a shortest separating sequence of S and T is generated using Algorithm 1; the length of this sequence equals 2^mn?1= 8.

Tables 1 and 2, shown below, represent the behavior relations of FSMs S and T. The state sets S = {a, b} and T = {1, 2}, the input set I = {i₁, ..., i_k}, k = 8, and the output set O = {0, 1} Ч S Ч T. The initial state of FSM S is a, the initial state of FSM T is 1. According to Proposition 4, the FSMs are separable and can be separated with an input sequence of length at least 2^mn?1 = 8. For the sake of simplicity, in this example, a state tuple (s,t) of S Ч T is represented as st.

According to Algorithm 2, first, all the non-empty subsets of the set S Ч T\ a1= {a2, b1, b2} are enumerated in such a way that each subset M_k+1 has no more states than the subset M_k, k = 1, ...,7. Subset M₁ = {a2, b1, b2}, while M₂ = {a2, b1}, M₃ = {a2, b2}, M₄ = {b1, b2}, M₅ = {a2}, M₆ = {b1}, M₇ = {b2}.

Given the input i₁, transitions (a, i₁, (1, a2), a), (a, i₁, (1, b1), b), (a, i₁, (1, b2), b), (b, i₁, (0, a1), a), and (b, i₁, (1, b1), a) are added to the relation h, while transitions (1, i₁, (1, b1), 1), (1, i₁, (1, a2), 2), (1, i₁, (1, b2), 2), (2, i₁, (0, a1), 1), and (2, i₁, (1, a2), 1) are added to the relation g.

Given the input i₂, transitions (a, i₂, (1, a2), a) and (a, i₂, (1, b1), b) are added to h since state a2 M₁ and M₂ = {a2, b1}, and transitions (b, i₂, (1, a2), a) and (b, i₂, (1, b1), b) are added to h since state b1 M₁ and M₂ = {a2, b1}. Transitions (1, i₂, (1, b1), 1), (1, i₂, (1, a2), 2) are added to g since state b1 M₁ and M₂ = {a2, b1}. Also, transitions (2, i₂, (1, b1), 1) and (2, i₂, (1, a2), 2) are added to the relation g since state a2 M₁ and M₂ = {a2, b1}. Moreover, the transition (a, i₂, (0, a1), a) is added to h while the transition (1, i₂, (0, a1), 1) is added to g since a1 M₁. Transitions under the inputs i₃, …, i₇ are derived in a similar way.

The input i₈ has to separate states b and 2; therefore, the transition (b, i₈, (1, a1), a) is added to the relation h, while the transition (2, i₈, (0, a1), 1) is added to the relation g. Transitions (a, i₈, (0, a1), a) and (a, i₈, (1, a1), a) are added to h and transitions (1, i₈, (0, a1), 1), (1, i₈, (1, a1), 1) are added to g.

Table 3 represents the behavior relation of the intersection S T. Algorithm 1 returns the tree given in Figure 1. Thus, a shortest input sequence that separates FSMs S and T is the sequence i₁ i₂ i₃ i₄ i₅ i₆ i₇ i₈ .

Table 1. FSM S Table 2. FSM T

Table 3. FSM S T

Figure 1. The truncated tree derived using Algorithm 1

5. EXPERIMENTAL EVALUATION

In this section, we experiment with Algorithm 1 for deriving a shortest separating sequence of two complete FSMs in order to determine how often a separating sequence exists, the effect of varying the number of nondeterministic transitions on the existence of a separating sequence, length of a separating sequence and how often the upper bound of a separating sequence is reachable.

The experiments are based on 490,000 pairs of randomly generated complete nondeterministic FSMs with varying number of states n = 2, 4, 6, 8, 10, inputs |I| = 2, 4, 6…14, outputs |O| = 2, 4, 6, …, 14. For each combination (n, |I|, |O|), an integer num is selected as 20, 40, 60, 80 or 100 percent of the product n |I|. Afterwards, for each combination (n, |I|, |O|, num) four groups each of 100 pairs (M₁, M₂) of machines, each with n states, |I| inputs and |O| outputs are derived. Each machine M₁ and M₂ in a pair of a group is derived in the following way:

Initially, a complete deterministic FSM with n states, |I| inputs and |O| outputs is randomly derived. Afterwards, nondeterministic transitions are added to the FSM as follows. First, num transitions are randomly selected. Then, for each selected transition (s,i), t different transitions with initial state s and input i are added to the FSM. The number t is calculated as y percent of the product n |O|, where y is an integer randomly selected within the selected interval R. An interval R of integers is selected as one of the ranges (0 to 20), (20 to 40), (40 to 60) or (60 to 80). For each derived pair of machines, Algorithm 1 is applied and a shortest sequence that separates the given pair is determined (if such a sequence exists). Table 4 contains a summary of a part of all conducted experiments, where for all pairs with a given n (Column I), num (Column II) and interval R (Column III), all experiments with varying |I| and |O| are considered. The percentage of how many of these pairs have a separating sequence is shown in Column V. The maximum length of a shortest separating sequence, MaxLen, of all experiments in a row is shown in Column IV.

Table 4. A selected part of conducted experiments

Figure 2. Existence of a separating sequences with respect to Num

According to the conducted experiments the existence of a separating sequence mainly depends on the values of Num and R and is almost independent of the size (i.e. number of states, inputs and outputs) of the machines. Moreover, MaxLen and thus, on average, length of separating sequences are less than mn. Figure 2 depicts the relationship between the existence of a separating sequence and the values of Num and the intervals R. For all conducted experiments the upper bound 2^mn-1 on the length of a separating sequence was never reached. It is worth noting that the generator used in the above experiments utilizes a random function when deriving transitions and it is interesting to study if similar results can be obtained when transitions are derived in another way; for example, if many transitions are derived in such a way that they take the machine to the initial state.

6. CONCLUSIONS

In this paper, an algorithm is proposed for deriving a shortest separating sequence of two complete FSMs (if such a sequence exists). Given arbitrary integers n and m, it is shown that there always exist FSMs S with n states and T with m states such that the length of a shortest separating sequence equals 2^mn-1. However, according to the conducted experiments there exists a large class of pairs of FSMs with n and m states such that the length of a shortest separating sequence of a pair is less than mn. The experiments also show that the existence of a separating sequence of two FSMs significantly depends on the number of nondeterministic transitions in these FSMs. The algorithm proposed in the paper can also be used for deriving a separating sequence for three or more FSMs. All the results obtained in this paper are applicable for partial FSMs, i.e., differently from the equivalence relation, the upper bounds on the length of a separating sequence for complete and partial FSMs coincide.

Acknowledgements

The authors would like to thank Dr. Martin R. Woodward and the anonymous reviewers for their helpful comments on improving this manuscript. Moreover, the authors would like to extend their gratitude to Goubieva Joulia at Tomsk State University for implementing and experimenting with the proposed algorithms.

References

1. G.v. Bochmann, and A. Petrenko. Protocol testing: review of methods and relevance for software testing. Proc. International Symposium on Software Testing and Analysis, Seattle, 1994: 109-123.

2. S.T. Chanson, A.A.F. Loureiro, and S.T. Vuong. On tools supporting the use of formal description techniques in protocol development. Computer Networks and ISDN Systems 1993: 25.

3. R. Dorofeeva, K. El-Fakih, S. Maag, A. R.Cavalli, and N. Yevtushenko. Experimental evaluation of FSM-based testing methods. Proc. of the IEEE International Conference on Software Engineering and Formal Methods (SEFM05), Germany, 2005: 23-32.

4. R. Lai. A survey of communication protocol testing. The Journal of Systems and Software 2002; 62: 21-46.

5. D. Lee and M. Yannakakis. Principles and methods of testing finite state machines-a survey. Proceedings of the IEEE, 1996; 84(8): 1090-1123.

6. H. AboElFotoh, O. Abou-Rabia, and H. Ural. A Test Generation Algorithm for Protocols Modeled as Non-Deterministic FSMs. The Software Eng. Journal 1993, 8(4):184-188.

7. H. Kloosterman. Test derivation from non-deterministic finite state machines. Proceedings of the IFIP Fifth International Workshop on Protocol Test Systems, Canada, 1993: 297-308.

8. P. Tripathy, K. Naik, Generattion of adaptive test cases from nondeterministic Finite State models. IFIP Trans. C: Commun. System C-11, 1993:309-320.

9. G. Luo, A. Petrenko, and G. Bochmann. Selecting test sequences for partially specified nondeterministic finite state machines. Proc. 7^th International Workshop on Protocol Test Systems, 1994.

10. G. Luo, G. Bochmann, and A. Petrenko. Test selection based on communicating non-deterministic finite-state machines using a generalized Wp-method. IEEE Transactions on Software Engineering 1994; 20(2):149-161.

11. R. Alur, C. Courcoubetis, and M. Yannakakis. Distinguishing tests for nondeterministic and probabilistic machines. Proc. the 27^th ACM Symposium on Theory of Computing, 1995:363-372.

12. A. Petrenko, N. Yevtushenko, and G. V. Bochmann. Testing deterministic implementations from their nondeterministic specifications. Proc. 9^th International Workshop on Protocol Test Systems, 1996; 125-140.

13. S.Yu. Boroday. Distinguishing Tests for Non-Deterministic Finite State Machines. Proc. IFIP TC6 11th International Workshop on Testing of Communicating Systems, 1998:101-107.

14. R. M. Hierons. Adaptive testing of a deterministic implementation against a nondeterministic finite state machine. The Computer Journal 1998; 41(5): 349-355.

15. I. Koufareva, N. Evtushenko, and A. Petrenko. Design of tests for nondeterministic machines with respect to reduction. Automatic Control and Computer Sciences, USA, 1998; 3.

16. R.M. Hierons. Using candidates to test a deterministic implementation against a non-deterministic finite state machine, The Computer Journal 2003; 46(3):307-318.

17. R.M. Hierons. Testing from a non-deterministic finite state machine using adaptive state counting. IEEE Transactions on Computers 2004; 53(10):1330-1342.

18. R.M. Hierons and H. Ural. Concerning the ordering of adaptive test sequences, Proc. 23rd IFIP International Conference on Formal Techniques for Networked and Distributed Systems (Lecture Notes in Computer Science, vol. 2767), Springer, 2003:289-302.

19. I. Hwang, T. Kim, S. Hong, and J. Lee. Test selection for a nondeterministic FSM. Computer Communications 2001; 24:1213-1223.

20. F. Zhang and T. Cheung, Optimal transfer trees and distinguishing trees for testing observable nondeterministic finite-state machines. IEEE Transactions on Software Engineering 2003; 29(1):1-14.

21. A. Petrenko, and N. Yevtushenko. Conformance tests as checking experiments for partial nondeterministic FSM. Proc. 5th International Workshop on Formal Approaches to Testing of Software (FATES 2005), 2005.

22. R. Miller, D. Chen, D. Lee, R. Hao. Coping with nondeterminism in network protocol testing. In Proceedings of the 17th IFIP International Conference on Testing of Communicating Systems, USA, 2005.

23. A.S. Tanenbaum, Computer Networks. Prentice-Hall, NJ, 1996.

24. A. Petrenko, N. Yevtushenko. Testing from partial deterministic FSM specifications. IEEE Trans. on Computers 2005; 54(9):1154-1165.

25. R. Milner. A Calculus of Communicating Systems. Lecture Notes in Computer Science, 1980; vol 92.

26. N. Spitsyna, V. Trenkaev, K. El-Fakih, N. Yevtushenko. FSM interoperability testing, Work In Progress: 23rd International Conference on Formal Techniques for Networked and Distributed Systems, 2003.

27. N. Spitsyna. FSM-based test suite derivation strategies for discrete event systems. Ph.D. Thesis, Tomsk State University, 2005: 1-158.

28. P. Starke, Abstract automata, American Elsevier, 1972: 3-419.