Improving the Automatic Test Generation process for Coverage Analysis using CBMC

Abstract

Proceedings of the 16th International RCRA workshop (RCRA 2009): Experimental Evaluation of Algorithms for Solving Problems with Combinatorial Explosion Reggio Emilia, Italy, 12 December 2009

-

Software Testing via Coverage Analysis is the most used technique for software veri cation in industry, but, since manual generation is involved, remains one of the most expensive process of the software development. Many tools have been proposed for the automatic test generation: on one hand they reduce the cost of the testing generation process, on the other hand the quality of the test set so generated is lower than the quality of the test set manually generated by domain experts. In fact, most of the time, the test set automatically generated contains redundant tests, i.e. test that does not contribute to reach the property of 100% of coverage: if they are eliminated by the set, the property still holds. Indeed, these redundant tests are useless from the perspective of the coverage, are not easy to detect and then to eliminate a posteriori, and, if maintained, imply additional costs during the veri cation process.

In this paper we present a methodology for the automatic generation of test set for Coverage Analysis, containing only non redundant test. We experimented it on a subset of modules of the ERTMS/ETCS source code, an industrial system for the control of the tra c railway, provided by Ansaldo STS, where we were able to verify completely 31 di erent modules of the ERTMS: On 20 modules we were able to generate a set of minimal test covering the 100% of the code for each function in each module; on 7 of them we generate a set of tests that does not cover the 100% of the branches due to unreachable code; the last 4 modules were not completely veri ed due to CBMC exponential blow-up explosion. The use of our methodology for test generation led to a dramatic increase in the productivity of the entire Software Development process by substantially reducing the number of tests generated and thus the costs of the testing phase. Testing [ 8 ] is the most used technique for software veri cation: it is easy to use and even if no error is found, it can release a set of tests certifying the (partial) correctness of the compiled system. The most used technique for test generation is random testing since it is automatic and simple to apply. However, it does not ensure an extensive test of the code: since it merely relies on probability it has quite low chance of nding semantically small faults. Thus, in order to increase the con dence of the correctness of the compiled system, it is often required that the provided set of tests covers 100% of the code. This requirement, however, substantially increases the costs associated to the testing phase, since it may involve the manual generation of tests. In the literature many techniques have been proposed to automatically generate test for coverage analysis [ 9 ], [10], [ 7 ]: on one hand they reduce the cost of the testing generation process, on the other hand most of the times the quality of the test set so generated is lower than the quality of the test set manually generated by domain experts. For instance, in a previous paper [ 7 ] we have shown how it is possible to automatically generate test sets covering 100% of the code using a bounded model checker in an industrial setting: Such test set met the desired coverage properties previously reached only by manual generation, but on the other hand it contained many redundant tests, i.e., tests not contributing to covering not otherwise covered portions of the code. Indeed, these redundant tests are useless from the perspective of the coverage, are not easy to detect and then to eliminate a posteriori, and, if maintained, imply additional costs during the veri cation process. Determine which test set to use is still a major problem in program testing. One technique that is in widespread use is to take the control ow graph from each of the program function and calculate a set of independent paths, i.e. a set of paths through the functions that are linearly independent. From this set, that has to cover the 100% of the branches in the control ow graph, it is possible to construct a test exercising that path, unless the path is unfeasible. In this paper we present a methodology for the automatic generation of a set of non redundant test, through the construction of a set of independent paths covering the 100% of the branches in the control ow graph of the function under test. In other words, given a program to test, for each function we rstly construct the control ow graph from which we deduce an independent set of paths. Then for each path we generate a test that, when the program (function) is executed, it explores exactly that path. As a test generator we use CBMC [ 1 ] a Bounded Model Checker for low-level ANSI-C programs. CBMC checks safety properties such as the correctness of pointer constructs, array bounds, and user-provided assertions. CBMC, as showed in [ 7 ], can also be used as a test generator, if it can take as input an instrumented code. However, the methodology proposed in [ 7 ] does not generate a set of tests without redundancy: usually the path explored to generate a test is chosen by CBMC in a heuristic way, thus the set of paths associated to the set of tests generated by CBMC is not guarantee to be non redundant. In this paper we show also how to instrument a function in order to force CBMC to generate a test following a given path. In this way we can generate a set of tests that satis es the 100% of the branch coverage. We experimented our methodology on a subset of modules of the ERTMS/ETCS [ 5 ] source code, an industrial system for the control of the tra c railway, provided by Ansaldo STS. ERTMS is an initiative from the European Community to create a unique signaling standard as a cornerstone for the achievement of the interoperability of the trans-European rail network and is likely to be adopted by the rest of the world as well. Ansaldo STS, an industry leader in Europe for the railway system, provides its implementation of the ERTMS/ETCS written in standard ANSI-C, which consists of thousands of code lines. In the eld of railway signaling systems the CENELEC EN50128 [ 3 ] guidelines for software development recommend the use of formal methods where it is possible and a 100% of testing coverage where it is impossible. In this paper the case study provided by Ansaldo STS has been veri ed with CBMC obtaining the target 100% code coverage, requested by CENELEC guidelines. The use of our methodology for test generation led to a dramatic increase in the productivity of the entire Software Development process by substantially reducing the number of tests generated and thus the costs of the testing phase. The paper is structured as follows: we rstly describe a simple and naive algorithm for test generation from a set of independent path, making the assumption of not having unfeasible paths in the program. Then we describe how to modify the algorithm in order to release the assumption and we nally show the experimental results and the conclusions. 2

