Journal of Software Engineering and Applications, 2013, 6, 500-510
http://dx.doi.org/10.4236/jsea.2013.69060 Published Online September 2013 (http://www.scirp.org/journal/jsea)
Test Selection on Extended Finite State Machines with
Provable Guarantees
Bo Guo, Mahadevan Subramaniam
Department of Computer Science, University of Nebraska Omaha, Omaha, USA.
Received July 22nd, 2013; revised August 21st, 2013; accepted August 29th, 2013
Copyright © 2013 Bo Guo, Mahadevan Subramaniam. This is an open access article distributed under the Creative Commons Attri-
bution License, which permits unrestricted use, distribution, and reproduction in any medium, provided the original work is properly
cited.
ABSTRACT
Building high confidence regression test suites to validate new system versions is a challenging problem. A model-
based approach to build a regression test suite from a given test suite is described. The generated test suite includes
every test that will traverse a change performed to produce the new version, and consists of only such tests to reduce the
testing costs. Finite state machines extended with typed variables (EFSMs) are used to model systems and system
changes are mapped to EFSM transition changes adding/deleting/replacing EFSM transitions and states. Tests are a
sequence of input and expected output messages with concrete parameter values over the supported data types. An in-
variant is formulated to characterize tests whose runtime behavior can be accurately predicted by analyzing their de-
scriptions along with the model. Incremental procedures to efficiently evaluate the invariant and to select tests for re-
gression are developed. Overlaps among the test descriptions are exploited to extend the approach to simultaneously
select multiple tests to reduce the test selection costs. Effectiveness of the approach is demonstrated by applying it to
several protocols, Web services, and model programs extracted from a popular testing benchmark. Our experimental
results show that the proposed approach is economical for regression test selection in all these examples. For all these
examples, the proposed approach is able to identify all tests exercising changes more efficiently than brute-force sym-
bolic evaluation.
Keywords: Formal Methods; Model-Based Software Testing; Regression Testing; Extended Finite State Machines
1. Introduction
Maintenance and evolution of complex systems is a
challenging problem since all the modifications made to
obtain a new system version must be thoroughly tested to
gain confidence that the new system functions correctly.
Usually, this requires users to select tests that exercise the
changes from the original test suite, evaluate the adequacy
of selected tests, and possibly design new tests. This is a
time consuming and error prone activity.
Usually, regression test suites are built by selecting
relevant tests from an available test suite. Automatically
identifying relevant tests from a test suite to validate the
new system version is called the regression test selection
problem. This is an active area of research with several
earlier works involving software programs ([1-3] are
excellent surveys) as well as executable system models [4,
5], which use finite state machines extended with vari-
ables (EFSMs). All of these works require the test traces
on original versions to be maintained to select tests, which
can be impractical for real systems using large test suites.
The methods also tend to be safe, leading to the selection
of many irrelevant tests that can increase the regression
test costs.
In this paper we present a model-based approach for
building regression test suites consisting of all and only
the relevant tests and without using any additional in-
formation about prior test executions. Such an approach
has the potential to reduce the maintenance overheads
across versions and regression costs due to more compact
test suites while increasing tester confidence due to the
absence of irrelevant tests. We consider EFSMs whose
variables range over a rich set of commonly used data
types. System tests are derived from EFSM tests, which
are a sequence of input and expected output messages
with concrete parameter values over the supported data
types. System changes are mapped to EFSM state and
transition changes that add/delete/replace one or more
EFSM transitions.

Test Selection on Extended Finite State Machines with Provable Guarantees 501
Given a change, and a test suite, the proposed approach
automatically analyzes each test description to a priori
determine the transitions that will be executed when the
test is run on the EFSM. We formulate an invariant for
each test that describes all the plausible EFSM execution
paths that the test can potentially take when it is run on the
EFSM. If the invariant is satisfiable, the transitions in the
corresponding path are guaranteed to be executed by the
test when it is run. The invariant for a test is automatically
built using the transitions (and their post-images) match-
ing the test description. Informally, a transition is a match
for a test description if it can process some test input in the
description. A theorem prover is used in a push-button
way to determine if the invariant is satisfiable and identi-
fies the associated transitions.
Often, several tests in the given test suite have over-
lapping descriptions. For instance, it is typical for tests to
use the same inputs to bring an EFSM to a common state
and then exercise other specific behaviors. Such tests as
well as others can be selected simultaneously whenever a
given change matches these tests at the overlapping por-
tions of their descriptions. To enable analysis of a group of
tests, a test suite is organized into a test forest whose each
tree represents a group of tests with overlapping descrip-
tions. We describe a procedure to simultaneously select
and discard groups of tests. Such a procedure alleviates
regression test selection costs in many cases.
The proposed approach has been implemented and ap-
plied to several EFSM models representing protocols, web
services, and other applications with encouraging results.
Our experimental results show that the proposed approach
is economical for regression test selection in all these
examples. For all the examples, the proposed approach
selects every test that exercises a change while discarding
all their relevant tests. Our experiments use a powerful
theorem prover called Simplify [6] extended with rewrite
rules [7].
Overview of the approach using a simple example fol-
lows next. Section 2 gives a brief overview of EFSM
model. EFSM changes, tests, and change exercising tests
are described in Section 3. In Section 4, we describe the
formulation of invariant based on test descriptions. Sec-
tion 5 describes incremental procedures for selecting tests
exercising changes and identifying unusable tests. Section
6 extends the approach to handle multiple tests. Section 7
describes related work. Section 8 describes our experi-
ments and Section 9 concludes the paper.
Simple Example: Consider a bank web service EFSM
depicted in Figure 1(a) whose transitions are given in
Figure 2. Users start by opening an account with a cash
amount greater than or equal to a minimum balance
amount (min), and are given a unique number as account
id. The current balance in each account is represented by
an array B[] mapping the account id to a non-negative
(a)
(b)
Figure 1. Bank web service EFSM and tests.
Figure 2. Bank web service transitions.
number. Users operate the account by performing deposits
and withdrawals. Withdrawals exceeding the current
balance are ignored. That leading to a balance lesser than
the min value results in a state where withdrawals are
ignored and a deposit that brings the balance above the
min value is only allowed. Accounts accrue a bonus that
doubles the current balance provided a specified maxi-
mum max number of withdrawals (that are not ignored)

