Journal of Software Engineering and Applications, 2013, 6, 500510 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. Email: bguo@unomaha.edu, msubramaniam@unomaha.edu 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 bruteforce sym bolic evaluation. Keywords: Formal Methods; ModelBased 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 ([13] 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 modelbased 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. Copyright © 2013 SciRes. JSEA
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 postimages) 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 pushbutton 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 nonnegative (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) Copyright © 2013 SciRes. JSEA
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 nonnegative. 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 [711], where more details can be found. Extended Finite State Machines: An EFSM E = (I, O, S, V, T) [9], is a 5tuple 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 stimage 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 postimage 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 mostgeneral 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 Copyright © 2013 SciRes. JSEA
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 postimages 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 pointwise 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 postimage, 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 preimage 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 postimage 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 preimage 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 postimages of the matching transitions as: () () 0 () 1 Init(Emgpos , k n kn 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 postimages 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 Copyright © 2013 SciRes. JSEA
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 Copyright © 2013 SciRes. JSEA
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 modelbased 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 ksatisfiable 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 ksatisfiable 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 ksatisfiable 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 = Copyright © 2013 SciRes. JSEA
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 nonempty 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 nonempty 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 leftright 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 lefttoright 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 codebased or modelbased. 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 codebased approaches. CodeBased Approaches: Codebased 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 highconfidence test suites. ModelBased Approaches: Modelbased approaches use executable models and modelprograms 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 Copyright © 2013 SciRes. JSEA
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 modelbased 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, reusable 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 wellknown 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 builtin 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 modelbased test generator ParTeg [20]. 8.1. Case Studies We have applied the prototype to ten examples from the literature: completion (Cmp), twophase commit (Tcp), and conference (Cnf), and thirdparty 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, twophase commit, and conference protocols described on the website3 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. Twophase 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 chatboxlike 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 thirdparty 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 Copyright © 2013 SciRes. JSEA
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 codebased tests to model based tests. SPG was used to select the modelbased tests. The corre sponding codebased tests were run on the original and modified code to identify the modelbased 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 nonzero num ber of faultrevealing tests for each version. To further check if SPG missed any of the faultrevealing tests, we ran all the codebased 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 faultrevealing 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 bruteforce symbolic execution (SYM) [25]. The Xaxis plots the examples and the Yaxis 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 Copyright © 2013 SciRes. JSEA
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 nonmodifi cation traversing tests in their entirety. 9. Conclusion An EFSM modelbased 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 September4 October 2008, pp. 99109. [2] G. Rothermel and M. J. Harrold, “Analyzing Regression Test Selection Techniques,” IEEE Transactions on Soft ware Engineering, Vol. 22, No. 8, 1996, pp. 529551. 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. 67120. 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. 6269. [5] B. Korel, L. Tahat and B. Vaysburg, “Model Based Re gression Test Reduction Using Dependence Analysis,” International Conference on Software Maintenance, 2002, pp. 214223. [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. 365473. 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, 35 April 1989, pp. 559 563. [8] B. Daniel and Z. Pitro, “On Communicating FiniteState Machines,” Journal of the ACM, Vol. 30, No. 2, 1983, pp. 323342. [9] D. Lee and M. Yiannakakis, “Principles and Methods of Testing Finite State MachinesSurvey,” 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, 812 December 2004, pp. 341356. [11] M. Subramaniam and B. Guo, “A RewriteBased 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. 173210. [13] E. Bringmann and A. Kramer, “ModelBased Testing of Automotive Systems,” Conference on Software Testing, Verification and Validation (ICST’08), Lillehammer, 911 April 2008, pp. 485493. [14] Y. Chen, R. L. Probert and D. P. Sims, “Specifica tionBased 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. 1630. 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. 252261. [17] B. Korel, L. H. Tahat and M. Harman, “Test Prioritization Using System Models,” Conference on Software Mainte nance, 2629 September 2005, pp. 559568. [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. 107111. [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. 405435. doi:10.1007/s1066400538612 Copyright © 2013 SciRes. JSEA
Test Selection on Extended Finite State Machines with Provable Guarantees Copyright © 2013 SciRes. JSEA 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, 1618 May 2006, pp. 103117. [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, 24 November 2009, pp. 146162. doi:10.1007/9783642050312_10 [24] H. K. N. Leung and L. White, “A Cost Model to Compare Regression Test Strategies,” Conference on Software Main tenance, Sorrento, 1517 October 1991, pp. 201208. [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
