Verifying embedded software functionality: Combining formal verification with testingEditor’s Note: In the final part in a four part series Abhik Roychoudhury, author of Embedded Systems and software validation, explains the usefulness of formal verification techniques to traditional software testing techniques.
As noted in Part 1 , Part 2, and Part 3 in this series, dynamic or trace-based checking methods are very useful for testing-oriented debugging. In other words, the software validation flow revolves around program testing—we test a program against selected test cases, and for the failed test cases (the ones for which the program output does not match the programmer’s “expectations”), we analyze the traces for these test cases using dynamic checking methods.
However, program testing, by its very nature, is nonexhaustive. It is not feasible to test a program against all possible inputs. As a result, for safety-critical software it is crucial to employ checking methods that go beyond testing-oriented debugging. .
Currently, many functionalities in our daily lives are software controlled—functionalities that earlier used to be controlled by electrical/mechanical devices. Two specific application domains where software is increasingly being used to control critical functionalities are automotive and avionics. .
Naturally, for such software it is critical to give certain guarantees about the software. Unfortunately, testing cannot deliver any guarantees about software behavior. Testing can only be used to show the presence of bugs; it cannot be used to guarantee the absence of bugs. .
For safety-critical software, it is necessary to formally check properties of the software and provide guarantees about its behavior. However, this is a tall order. How do we specify the guarantees that we need? .
And, how do we formally check programs for such guarantees? Our first thought is to employ automated checking methods such as model checking, which checks a temporal logic property (a property constraining the order in which events can occur) against a finite-state transition system. .
Model checking is not directly applicable for software verification, because any program in a modern programming language (such as C or Java) contains variables from infinite domains (integers, floating-point numbers).
The presence of a single integer variable in the program makes it infinite-state, because the variable may take up infinitely many values. The solution to the problem is to come up with abstractions of the variable values. .
That is, instead of maintaining the exact values of the program variables, we maintain only a finite abstraction of the variable values.We first give an example of the abstract representation of variable values, and then explain how the abstraction is achieved.
Consider the program fragment in Figure 5.14 below. This program contains only one integer variable x. Suppose we want to prove that x == 0 at the end of the program. One possibility is to exactly maintain the control flow and data variable values, and check that x is indeed zero at the end of the program. The problem with this approach is that x can, in general, acquire infinitely many values—in other words, the amount of memory required to store the value of x is unbounded. Indeed, in any implementation of integer data types, a finite number of bits (say 32 or 64 bits) will be allocated to represent an integer. .
Figure 5-14. Program fragment for showing data abstraction.
In our reasoning, we do not want to be restricted by the exact implementation of integer data types, nor do we need to be. Instead, we can abstract the value of the program variables by maintaining the true/false values of certain propositions about the program variables.
Simply put, we do not maintain the exact values of the program variables; instead we only maintain the true/false answers to certain questions on the program variable values. Thus, in the preceding example, instead of maintaining the exact value of x,we might only maintain whether x == 0.
This may be denoted by a boolean variable [x == 0], which is true if x == 0 and false otherwise.With such an abstraction, building a finite-state transition system is easy.
It is a graph whose nodes are the (abstracted) program states, and each edge denotes a transition between two states via the execution of a program statement. The finite-state transition system for the following program will be as shown in Figure 5.15 below.
Figure 5.15. A program fragment and its abstracted transition system.
In the finite-state transition system shown in Figure 5.15, each program state (i.e., each node in the graph) corresponds to:
1 - The value of the program counter (i.e., where the control flow is), and
2 - The value of the boolean variable [x == 0].
In other words, the control flow in the program is represented exactly—we do not employ any abstraction there. On the other hand, while representing the value of the data variables, we do not maintain the exact values—we only maintain the true/false answers to certain questions on the program variables.
In this case, the only program variable is x, whose exact value is not maintained—instead we only maintain whether x is equal to 0. In other words, we abstract a program P with another program P’ such that
1 - The control flow in P and P’ are identical, and
2 - The only data type in program P’ is boolean, that is, all variables in program P‘ are boolean variables.
The boolean variables in program P’ are, of course, related to the data variables in program P. Indeed, each boolean variable in P’ denotes a true/false question about the variable values in program P. Given a set of true/false questions about the variables in P, deriving program P’ from program P is automatic.
Program P’ really represents a finite-state transition system that can be subjected to state space exploration via model checking. The states of the transition system correspond to
(a) the value of the program counter, and
(b) the value of the boolean variables.
Assuming that the number of possible program counter values (roughly corresponding to the number of lines in the program) is finite, and the number of boolean variables is finite, the number of states in the transition system is indeed finite.
Currently no items