Test Selection on Extended Finite State Machines with Provable Guarantees 502
and deposits succeed in maintaining a balance greater than
or equal to the min value. The bonus amount is transferred
incrementally to the account and no operations are proc-
essed during this period. The solid arcs in Figure 1(a) are
external transitions that can be observed by their mes-
sages. Others (dashed arcs in Figure 1(a)) are internal
transitions.
A test suite used to validate the EFSM is given in
Figure 1(b). Each test starts the EFSM in the state with id
= 0; min = 50; max = 2; (Timer) T1 = max; bonus = 0.
Now, suppose that we delete transition t12 and add
transition t'12 to allow withdrawals when the balance is
below min but is non-negative. Usually, tests in the
original test suite that are will execute (or executed) the
added (or deleted) transition are said to exercise the
change and selected for regression. Test λ1 is not selected
because it does not exercise the change whereas tests λ2
and λ3 are selected because they exercise the change.
The descriptions of these tests can be automatically
analyzed to accurately predict whether they will exercise
the change when run. So these tests can be selected and/or
discarded without running them. The proposed approach
develops procedures that analyze test descriptions to se-
lect and discard tests to build a high confidence regression
test suite.
2. Preliminaries
This section is mostly derived from earlier works [7-11],
where more details can be found.
Extended Finite State Machines: An EFSM E = (I, O,
S, V, T) [9], is a 5-tuple where I, O, S, V , and T are finite
sets of parameterized input and output messages, states,
variables, and transitions respectively. Each message in I
and O has a finite number of parameters; finite set of
variables, V = X ∪ {IQ, OQ}, is the union of the set of
data variables X and two message queue variables IQ and
OQ denoting the input and output queues from and to the
environment respectively. A transition, t: im(p[]), Pt, st→
qt, om(e[]), At, where p[] = p1, …, pn are distinct, typed
parameter variables, Pt is the guard, At is an ordered se-
quence of assignments, and e[] = e1, …, ew is a list of
expressions over V and parameters p[]. Transitions hav-
ing an input and an output message are called external
transitions; others are internal transitions.
The global state of an EFSM consists of a state from S
and a set of constraints over variables. The state is con-
crete if each variable is constrained to a constant value.
A state is initial, if the constraints satisfy the initial con-
ditions of the system. A transition is enabled in a system
global state if the message in the global state is an in-
stance of the input message of the transition and the
global state satisfies the guard of the transition. Execu-
tion step, g → tg′, transitions from global state g to g′
using t enabled in g. A run is a sequence of consecutive
steps starting and ending in initial global states.
The most general po st-image of a transition t, Mgpos
(t), is a global state representing all the concrete global
states that can result after executing the transition t. The
concrete post-image of transition t from a global state g,
Cpos(t, g), is the concrete global state produced by exe-
cuting transition t in the global state g. If t is not enabled
in g then Cp os (t, g) has the value false. Concrete post-
images to deal with the dynamic behavior of tests. We
relate the static and the dynamic behaviors of a transi-
tion by relating their most-general and concrete post-
images with respect to a concrete a global state as: Cpos
(t, g) = Mgpos(t) ∧ g.
3. EFSM Changes and Tests
3.1. Changes
Changes to the EFSM are specified at the transition level.
An addition change, δ = <+, ta>, adds a new external
transition ta to an EFSM. A deletion change, δ = <−, td>,
deletes an existing external transition td from an EFSM.
A replacement change, δ = <−/+, (td, ta) >, replaces an
existing external transition td in an EFSM by a new ex-
ternal transition ta. Certain transition changes may have
larger impacts and can modify the EFSM interface itself.
For instance, an addition change can introduce new
EFSM messages and states. Similarly, a deletion change
can result in the removal of existing messages and states.
Other EFSM changes such as addition or deletion of
states and/or variables can all be expressed in terms of
changes to the transitions. All the EFSM changes are
assumed to produce a new EFSM that is deterministic
and consistent.
3.2. EFSM Tests
An EFSM test, λ = <g0, [i1/o1, …,in/on]>, is a pair, whose
first component is a concrete global state g0 and the sec-
ond component is a finite sequence of test elements of
the form: test input/expected test output. Each input (and
output) is a sequence of assignments to the message
queue and/or data variables. Only constants appear in an
input. Both constants and data variables can appear in an
output. For brevity, our test inputs and outputs only refer
to the messages (queues are implicit) and not to the data
variables.
Example: The EFSM tests for the bank example are
depicted in Figure 1(b). Test inputs of all these tests as-
sign a single message having constant parameter values
to the input message queue and expected outputs assign
constant values and variables to the output message
queue.
Now, we extend EFSM executions to handle test inputs.
A test input extended concrete global state of EFSM
is a global state of the EFSM in which the message pa-