Branch Coverage Via Path Generation

In this section we rst present some basic notions used through the paper, then the basic algorithm is presented, under the assumption of not having to test program with unfeasible paths and nally we present the advanced algorithm taking into account also the unfeasible paths. 2.1 A

Basic De nitions

N is a set of nodes ow graph is a directed graph C = (N,E,ns,ne) where

E is a binary relation on N (a subset of N x N ), referred to a set of edges; ns 2 N and ne 2 N are unique entry (start) and unique exit nodes respectively.

A control ow graph is a representation, using graph notation, of all paths that might be traversed by a program during its execution. Each node in the graph represents a basic block, i.e. a piece of code without any jump or jump target; jump targets start a block and jumps end a block. Directed edges are used to represent jumps in the control ow. In most representations there are two specially designated blocks: the entry block, through which control enters into the ow graph, and the exit block, through which all the control ows leave. Moreover, for each edge, it is also annotated which branch condition, if any, it represents. We say that a branch predicate guards a basic block if the true value of the predicate implies the execution of the block. Given a control ow graph G, a path p in G is a sequence p = fn1; n2; :::nkg of nodes such that n1 = ns and nk = ne and for all i; 1 i k, (ni; ni+1) 2 E. Notice that an assignment to the input variables determines a path along the control ow graph, but the contrary is not always true. We say that a path is feasible if it exists an assignment to the program's input X for which the path is traversed during the program execution, otherwise the path is unfeasible. Given a set of path of a control ow graph, an independent path is a path such that: there is at least an edge in the path that does not occur in any other path in the set. A branch is de ned as any decision outcome in the source code. This is re ected in the unwinded ow graph: for every decision we have one or more nodes with two or more outgoing edges, representing the branches. Di erent edges in the unwinded graph may refer to the same original branch. Covering a branch requires producing at least a test that contains at least an edge which referes to that branch. CBMC is a Bounded Model Checker for software veri cation [ 1 ], that takes as input a low-level C program and it checks safety properties such as the correctness of pointer constructs, array bounds, and user-provided assertions. Given a program D, and a property P , the veri cation is done translating both the program and the property into a Boolean formula in Conjunctive Normal Form (CNF) and giving the result to a SAT solver like MiniSat [ 4 ]. If the SAT solver returns false then the property holds, otherwise the property does not hold. The conversion from a C program into a CNF consists of three steps: 1. Each function call should be replaced by its function body; 2. Each loop should be unwound, i.e. the body has to be duplicated k times, where k is a parameter given in input (goto statements are unwound in a similar way). Notice that each copy of the body is guarded by an if statement that uses the same condition of the loop statement. 3. The program and the property are rewritten into an equivalent program in Single Static Assignment (SSA) form [ 2 ] that is an Intermediate Representation (IR) where each variable is assigned exactly once. In the original IR existing variables are split into versions, new variables are typically indicated by the original name with a subscript, so that every de nition gets its own version.

