Verifying embedded software functionality: Combining formal verification with testing

Abhik Roychoudhury

August 29, 2012

Abhik Roychoudhury

Formal verification methods achieve full coverage of program behaviors in the abstract state space. However, because of the information (about program variable values) lost in the abstraction, the errors reported by covering the abstract state space might not correspond to actual errors in a concrete program.We saw an example in earlier in this series, reproduced here for convenience:

1 x = 0;
2 x = x + 1;
3 x = x – 1;
4 if (x == 1) {
5 ... /* error */}

Here, by abstracting the program only w.r.t. the predicate [x == 0] and model checking the abstracted program, we are unable to infer that the error location is unreachable. Thus, we report a false bug, a path to the error location as follows: (1,[x == 0]), 2,[x==0]), (3, ![x==0]), (4,![x==0]), (5, ...)

This is what we mean by a false positive or a false alarm: a reported bug that does not correspond to any program error. Such a false alarm appears because of the information loss in abstraction and will show up during model checking of the abstract state space.

Because formal verification (such as model checking) and testing methods have complementary strengths and weaknesses, there have been attempts to combine them and reap the benefits of both. One possibility that has been studied is to use model checking for systematic generation of tests.

Yet another possibility is to use tests (and the observations resulting from running these tests) for learning about the program model, when the program is a black box. Usually these methods can be thought of as model checking helping testing, or vice versa.

In the recent past, software validation methods where testing and model checking simultaneously help each other have also been studied.To discuss the inner workings of such methods, we modify the example program in the preceding and introduce a program loop that does not modify variable x:

1 x = 0;
2 x = x + 1;
3 x = x – 1;
4 for (i=0; i<100; i++){
5 ... /* x is not modified in the loop */
6 }
7 if (x == 0) {
8 ... /* error */ }
9 ... /* end of program */

Suppose we want to check whether the error location is reachable. How do we start? We can perform predicate abstraction of the program and perform model checking of the abstracted program.

The property we want to verify states that the error location is never reached—specified as

G(pc≠8)

in linear-time temporal logic (LTL). The foregoing property states that the program counter ( pc) never goes to line 8 (the error location).A violation of the property will be a counterexample trace that reaches line 8.

To perform predicate abstraction, we need a set of predicates w.r.t. which we abstract. What set of predicates do we choose? As discussed earlier, we can simply start with the null set of predicates.

This the coarsest possible predicate abstraction, which treats each path in a program’s control-flow graph as feasible (i.e., the abstraction assumes that for each path _ in the control flow graph of a program, there is some program input exercising the path). Model checking finds the shortest counterexample trace:

1,2,3,4,7,8

Because we did predicate abstraction w.r.t. a null set of predicates, we are not keeping track of the program variable values at all in the abstracted finite-state transition system. We only keep track of the program-counter value (also called the control location). We can now analyze this counterexample trace by collecting its path constraint, This will show that the foregoing is a spurious counterexample, because there is no concrete execution

1,2,3,4,7,8

the loop needs to be iterated 100 times!!

According to the abstraction refinement methodology, we need to abstract our program w.r.t. a new predicate and run model checking again. The trouble with this approach is that whatever predicates we abstract our program with, model checking will successively uncover longer and longer paths to line 8 (all of which are spurious, that is, do not correspond to any concrete program execution). These paths correspond to the number of times we iterate through the loop.

1, 2, 3, 4, 7, 8
1, 2, 3, 4, 5, 6, 4, 7, 8
1, 2, 3, 4, 5, 6, 4, 5, 6, 4, 7, 8

This is clearly inefficient. In our program, we will then need 100 refinement steps to show that the error location is indeed not reachable. If we had a loop iterating 1 million times, we would have required 1 million refinement steps!

Fortunately, testing methods can be combined with model checking to solve our problem. Here, we first abstract the program w.r.t. the null set of predicates and run model checking. This produces (as before), the counterexample trace:

1,2,3,4,7,8

We can now use directed testing to attempt a concrete test trace that goes through this path (or as long a prefix of the path as possible). We find a concrete trace that visits lines 1, 2, 3, but not line 8. The trace is

1,2,3,(4,5,6)¹⁰⁰,4,7,8

Note that this is a concrete path which can be exercised by executing the program. Thus, our concrete test trace straightaway shows that the error location is reachable, because it visits the error location (line 8). So, we completely avoided the 100 refinement steps necessary to show this error via pure abstraction refinement-oriented verification.

In summary, testing methods try to find witnesses of errors, whereas formal verification methods prove the absence of errors. Both have their unique plus and minus points. By judiciously combining them, we can develop powerful software validation methods that rely on testing to show presence of bugs, and on verification to show absence of them.

To read Part 1, go to “Why it’s necessary”.
To read Part 2, go to “The power of dynamic slicing.”
To read Part 3, go to “Fault localization, metrics, and directed testing.”

Used with permission from Morgan Kaufmann, a division of Elsevier. Copyright 2009, from "Embedded Systems and Software Validation," by Abhik Roychoudbury. For more information about this title and other similar books, visit www.elsevierdirect.com

Abhik Roychoudhury is associate professor at the National Univdrsity of Singapore. He received his Ph.D. in computer science from the State University of New York at Stony Brook. His research interests are system modeling and validation with a specific focus on embedded software and systems.