Test Selection on Extended Finite State Machines with Provable Guarantees 503
rameters are bound to the constant values specified by
the test input. Transition t processes the test input i in the
concrete global state g if the transition t is enabled in the
extended concrete global state gi.
Test λ is applied to EFSM E by starting E in concrete
global state g0. Transition t0 enabled in g0 is executed to
generate concrete global state, say, g1, and the process
repeated until no more transitions are enabled in the last
generated concrete global state, say, gm. Extend gm with
the first test input i1 and execute the enabled transition tm
to generate the state gm+1. Transition enabled in gm+1 is
executed to produce the next state and the process is re-
peated. The process terminates on either reaching the
initial concrete global state after processing all test inputs
or if no progress can be made.
4. Structural Test Invariant
Transitions matching test inputs and sequences of sets of
transitions matching a test description are described. Test
extended most general pre- and post-images are then
defined and used to formulate the invariant for tests.
4.1. Matching Transitions and Sequences
Definition: A transition matches a test input if 1) the test
input is an instance of the input message of the transition
and 2) the instantiated transition guard is satisfiable.
Example: In Figure 2, t5 matches the input wdraw
(1,110) of test λ2 since wdraw(1,100) is an instance of
wdraw(i, v) with i = 1, and v = 110, and the instantiated
guard of t5: (1 == id) ∧ (110 >0) ∧ 0 <= (B[1] - 110) ∧
(B[1] - 110) < min ∧ (T1 >0), is a satisfiable formula. 
The match operation only checks the input message
and the guard but ignores the input state of the transition.
Hence the operation is conservative i.e., a transition may
match a test input but may not able to process that input
when the test is actually applied. However, as shown
below, the operation will include all the transitions that
can process the test input.
Several EFSM transitions can match a test input. Let
T(ik) be the (possibly empty) set of all transitions match-
ing the test input ik. A matching sequence, ϕ(λ) =
[T(i1), …, T(in)], of a test λ is a sequence of sets of transi-
tions constructed by point-wise matching of the inputs of
the test λ. A transition sequence, ρ = [t1, …, tn]
∈ ϕ(λ) if
each tk ∈ T(ik), k = 1n.
Example: Matching sequence ϕ(λ2) = [{t1}, {t2, t6}, {t3, t4,
t5, t12}, {t3, t4, t5, t12}, {t7, t8}] for the test λ2 in Figure 1(b).
A transition sequence of ϕ(λ2) is ρ = [t1, t2, t3, t3, t7]. 
4.2. Deriving Invariant from a Test Description
Recall from Section 2 that the most general post-image,
of a transition tw, Mgpos(tw),is a global state representing
all the concrete global states that can result after execut-
ing the transition. The most general pre-image of tran-
sition tw, Mgpre(tw), is a global state representing all the
concrete global states in which the transition is enabled.
Let the transition tw match the test input iw. The test
extended most general post-image of tw with respect to
input iw, denoted as Emgpos(tw), is the set of all global
states that can be produced by executing transition tw
instantiated with input iw. Emgpos(tw) = false (empty set
of global states) if tw does not match iw.
The test extended most general pre-image of tw with
respect to input iw, denoted as Emgpre(tw), is the set of all
global states where transition tw instantiated with input iw
is enabled. Emgpre(tw) = false, if tw does not match iw.
A structural invariant for a test λ = <g0, [i1/o1, …,
in/on]>, can be formulated using test description and test
extended post-images of the matching transitions as:
() ()
0
() 1
Init(Emgpos ,
k
n
kn
g
t
ρφλ
ψλ
∈=
=∨ ∧∧
where the predicate Init checks if its argument is an ini-
tial global state and ρ is the transition sequence [t1, …, tn].
Each disjunct of ψ(λ) corresponds to a transition se-
quence ρ from the matching sequence ϕ(λ) and is made of
n + 1 conjunctions. First conjunct is the concrete global
state g0 in which the test λ starts and the remaining n
conjuncts are the test extended post-images of the n tran-
sitions in ρ.
The invariant ψ(λ) simply checks that the matching
sequence ϕ(λ) contains at least one feasible run from the
concrete global state g0 in which the test λ is applied.
Each disjunct in ψ(λ) considers a transition sequence
from the matching sequence and incrementally checks its
feasibility. The transition sequence is a feasible run if the
disjunct is satisfiable. Since EFSMs are deterministic,
each test has at most one test run and therefore, at most
one of the disjuncts is satisfiable. Hence the invariant is
satisfiable if and only if the test run consists of the transi-
tions appearing in the corresponding disjunct. Therefore,
all the transitions that will appear in a test run can be
accurately predicted (without running the test) if the in-
variant of the test is satisfied.
An efficient approach to check the satisfiability of the
invariant employs a directed transition control graph
TCG(λ) consisting of transitions belonging to the match-
ing sequence ϕ(λ). The graph has a special start node and
one node for each occurrence of each transition in the
matching sequence ϕ(λ). Node twj denotes the occurrence
of transition twin the jth matching set T(ij) in ϕ(λ). TCG(λ)
is a levelized graph with level 0 having the start node
and level k, k ≥ 1, consisting of nodes representing all
transitions in matching set T(ik).
Edges in the graph connect a node in a level to zero or
more nodes in the next level. Edges can have a label s

Test Selection on Extended Finite State Machines with Provable Guarantees 504
(single successor) or a label c (a potential successor). Let
tv and tw be nodes at levels k and k +1 respectively. Edge
(tvk, tw(k+1), s) belongs to the graph if the transition tw
must follow tv in all runs. Otherwise, the edge (tvk,
tw(k+1), c) belongs to the graph. An edge from start toa
node tw1 with label s is added if tw is enabled in the ini-
tial state g0.
Example: The Figure 3 depicts the transition control
graph TCG(λ2) for the test λ2. 
The procedure to check the invariant is described in
Figure 4. It takes a test λ and the graph TCG(λ) as inputs
and outputs Success if the transitions executed by the test
can be accurately predicted and Fail otherwise. The
graph is traversed level by level starting at the level 0 to
see if any path in the graph forms a feasible run from the
concrete global state g0. At each level, a node is marked
by the procedure if the sequence of transitions in the path
from the start node to the marked node in the graph
forms a feasible path from the concrete state g0of the test
λ. A label, L(tk), is associated with the marked node tk in
each level k. Let ρ = [t1, …,tw] be the transition sequence
that forms a feasible path from g0 when the procedure
reaches the current level (clevel in Figure 4). The label
associated with a node tk belonging to the sequence ρ is
L(tk) = g0 ∧ Emgpos(t1) ∧ …∧ Emgpos(tk−1).
To extend the feasible path to the w + 1thlevel, first, the
candidate immediate successor nodes of the marked node
at the current level are identified. If the marked node
corresponding to tw has an immediate successor linked by
Figure 3. TCG for λ2.
Figure 4. Check procedure.
an s edge, then this is the only candidate immediate suc-
cessor. In this case, the other immediate successors of the
node corresponding to tw, if any, are deleted from the
graph. Deleting these edges from the graph may make
certain nodes dangling i.e., nodes that do not have any
successor and/or a predecessor. Such nodes cannot par-
ticipate in the feasible run, if any, and hence are deleted
from the graph along with the resulting dangling edges.
Such deletion of dangling nodes and edges is repeated
until no more such nodes and edges remain. If the
marked node corresponding to tw has no immediate suc-
cess or linked by an s edge, then all the nodes are candi-
date immediate successors.
Then, we propagate the label L(tw) to each of the can-
didate immediate successors tw+1 and compute a formula
F = (L(tw) ∧ Emgpos(tw))
⇒ Emgpre(tw+1). The formula F
states that processing the test input w using transition twin
the concrete global state g0 ∧ Emgpos(t1) ∧ …∧
Emgpos(tw−1) will result in a concrete global state in
which the immediate successor transition tw+1 processing
the test input iw+1 is enabled. If F is valid then that im-
mediate successor node is marked and the label L(tw+1) is
set. The current level is incremented and the procedure is
continued. If the propagated formula F is not valid for

Test Selection on Extended Finite State Machines with Provable Guarantees 505
any of the candidate successors then this implies that no
transition in the matching set T(iw+1) can process the test
input iw+1 in the concrete global state obtained after
processing the first w test inputs. And, the procedure fails.
If the path can be extended up to the last level (level n) of
the graph and the L(tn) ∧ Emgpos(tn) is an initial concrete
global state then the procedure returns Success. Other-
wise, the procedure returns Fail.
5. Selecting Tests
The model-based regression test selection problem using
the EFSMs is analogous to that for programs [10]. It
takes as inputs–a deterministic, consistent EFSM E1 with
a test suite T, and a change δ that produces a modified,
deterministic and consistent EFSM E2. It outputs a test
suite T′ ∧ T, consisting of subset of tests of T guaranteed
to exercise the change δ on E2.
Test λ = <g0, [i1/o1, …, in/on]> exercises an addition
change δ = <+, ta> on E2 if there exists a feasible path ρ =
[t1, …, ta] from g0 on E2. Test λ exercises a deletion
change δ = <−, td> on E2 if there exists a feasible path ρ
= [t1, …,td] from g0 on E1. Test λ exercises a replacement
change, δ = <−/+, (td, ta)> on E2 if it either exercises the
addition change <+, ta> on E2 or it exercises the deletion
change <−, td> on E2.
For test selection, we slightly generalize the satisfi-
ability of the invariant. Let λ be any test for an EFSM E.
Definition: Let ρ = [t1, …,tk] be a transition sequence
obtained from a path: start → t1→ …→ tk of TCG(λ).
The invariant ψ(λ) is k-satisfiable if ρ is a feasible path
over E for the test λ.
5.1. Selecting Tests for Addition Changes
The main steps of an incremental procedure to determine
if the test λ is a candidate for an addition change δ are
given below. The procedure takes the original model E1,
the matching sequence, the graph TCG(λ), and the added
transition ta as its inputs and returns 1 if λ is a candidate
test for δ and returns 0 otherwise. It also outputs the up-
dated compatibility graph to be used for future changes.
1) Update the original matching sequence ϕ(λ) by
adding ta to the appropriate matching sets.
2) Suppose that ta occurs exactly once in the kth set of
ϕ(λ). Check if ψ(λ) is k-satisfiable on E1using the original
graph TCG(λ). If so then not ta, but some original transi-
tion, will process the kth test input on new EFSM E2. If
ψ(λ) is only(k − 1)-satisfiable, let F = (L(tk−1) ∧ Emgpos
(tk−1)) ⇒ Emgpre(ta), where tk−1 is the node marked at
level k − 1. If F is not a valid, ta will not process the kth
input on E2 (this is also the case when ψ(λ) is satisfiable
to a level less than k − 1). So, λ is not a candidate; the
graph is unchanged.
If ψ(λ) is (k – 1)-satisfiable, but not k-satisfiable and F
is a valid then λ is a candidate and the transition ta will
process the kth input on E2. Update TCG(λ) by adding
node ta at level k and edge (tk−1, ta, s). Attempt to extend
the feasible path to level k + 1 using the procedure de-
scribed in Figure 4, using the updated graph. If success-
ful and tk+1 is the marked, add edge, (ta, tk+1, s), to the
updated graph and output the resulting graph.
3) If ta occurs in many sets of sequence ϕ(λ), all in the
interval [l, m] and ψ(λ) is satisfiable up to level m or
higher, then λ is not a candidate and the graph is un-
changed. Otherwise, process each level in the interval,
starting at level l, as described above. Go to next level
only if ta will not process inputs at the previous levels.
4) Finally, if ta does not occur in sequence ϕ(λ), the
test λ is not a candidate and the graph is unchanged.
The above incremental procedure uses the original
graph to identify candidate tests. The graph is locally
updated so that they can be similarly used in selecting
tests for future changes. Such an incremental procedure
can be effective in practice since it is bounded by the size
of the matching sequence elements affected by the
change and is independent of the overall size of the
EFSM. Further, focusing on the earliest occurrence of
change transition can reduce the analysis time, especially
for long tests.
5.2. Selecting Tests for Deletion Changes
The main steps of the procedure are similar to those of
the procedure for the addition change described above.
The only difference is in the updating of the compatibil-
ity graph. While handling a deletion change, if a node
corresponding to transition td in the graph is marked by
the invariant checking procedure run on E1, the corre-
sponding test is selected. In this case, the updated graph
is obtained by deleting every node and the resulting dan-
gling edges from the graph corresponding to transition td.
The process is repeated with all the nodes that do not
have an immediate predecessor or an immediate succes-
sor until no more such nodes can be found and the re-
sulting graph is returned as the updated graph.
Replacement changes are viewed as a pair of addition
and deletion changes. Tests are selected if they are cho-
sen for either.
6. Simultaneous Test Selection
Often, several tests in the given test suite start in the
same concrete global state and have overlapping test in-
puts. For instance, it is typical for tests to use the same
inputs to bring the EFSM to a common state and then
exercise other specific behaviors. Such tests can be se-
lected simultaneously whenever a change matches these
tests at the overlapping portions of their test inputs. To
simultaneously select and discard tests, the test suite T =