Given the property P and a program D both in SSA form, the formula D ^ :P is rst converted into a bit-vector equation, i.e. each variable is represented by a bit-vector of xed size, and the operations are converted into bit-vector operations. Finally, it is converted into a propositional formula in Conjunctive Normal Form (CNF), by adding intermediate variables. If applying a SAT solver to the CNF, the equation is satis able, then the property does not hold, and an assignment to the variables making the formula true is returned. Starting from this assignment, it is possible to construct an error trace showing where the property does not hold in the program. Otherwise, if the resulting CNF is false the property holds. However, we can not conclude by saying that the program is veri ed, but we can say that it is veri ed for a given k. Choosing another k0 > k does not ensure that the property holds. In order to use CBMC as a test generator we need to modify the code in input as rstly presented in [ 7 ]: the code under test is instrumented with an assert(0) after each branch; the instrumented code is given as input to CBMC with an assert activated at the time. For each assert, CBMC returns an assignment to the input variables (a test) violating the property (assert(0)). The asserts are inserted in a naive way without any reasoning, this would generate more tests than necessary. Let's take the following example: if a == 10 then B1 else B2 if a 6= 5 then B3 else B4 given the methodology in [ 7 ], it will generate four di erent program codes adding an assert(0) at the end of each block, namely B1; B2; B3; B4. The set of tests

