Verifying embedded software functionality: The power of dynamic slicing
Suppose the programmer wants an explanation of the value of sum printed in line 10; thus the slicing criterion is (10,sum). We seek an automated method that can find the fragment of the program which influences the value of sum at line 10; this fragment will be treated as the explanation of the value of sum in line 10.
In constructing the explanation, we try to answer the following questions:
Dynamic data dependence: Which variable assignment was propagated to the value of sum printed in line 10?
Dynamic control dependence: What is the nearest conditional branch statement that enables line 10 to be executed, in the execution trace under consideration? These questions can be answered by a backwards traversal of the execution trace starting from line 10, the slicing criterion. In particular, the value of sum in line 10 contains the value set in the last execution of line 7. As far as dynamic control dependencies go, we observe that the execution of line 10 is unconditional, it does not depend on any conditional branch statement evaluating in a certain direction.
In case the reader is reasoning that line 10 got executed only because the while-loop (line 5) terminated and hence line 5 and line 10 are control dependent, here is the way to think about this matter. Any program execution from line 5 to the end of the program will pass through line 10. Hence line 5 does not enable line 10 to be executed.
The dynamic control and data dependencies in an execution trace are typically summarized in a dynamic dependency graph. Because one statement may be executed several time in an execution trace, we distinguish between the different occurrences of the same statement—each occurrence is a separate statement instance.
The nodes of a dynamic dependency graph are the statement instances, and the edges are dynamic dependencies (both data and control dependencies). Part of the dynamic dependency graph for the example program of Figure 5.4 with input N = 3 is given in Figure 5.5 below; dashed edges denote control dependencies, and solid edges denote data dependencies.We show only the part of the dynamic dependency graph that is relevant to our slicing criterion—the value of sum in line 10 of the program.
Each node in the dynamic dependency graph in Figure 5.5 is of the form ij denoting the jth occurrence of line i in the execution trace of the program in Figure 5.4 with input N = 3. Let us now explain the dependencies shown in Figure 5.5.
Statement instance 101 is dynamically data dependent on 71, because the definition of sum in 71 is used in 101. Also, statement instance 71 is dynamically control dependent on statement instance 62; 62 is the nearest enclosing branch statement instance s.t. the evaluation of the corresponding branch, which allows 71 to be executed. Figure 5.5 shows only a fragment of the dynamic dependency graph—the fragment that is reachable from our slicing criterion, the value of sum in line 10.
The slice consists of the following statement instances from which statement instances 101,71,62,52,91,31,51,21,11 that is, instances of the following statements: {1, 2, 3, 5, 6, 7, 9,10} Lines 4 and 8, which manipulate the variable prod, are not in the slice.
Loading comments... Write a comment