Test Selection on Extended Finite State Machines with Provable Guarantees 506
{λ1, …, λn} of the original EFSM E1 is partitioned into
groups of tests. Each group G = {λ1, …, λk} ⊆ T consists
of tests that are applied in the same concrete global state
g0 and share a non-empty prefix of their test inputs, i.e.,
they have at least the same first test input.
Each group G is represented using a test suite tree
(TST). Each node of the TST tree denotes a test input
occurring at a particular position in the non-empty prefix
of the test inputs of the tests in G. The root node of TST
denotes test input of the tests in G occurring at the first
position of the prefix. Node v is a child of node u in TST
if in some test in G, the test input iu at a position p in the
prefix is an immediate predecessor of the test input iv at
position p + 1. The edge between a parent node u and
child node v is labeled by the set consisting of all tests
where this is the case. Further, the set of tests labeling an
edge between a parent and a child node is the union of all
tests appearing in the subtree rooted at the child node.
Example: TST in Figure 5 represents the test suite of
Figure 1(b).
Below, we describe a procedure to simultaneously se-
lect and discard tests from T to build a test suite T′ for the
new EFSM E2 for addition change δ = ⟨+, ta⟩.
Consider a TST comprised of a group of tests G all
starting in the concrete global state g0. To select tests
from this TST, for each node u, the set of transitions of
the EFSM E2 matching the test input iu, T(iu), is com-
puted. Each matching set T(u) of the node u is main-
tained at that node. If ta does not appear in any matching
sets, none of the tests in the TST are chosen.
Suppose that ta appears in some matching set T(iu) at
node u of the TST. Let the sequence of matching sets
from the root node of the TST to the node u be the
matching sequence α = [T(i1), …, T(in), T(iu)]. We build a
control graph using the transitions appearing in α and use
Figure 5. TST for bank example.
the procedure in Figure 4 with the graph and g0 as its
inputs to determine if some transition sequence belong-
ing to α forms a feasible path from g0 on E2. If the pro-
cedure returns Success and transition ta is the transition
marked by the procedure in the matching set T(iu), all
tests labeling the edge between in and iu in the TST are
chosen. Node iu and its descendants are removed.
If the procedure returns Fail because only a prefix of
the matching sequence α, say, [T(i1), …, T(im)] contains a
feasible path then the TST is updated by setting the sets
T(i1), …, T(im) to the respective transitions marked by the
procedure. The subtree of TST rooted at the node im+1 is
removed (all tests in this subtree are discarded since they
do not exercise the addition change).
The procedure can also return Success but ta may not
be the marked transition in the matching set T(iu). In this
case, we update the matching sets with the transitions
marked by the procedure to incrementally continue ana-
lyzing the extensions of the matching sequence α reach-
ing other nodes of the TST whose sets include ta.
The left-right traversal of the updated TST (and the
test suite T) is continued until all nodes in the TST whose
sets contain ta have been analyzed. All the tests chosen in
are included in T′ and the same process is repeated with
each TST. Procedures to select multiple tests for deletion
and replacement changes are similar.
Example: The matching nodes u for the bank example
are highlighted in Figure 5. A left-to-right traversal of
this tree selects tests λ2, λ3 at level 4 after which the
nodes at the lower levels can be removed.