T = ft1; t2; t3; t4g generated covers the 100% of the branches for construction, and for example set of paths pathGenerator(C) 0 P = fg; 1 Au = update(P,C); 2 while jAuj 6= 0 do 3 P = P [ genApath(ns,Au); 4 return P; path genApath(n,Au) 5 if n ne then return fng 6 maxn = succ(n).first(); 7 foreach si 2 succ(n) do 8 if jAu(maxs)j < jAu(si)j then 9 maxs = si 10 else if jAu(maxs)j == jAu(si)j then 11 if E(n; maxs) 2= Au then 12 maxs = si 13 Au = update(P,C); 14 return fng [

genApath(maxs,Au) they could be:

t1: (a = 10), t2: (a = 6), t3: (a = 5), t4: (a = 4) However it may be the case that eliminating one or two test from the set the 100% of branch are still covered, for example also the test set T 0 = ft1; t3g covers the 100% of the branches. In the naive algorithm we always generate more test of the ones needed to grant the 100% of branch coverage. This may increase the costs associated to the testing phase, in particular during the regression phase. In order to reduce the size of the test set we rst construct a set of independent paths covering the 100% of the branches of the control ow graph. Then, given a path in the set, it is possible to instrument CBMC in order to generate a test following the path. The testing process is presented in gure 1. It assumes that all the paths are feasible. This is a big restriction that is made only for a better comprehension of the algorithm. In the next subsections the algorithm that takes s0 b1 b3 s4 s4 int Test1(int[ ] a, int size) b1 s0 int b = 0; int c = 0; b3 b1; b2, s1 for ( ; (c < size); c++) s4 b3; b4 if (a[c] < 0) b1 s2 b++; s3 return b; int Test1(int[ ] a, int size) int b = 0; int c = 0; assume(c < size); assume(a[c] < 0); b++; c++; assume(c < size); assume(!(a[c] < 0));

c++; assume(!(c < size)); assert(); s13 return b; into account unfeasible paths is presented.

The process in gure 1 rstly analyzes the code under test and it constructs a set of independent paths covering the 100% of the branches in the control ow graph associated to the program under test (pathGenerator), i.e. each path covers at least a branch not covered by any other path. Then, from each path, the module ATG via CBMC will generate a test in a way similar to the one presented in [ 7 ]. For each path, the original code is instrumented and it is given to CBMC, which will return an assignment to the input variables, a test, soliciting the path through the code. The process is composed by three main functions: pathGenerator, genApath, ATGviaCBMC, as shown in gure 2 and 3. pathGenerator is a function presented into details in gure 2, left, that takes as input the control ow graph representation of the program under test (C). It returns a set of basis paths (P) covering the 100% of the branches in C. P is initially empty. Au is the set of branches in C not yet covered by any path in P. Au initially contains all the branches in C. Given a node n 2 C, Au(n) is a set of branches not yet covered in C, that can be covered from n. Given a node n, Au(n) is de ned recursively as follow: Au(ne) = fg Au(n) = Sjis=u1cc(n)j Au(si) [ fE(n; si)g : E(n; si) 2 Au fg : E(n; si) 2= Au where ne is the end node of the control ow graph, si is a successor of n, E(n1; n2) is the branch from n1 to n2 and succ(n) is the set containing all the successors of n. So for example, given a control ow graph C, s0 a root node and s1 is a successor of s0 connected with a branch b1. Let be s2 a successor of s1 connected with a branch b2, then Au(s0) = fb1; b2g. Notice that Au = Au(ns). Looking at the algorithm in gure 2, left, that generates a set of paths, it starts from an empty set of paths (line 0) and a set of uncovered branches containing all the branches of C (line 1). The function UPDATE(P,C) returns all the branches of C not yet covered by P. Moreover for each node n in C, it will update Au(n). Then, while there are still uncovered branches in C(line 2), a new path is generated and added to P (line 3). genApath is a recursive function that given a set of uncovered branches (Au) and a starting node (n) generates a path containing at least an uncovered branch in Au. It always starts from the beginning of the control ow graph (line 3) from the node ns. The idea is: starting from a node n, the algorithm explores successors of n, si, and it chooses the one having the greatest number of uncovered branches (from line 8 till 12). If a tie is found between two successors of n (line 10), n1 and n2, then the one having E(n; ni) 2 Au, in lexicographic order, is chosen. The algorithm stops whenever the end of the control ow graph (ne) is reached line 5. Then the path is constructed in a backtrack way, starting from the last node ne, including all the nodes explored by the algorithm (line 14). The algorithms in gure 2 left and right only generate a set of independent paths.

ATGviaCBMC is a function that takes as input a set of paths and it will return (if exists) a test for the program under test representing each path. T is the set of tests generated, initially empty (line 15). Then for each path the program D is modi ed, i.e. opportunely instrumented,(line 17) and a new program, D0 is created. D0 is then passed to the tool CBMC(line 18) that returns as assignment to the input variables exploring the path in input. D0 has to be carefully instrumented in order to generate a test. In [ 7 ] an assert(0) is added when a branch needs to be covered. However CBMC chooses which path has to follow in order to generate a test to cover the assert. We can still use CBMC but we need something to force CBMC to reach an assertion through a path. CBMC has a construct, namely assume (expression = value) that inserted at a given point in the code enforces the expression to assume exactly that value at that point. Using the assume construct we can enforce a path at the time in the code, obtaining from CBMC a test exploring the path. In order to obtain the 100% of the branch coverage for each independent path we produce an instrumented code using the assume construct to enforce the path and we put an assert(0) at the end of the code. Then for each instrumented code we run CBMC that returns a test for that path.

An example of the algorithm behavior is presented below. Let's assume as a function under test the function presented in gure 4 which counts negatives in an array. The algorithm presented above takes as input C, i.e. the control ow graph representation of the function in gure 4, left already unwinded. The set of paths, line 0, is initially empty and the Au is updated (line 1) with all the branches of the Control Flow graph, Au = fb1; b2; b3; b4g. For each node n it is also updated Au(n). Notice that the function genApath will work on the control ow graph unwinded, which is shown in gure 5, right, assuming an unwind value of 3. Each function has a minimum unwind value k, necessary to reach full coverage, which depends on the cycles structure. Best way to set k would be to know such minimum a priori but that's not feasible in an automatic way so, a good alternative solution is to start testing with low k and increase it until coverage is reached. Lower k are faster to test but have less chances to reach full coverage while bigger k requires more time and e ort for both CBMC and our algorithm and also increase the chances that CBMC will fail to nd an answer in the given time. At the rst node there is only one branch (without any label) and then the recursive call to genApath(s1,Au) is executed. At this point since s1 is not the end node, its successor nodes (s2 and s13) would be explored. maxs = s2, since jAu(s13)j = 0 and jAu(s2)j = 4 (fb1; b2; b3; b4g). The current coverage status is then updated by deleting b1, which is the incoming edge used to reach s2, from both Au and from each Au(n) where n is a node in C. A new recursive call, genApath(s2,Au) is executed. Then the algorithm chooses between s3 and s4, having jAu(s3)j = jAu(s4)j = 3, (fb2; b3; b4g) and being both edges b3 and b4 uncovered, the algorithm breaks the ties by lexicographic order choosing s3. Au is updated deleting b4 and it is also updated for each node. From node s3 to node s5 there is a single path to be followed. On node s5 maxs = s6 with jAu(s6)j = 2 (fb2; b3g) against jAu(s13)j = 0. From s6, s8 will be chosen because even if jAu(s7)j = jAu(s8)j = 2, b3 is not yet covered. Finally the algorithm will go from s9 to s13, covering b2. As soon as the algorithm reaches the s13 node it will stop and backtrack until the root constructing the path, i.e. p1 = fs0; s1; s2; s3; s4; s5; s6; s8; s9; s13g. This path can cover all the branches, so no more calls will be necessary. The pathGenerator function will return a set of paths, P = fp1g and then the function ATGviaCBMC is called. The function instrument the code in order to force CBMC to follow the path. In gure 4, right, the modi ed code (C0) for the generated path is presented. Notice that: the instrumented code is already unwinded, unnecessary code is removed in order to help CBMC to nd a solution. Since we are exploring a path only the code explored by the path is necessary.

CBMC, taking as input the modi ed code, will generate a test, i.e. with the following inputs, size = 2, a[0] = 1 and a[ 1 ] = 0. 2.3

Using CBMC for Unfeasible Path

In case of unfeasible paths the algorithm presented above will generate a set of tests that does not cover the 100% of the branches. In order to overcome the problem whenever a path is generated, a checker is used to analyze the path and return if the path is feasible or not. In case of unfeasible path a new path has to be generated. As feasibility checker we use CBMC: if a test is returned from CBMC then the path is feasible otherwise is not. The new algorithm is composed by a function CreateTestSet that uses the function generatePath, that it is similar to the one presented above: this function also takes as input a set of branches that have not to be covered from the path returned. In case that this set is empty the function is equivalent to the one presented above.

CreateTestSet is a function presented in gure 6 that given a set of branches(Au) and a program P returns a set of tests covering the 100% of the branches in Au. Given a nite set of paths of a program P (P k), generate a path covering as much branches in Au as possible CreateTestSet generates a path covering as much branches as possible of Au (line 2) starting from the basic path (bp) and avoiding the Forbidden branches (F). If such path exists, then CBMC is invoked (line 4) and if the path is feasible CBMC returns a vector of values for the input variables; then the test is added to the set of Tests T (line 8) and the branches traversed by P are eliminated from Au. If the path is unfeasible the function analisePath returns (if any) the subset of arch which make it feasible (bp) and the arches set of Tests createTestSet(Au; P; kmax) 0 k = 4; T = fg; bp = fnsg; F = fg 1 while jAuj > 0 & k < kmax do 2 p = generateP ath(Au; bp; F; P k) 3 if jpj > 0 then 4 t = generateT est(p; P k) 5 if t == t0 then 6 hbp; F i = analiseP ath(bp; p; F; P k) 7 else if t == tstop then 8 return T 9 else 10 T = T S ftg 11 bp = fnsg 12 Au = update(Au,p) 13 else 14 if bp 6= fnsg then 15 F = fbpg 16 bp = bp n tail(bp) 17 else 18 k=k*2; F =fg; bp = fnsg 19 return T making the path unfeasible are stored in F (line 6) so that the next path will be generated starting from bp and avoiding the forbidden path. If the path generated in line 2 is empty, i.e. does not exists any path starting from bp and covering at least a branch in Au such that the branch is forbidden, then a new basic path is computed, i.e. the tail of the basic path is removed and it became a forbidden arch. If bp was the root, jAuj is not equal to zero, then there are some branches not covered with the xed k: at this point (line 16) k is incremented and the search restarts again. The function returns the set of tests so computed.

Suppose, for example, that the function in gure 4 did not have the size of the array as an input, but instead it is hard coded in the cycle and it is greater than 2, i.e. 3. Also necessarily consider a greater unwind value, i.e. 4 instead of 3. In this case the previous algorithm would generate the exact same path but that would be unfeasible because it tries to exit from the cycle after two iterations, which cannot be done. The new algorithm will then exclude that possibility by removing and forbidding the last step from the path and compute another path with the same initial subpath which will stay in the cycle one more iteration and exit afterwards. This will be found feasible and reported as a test. manual 127 57 17 43 18 39 27 200 144 35 312 34 181 157 322 69 36 101 62 119 2100

Experimental Analysis

Nowadays trains are equipped with up to six di erent navigational systems which are extremely costly and take space on-board. A train crossing from one European country to another must switch the operating standards as it crosses the border. The European Rail Tra c Management System [ 5 ] is an EU \major European industrial project" to enhance cross-border interoperability and signaling procurement by creating a single Europe-wide standard for railway signaling. ERTMS has two basic components: ETCS, the European Train Control System, transmits speed information to the train driver and it monitors constantly the driver's compliance with the speed information; GSM-R is based on standard GSM but it uses various frequencies speci c to rail as well as certain advanced functions. It is the radio system used to exchange voice and data information between the track and the train. unreachable path 1 2 2 1 1 1 1 2 0 2 0 13

Ansaldo STS as part of the European Project produces the European Vital Computer (EVC) software, a fail-safe system which supervises and controls the speed pro les using the information received from the in-track balises transmitted to the train. Following the CENELEC standards Ansaldo STS needs to provide a certi cate of the integrity level required, i.e. it has to provide a set of tests covering the 100% of the branches. In order to simplify the readability, the Ansaldo STS implementation of the EVC is developed into di erent modules of xed size. In our experimental analysis we took a subset of the interconnected modules of the EVC and we applied the automatic test generation strategy seen in the section above. We get more than 130 di erent modules, containing more than 100.000 lines of code distributed in more than 1700 functions. As a comparison we only took 31 di erent modules, the modules on which we get informations about the tests manually generated by Ansaldo STS. As unwind, after a brief analysis, we start from k = 5 till k = 100, with step 2. We also set a 20 minutes timeout for both our algorithm and CBMC.

In gure 7 are reported the results on the module on which we reach the 100% of branch coverage. The columns from left to right represent: the name of the module (for copyright reasons they are coded), the number of functions contained in the module, the number of tests needed to reach the 100% of branch coverage using the naive method presented in [ 7 ], the number of tests using manual generation, provided by Ansaldo STS, the number of tests generated by our technique presented above. Our algorithm on 20 modules always reach the 100% of the branch coverage. Firstly notice that the number of tests generated by the naive method is always greater than the number of tests generated manually: In 5 cases the number of tests manually generated by the naive algorithm is more than a factor two with respect the number of tests automatically generated, while there is only one case where manual generation creates more tests than the naive method, i.e. for the module03. This is mainly due to the manual generation method. For each function Ansaldo STS maintains a set of functionality tests say Tf : if Tf already guarantee branch coverage then no more test are generated, otherwise a new test set Tc is generated to cover remaining branches. The nal test set for coverage will be: T = Tf [ Tc, which frequently contains redundant test. In this case, for the module03, the number of tests for functionality covers the 100% of the branches and from a coverage point of view, there are some test that are redundant. Moreover, looking at gure 7, we always automatically generate a test set having size smaller that the one generated by Ansaldo STS. Only module10 does not follow this rule mainly due to the unwind strategy used: starting from greater k, it is possible to generate smaller test set covering the 100% of the branch [ 6 ]. As a matter of fact, for all the other modules, the number of tests is always less than the number of tests manually generated. The time used to generate the tests is very low and it is not comparable with the time spent by Ansaldo STS to manually generate them, as already described in [ 7 ].

In gure 8 are also reported the modules on which we were not able to obtain full coverage: the rst column reports the name, the second column the number of functions in the module, third the number of functions not covered due to unreachable code and the last column reports the number of functions not fully covered due to CBMC time-out. The functions that are not reported in the last two columns, have been fully covered, with less test than manual generation. As shown in the table, few functions have been reported as uncoverable, in particular the functions presenting unreachable codes have been manually checked. Also Ansaldo STS has reported that these functions can not be fully covered. The results, as shown in the tables, are that only 4 modules out of 31 can not be completely covered (13% of the modules) and the number of functions that can not be covered are 11 (resp. 13) for timeout (resp. unreachable code) out of 415. 4

Conclusion

In this paper we have presented a methodology for the automatic generation of test set for Coverage Analysis, containing only non redundant test. The generation goes through the construction of a set of feasible (if exist) independent paths. We have experimented our methodology on a subset of modules of the ERTMS/ETCS source code, an industrial system for the control of the tra c railway, provided by Ansaldo STS. With our methodology we were able to verify completely 20 out of 31 di erent modules of the ERTMS. On the remaining we were able to conclude that 7 out of 31 could not be covered due to unreachable code while for the last 4 out of 31 has been impossible to reach complete coverage since CBMC could not nish. This paper has shown that the use of our methodology for test generation led to a dramatic increase in the productivity of the entire Software Development process by substantially reducing the number of tests generated and thus the costs of the testing phase.

References

[1] E. Clarke , D. Kroening , F. Lerda . : A Tool for Checking ANSI-C Program. Tools and Algorithms for the Construction and Analysis of Systems , 2004 , pp. 168 { 176 .

[2] R. Cytron , J. Ferrante , B. K. Rosen , M. N. Wegman , F. K. Zadeck. : E ciently Computing Static Single Assignment Form and the Control Dependence Graph . In ACM Transactions on Programming Languages and Systems , 1991 , vol. 13 , number 4, pp. 451 { 490 .

[3] European Committee for Electrotechnical Standardization. : Railway Applications - Communication, signalling and processing systems - Software for railway control and protection systems . http:://www.cenelec.eu

[4] N. Een , N. Sorensson. : An Extensible SAT-solver . In Satis ability Workshop , 2003 , pp. 502 - 518 .

[5] ERTMS: The o cial Website . http://www.ertms.com/, 2008 .

[6] A. Arcuri . : Longer is Better: On the Role of Test Sequence Length in Software Testing . 2009

[7] D. Angeletti , E. Giunchiglia, M. Narizzano , A. Puddu , S. Sabina. : Automatic Test Generation for Coverage Analysis of ERTMS software . International Conference on Software Testing , Veri cation , and Validation (ICST). Denver (CO) 2009 .

[8] B. Beizer . : Software testing techniques . New York: Van Nostrand Reinhold Co. 1990 .

[9] H. Chockler , O. Kupferman , R.P. Kurshan , M.Y. Vardi . : A Practical Approach to Coverage in Model Checking . n Proceedings of the 13th international Conference on Computer Aided Veri cation , 2001 , vol. 2102 . pp. 66 - 78 .