7. Related Work
Approaches for regression testing have been broadly
classified as being code-based or model-based. Yoo and
Harman [3] is a recent survey on regression test selection
and related problems. Rothermal and Harrold [2] and
Harrold and Orso [1] are two other surveys emphasizing
code-based approaches.
Code-Based Approaches: Code-based approaches
work on Programs and have been extensively studied
earlier. The above surveys discuss many of these ap-
proaches in detail. Most of these approaches perform
control and data flow analysis to determine the difference
between original and modified programs and use avail-
able test traces to determine if the test should be selected
for regression. However, these methods are conservative
do not target precise selection of tests [12]. On the other
hand, precisely selecting tests is a primary goal of this
paper, which is crucial for high-confidence test suites.
Model-Based Approaches: Model-based approaches
use executable models and model-programs instead of
actual code to select regression tests. Recently, there has
been a lot of interest in this area due to the advent of
embedded systems such as automobiles [13] and com-

Test Selection on Extended Finite State Machines with Provable Guarantees 507
plex component based systems [14], where early testing
of models can alleviate the validation costs of actual sys-
tems. Earlier works on model-based regression testing
include works by Briand et al. [15,16] using UML mod-
els and that by Korel et al. [5,17,18] using EFSM models.
The approach described in [15,16] extracts changes by
comparing two versions of a class, use case/sequence
diagrams in a UML design. These changes are then used
to classify a test as obsolete, retestable, re-usable by
mapping a test to a complete message sequence in a se-
quence diagram. Earlier works using EFSMs have fo-
cused on regression test minimization, and prioritization
problems, unlike test selection considered in this paper.
The proposed approach differs from the above model-
based approaches in its focus on constructing accurate
regression test suites based on models. Unlike the earlier
approaches, in the proposed approach no test exercising a
change in the EFSM is missed and every test that does
not exercise any change in the EFSM is selected. Second,
our EFSM models and the analysis procedures handle a
rich set of data types and allow test cases to have con-
stant values involving all these data types including ag-
gregate data types. Finally, the proposed approach ex-
ploits the overlap in test descriptions to simultaneously
select or discard tests for building a regression test suite.
8. Experiments
We refer to the proposed approach as SPG (selection
with provable guarantees) in this section. We have im-
plemented SPG and applied it several web services, pro-
tocols, as well as many model programs taken from a
well-known testing benchmark [19]. Our objectives for
these experiments are: study the efficiency of SPG for
regression test selection for EFSMs. Our prototype is
coded in Perl and C on a Linux server with 4GB memory
and employs built-in graph libraries. It uses the reasoning
framework, SAIL, implemented based on the theorem
prover Simplify [6] extended with queues [11].
Change and Test Generation: We use the changes
provided by the applications whenever they are available.
In addition, changes are synthetically generated using the
following simple process. Given an EFSM model (text
files), the number of transitions to be changed, and the
overall number of mutated EFSMs, the input EFSM is
first compiled into a graph. A new graph corresponding to
each new EFSM is got from the original graph by marking
the number of transitions given as input with the change
actions a (addition) or d (deletion), chosen randomly. The
process is repeated to generate the new EFSMs.
The test suite for the original EFSM is hand crafted
wherever possible, such as those for model programs from
[19]. Tests were also automatically generated using the
model-based test generator ParTeg [20].
8.1. Case Studies
We have applied the prototype to ten examples from the
literature: completion (Cmp), two-phase commit (Tcp),
and conference (Cnf), and third-party call (Thp), Cruise
Control (Con), Printtokens (Pri)2, automatic teller ma-
chine (Atm) [4,5], bank (Bnk),vending machine (Ven), and
a Microwave oven (Mic) [21]. The completion, two-phase
commit, and conference protocols described on the
web-site3 have been used earlier to evaluate formal testing
approaches. The completion protocol Cmp is used by an
application to tell the coordinator to try, commit, or abort
an atomic transaction. Two-phase commit Tcp is a coor-
dination protocol that defines how participants reach an
agreement on the outcome of an atomic transaction.
The conference protocol, Cnf, is a chatbox-like protocol.
The EFSM models for Cmp and Tcp were manually cre-
ated using their graphical and textual descriptions and
contain 7 and 14 transitions respectively. Their test suites
have 300 and 800 tests respectively. For the Cnf protocol,
we used the EFSM description (c) available from the
website referred above. This model has 19 transitions and
the test suite has 723 tests. The website gives two EFSMs
called (c) and (d) and describes four changes to transform
EFSM (c) to EFSM (d). The four changes specified there
are all additions that allow members to send data before
joining the conference. The third-party call (Thp) is a
protocol from Praxis with 15 transitions and 837 tests
[22].
Cruise Control (Con) and Printtokens (Pri) are pro-
grams from the popular test benchmark [19]. These pro-
grams are manually translated to obtain the EFSM models.
The EFSM for Con has 13 transitions and 1000 tests.
EFSM for Prn has 89 transitions and 1439 tests. Micro-
wave Oven (Mic) is originally described as a Kripke
structure [21]. We simply modified the labels on the arcs
to obtain EFSM transitions by adding input and output
messages. The model has 12 transitions and 1160 tests.
The remaining examples web automatic teller machine
(Atm) (6 transitions and 800 tests), bank (Bnk ) (9 transi-
tions and 1124 tests), a vending machine example (Ven)
(8 transitions and 87 tests) all appear as EFSMs in an
earlier testing paper [23] and were used as such.
8.2. Results
Overview: Our results for the SPG approach are summa-
rized in a table in Table 1. The first column of the table
lists the ten examples along with the number of EFSM
transitions. The second column lists the test suite size
and the average test length for each example.
Columns three, four, and five show C1, the cost for
running the full test suite, C2, the cost for running the
selected tests, and C3, the cost for performing analysis
respectively. These columns list the average costs per

Test Selection on Extended Finite State Machines with Provable Guarantees 508
Table 1. Regression test selec tion c o sts for SPG.
TestSuite
Case
Size Avg length
C1
sec
C2
sec
C3
sec
Select
Tests
Avg time
Save (%)
Con (13) 1000 78 2152837 629 386 32
Prn (89) 1439 102 63453511 2035 798 13
Atm (6) 800 50 1210842 214 486 13
Mic (12) 1160 12 28992 7 614 66
Bnk (9) 1124 35 2483738 1041 364 28
Thp (15) 837 66 1249367 232 203 52
Ven (8) 87 37 92 23 50 20 20
Cnf (19) 723 47 629328 187 257 18
Cmp (7) 800 59 532252 132 316 28
Tcp (14) 311 18 14748 27 102 49
change. Next column is the average number of selected
tests per change. Finally, the last column lists the average
time savings per change, defined as the percentage (C1 -
(C2 + C3))/C1, based on the cost model of [24].
As seen from Table 1, SPG achieves an average time
savings of around 30% while achieving an average re-
duction of around 40% in the size of the test suite se-
lected for all attempted examples.
Time Savings: Varying amount of time savings ob-
tained across these examples can be mainly attributed to
three reasons: complexity of the data values, and data
types used in the EFSMs and the tests, exploiting overlap
in the test descriptions, and the compatibility of transi-
tions. Time savings higher than 50% for Mic are mainly
due to simple data types such as boolean and integers
whereas Atmand Bnk do not have as much time savings
since their EFSMs and tests involve arrays. Time savings
are significant for Thp because the input messages in its
EFSM have no parameters. Consequently, its tests do not
involve any concrete values and allow for lot more over-
laps in the test descriptions. These overlaps are effec-
tively exploited by our simultaneous test selection pro-
cedures using the TST trees.
Reduction in Test Suites: The variance in the number
of selected tests largely depends on the number of transi-
tions in the EFSM models, and those appearing in loops.
Consider the examples Atm with 6 transitions and high
(486) average number of selected tests and Ven with 8
transitions and a very low (20) average number of se-
lected tests. The difference in the average number of se-
lected tests in these examples can be attributed to the
number of transitions appearing in loops. Almost all
transitions of example Atm appear together in one or
more loops. Hence a feasible run corresponding to each
test is likely to contain all of the transitions and this leads
to high number of selected tests. This is in contrast with
Ven where loops contain at most one or two transitions.
Reduction in test suite size is directly related to time
savings in examples such as Prn, Atm, and Thp. However,
in Con, almost 70% of the tests are discarded but time
savings are not as much. This is because discarded do not
take much time to run. Similarly, in Mic few tests are
eliminated but the time savings are higher.
Fault Detection Using SPG: We also studied whether
faults in the system under test can be detected by SPG.
We considered faults that are caused solely due to the
changes in the model. The criterion for test selection
used by SPG is a necessary condition for detecting such
faults. We used the popular TCAS example from the test
benchmark [19] with 41 versions and 1590 tests. We
chose the faulty versions Ver1, Ver2, Ver6, Ver7, Ver8,
and Ver9 produced by mutation analysis. We created
models from each of the faulty versions of the code and
translated the code-based tests to model based tests. SPG
was used to select the model-based tests. The corre-
sponding code-based tests were run on the original and
modified code to identify the model-based tests revealing
faults. Our results are depicted in Table 2. The first
column gives the faulty versions; the second column
gives the tests selected by SPG; the third column gives
the number of selected tests that reveal faults.
As shown, SPG was able to identify a non-zero num-
ber of fault-revealing tests for each version. To further
check if SPG missed any of the fault-revealing tests, we
ran all the code-based tests in the original test suite on
both the original and modified C programs and collected
the tests producing different outputs. These tests were the
same as those identified using SPG in all cases. Hence
SPG selects all the fault-revealing tests in all the ver-
sions.
SPG vs. SYM: The first and third bars in Figure 6
depict the results of our comparison of the analysis costs
(C3) of the SPG and brute-force symbolic execution
(SYM) [25]. The X-axis plots the examples and the
Y-axis plots the analysis cost in seconds. Results show
that cost of SYM is higher than that of SPG in all exam-
ples. This is because, first, SYM does not exploit the test
Table 2. Regression test selec tion c o sts for SPG.
TCAS (1590 test s) Selected tests Fault Reveal tests
Ver1 432 130
Ver2 527 61
Ver6 331 12
Ver7 1560 36
Ver8 1560 1
Ver9 508 9

Test Selection on Extended Finite State Machines with Provable Guarantees 509
0
500
1000
1500
2000
ConPrnAtm MicBnkThpVenCnf Cmp Tcp
SYM SPG
Figure 6. Regression test selection costs for SPG.
description and hence considers every transition in each
execution step and second, SYM analyzes non-modifi-
cation traversing tests in their entirety.
9. Conclusion
An EFSM model-based formal approach to accurately
select tests for regression testing is described. Test de-
scriptions are statically analyzed using the model to for-
mulate a structural invariant such that the transitions that
will be executed by the test can be provably predicted
whenever the invariant is satisfiable. Bounded, incre-
mental procedures for selecting tests guaranteed to exer-
cise addition/deletion/replacement changes and identify
unusable tests are described. We also extend the proce-
dures to simultaneously select and discard multiple tests
from a test suite by exploiting the overlap in the test de-
scriptions. The effectiveness of the approach is illustrated
on several examples including programs from a popular
benchmark, web services, and protocols. Our results
show that our approach achieves an efficiency of around
30% in all these examples and reduces test suit sizes up
to 40%, while being fully inclusive and precise.
REFERENCES
[1] M. J. Harrold and A. Orso, “Retesting Software during
Development and Maintenance,” Frontiers of Software
Maintenance, Beijing, 28 September-4 October 2008, pp.
99-109.
[2] G. Rothermel and M. J. Harrold, “Analyzing Regression
Test Selection Techniques,” IEEE Transactions on Soft-
ware Engineering, Vol. 22, No. 8, 1996, pp. 529-551.
doi:10.1109/32.536955
[3] S. Yoo and M. Harman, “Regression Testing Minimiza-
tion, Selection, and Prioritization: A Survey,” Software
Testing, Verification, and Reliability, Vol. 22, No. 2, 2010,
pp. 67-120. doi:10.1002/stvr.430
[4] Y. Chen, R. L. Rrobert and H. Ural, “Regression Test
Suite Reduction Using Extended Dependence Analysis,”
4th Workshop on Software Quality Assurance, 2007, pp.
62-69.
[5] B. Korel, L. Tahat and B. Vaysburg, “Model Based Re-
gression Test Reduction Using Dependence Analysis,”
International Conference on Software Maintenance, 2002,
pp. 214-223.
[6] D. Detlefs, G. Nelson and J. B. Saxe, “Simplify: A Theo-
rem Prover for Program Checking,” Journal of the ACM,
52, 3, 2005, pp. 365-473. doi:10.1145/1066100.1066102
[7] D. Kapur and H. Zhang, “An Overview of Rewrite Rule
Laboratory (RRL),” Conference on Rewriting Techniques
and Applications, Chapel Hill, 3-5 April 1989, pp. 559-
563.
[8] B. Daniel and Z. Pitro, “On Communicating Finite-State
Machines,” Journal of the ACM, Vol. 30, No. 2, 1983, pp.
323-342.
[9] D. Lee and M. Yiannakakis, “Principles and Methods of
Testing Finite State Machines-Survey,” IEEE Computers,
Vol. 84, No. 8, 1996.
[10] M. Subramaniam and P. Chundi, “An Approach to Pre-
serve Protocol Consistency and Executability across Up-
dates,” Conference on Formal Engineering Methods, Se-
attle, 8-12 December 2004, pp. 341-356.
[11] M. Subramaniam and B. Guo, “A Rewrite-Based Ap-
proach for Change Impact Analysis of Communicating
Systems Using a Theorem Prover,” Tech Report, De-
partment of Computer Science, University of New Or-
leans, New Orleans, 2008.
[12] G. Rothermel and M. J. Harrold, “A Safe, Efficient Re-
gression Test Selection Technique,” ACM Transactions
on Software Engineering and Methodology, Vol. 6, No. 2,
1997, pp. 173-210.
[13] E. Bringmann and A. Kramer, “Model-Based Testing of
Automotive Systems,” Conference on Software Testing,
Verification and Validation (ICST’08), Lillehammer, 9-11
April 2008, pp. 485-493.
[14] Y. Chen, R. L. Probert and D. P. Sims, “Specifica-
tion-Based Regression Test Selection with Risk Analy-
sis,” Conference of the Centre for Advanced Studies on
Collaborative Research, 2002.
[15] L.C. Briand, Y. Labiche and S. He, “Automating Regres-
sion Test Selection Based on UML Designs,” Information
and Software Technology, Vol. 51, No. 1, 2009, pp. 16-30.
doi:10.1016/j.infsof.2008.09.010
[16] L. C. Briand, Y. Labiche and G. Soccar, “Automating
Impact Analysis and Regression Test Selection Based on
UML Designs,” Conference on Software Maintenance,
2002, pp. 252-261.
[17] B. Korel, L. H. Tahat and M. Harman, “Test Prioritization
Using System Models,” Conference on Software Mainte-
nance, 26-29 September 2005, pp. 559-568.
[18] B. Vaysburg, L. H. Tahat and B. Korel, “Dependence
Analysis in Reduction of Requirement Based Test Suites,”
Symptoms on Software Testing and Analysis, Vol. 27, No.
4, 2002, pp. 107-111.
[19] H. Do, S. Elbaum and G. Rothermel, “Supporting Con-
trolled Experimentation with Testing Techniques: An In-
frastructure and Its Potential Impact,” Empirical Software
Engineering, Vol. 10, No. 4, 2005, pp. 405-435.
doi:10.1007/s10664-005-3861-2

Test Selection on Extended Finite State Machines with Provable Guarantees 510
[20] S. Weibleder, “Parteg”. http://parteg.sourceforge.net/
[21] E. M. Clarke, O. Grumberg and D. A. Peled, “Model
Checking,” MIT Press, Cambridge, 1999.
[22] C. Keum, S. Kang, I. Ko, J. Baik and Y. Choi, “Generat-
ing Test Cases for Web Services Using Extended Finite
State Machine,” Conference on Testing of Software and
Communication Systems, New York, 16-18 May 2006, pp.
103-117.
[23] M. Subramaniam, L. Xiao, B. Guo and Z. Pap, “Ap-
proach for Test Selection for EFSMs Using a Prover,”
Conference on Testing of Software and Communications
Systems, Eindhoven, 2-4 November 2009, pp. 146-162.
doi:10.1007/978-3-642-05031-2_10
[24] H. K. N. Leung and L. White, “A Cost Model to Compare
Regression Test Strategies,” Conference on Software Main-
tenance, Sorrento, 15-17 October 1991, pp. 201-208.
[25] J. C. King, “Symbolic Executed and Program Testing,” Com-
munications of the ACM, Vol. 19, No. 7, 1976, pp. 358-
394. doi:10.1145/360248.360252