Date : Nov. 27th 2003 © PolySpace Technologies 1/8 STATIC VERIFICATION OF DYNAMIC PROPERTIES Dr. Alain Deutsch Chief Technical Officer PolySpace Technologies ABSTRACT This paper is a tutorial on the principles and applications of static verification of dynamic properties to development, verification and validation of embedded applications. The topics covered include what static verification of dynamic properties is, how it works, how it can help in verification and validation activities. It will also present an industrial tool for the automatic detection of run-time errors. 1. INTRODUCTION The principles of static verification of dynamic properties are based on a paradigm that is at the heart of other engineering activities. Activities such as designing a bridge, computing the trajectory of a satellite or optimizing the shape of a plane wing are all based on applied mathematics, whose use is facilitated by high-speed processors. If we want to formalize this statement, we would say that all these engineering activities are based on a central paradigm that consists of a three-step method: ! Modeling a physical world system as a set of mathematical equations ! Solving these equations using high-speed processors ! Using the solutions to these equations to predict the behavior of the physical system However, there is one engineering activity that has not yet fully benefited from this paradigm when it comes to verification and validation: software engineering. Indeed, software validation is still often mostly based on test techniques which consist in enumeratively executing the application a high number of times. If you succeed in running a high enough number of executions without observing any error, then the software is considered validated. Unfortunately this does not imply that the software is free of run-time errors. Indeed, detecting a run-time error during tests requires: 1. Executing the right statement during tests … 2. … with the right combination of values (as mere execution of the statement may not be enough) … 3. …and detect the error if it occurs (as triggering the error may not be enough) Even achieving 100% statement coverage during tests may not be enough to detect all errors. We thus propose to adopt a new approach to software validation: the use of methods based on applied mathematics such as static verification of dynamic properties. 2. WHAT IS STATIC VERIFICATION OF DYNAMIC PROPERTIES? Static verification of dynamic properties is a software analysis technique that is based on data-flow analysis. Data-flow analysis is a branch of computer science which aims to statistically compute program properties. It is basically done inDate : Nov. 27th 2003 © PolySpace Technologies 2/8 two steps: translating programs into equations over lattices and then solving these equations by fixed-point iterations. It is now widely used in modern compilers for code optimization purposes. It was pioneered by Kildall in 1973 [1]. Here are a few examples of program-point specific properties computable by data-flow analysis used in optimizing compilers: ! A first example is the computation of live variables. The basic idea is to determine a set of variables that will be possibly used in the future so as to be able to allocate the same register to variables that are not simultaneously live. ! A second example is constant propagation. Here the aim is to replace reads of variables which always have the same value at a given point by a constant. ! A third example is computing available expressions. It consists in determining a set of expressions that are always evaluated in the past and so to proceed to Common Subexpression Elimination (CSE). Similarly, determining very busy expressions – a set of expressions which will always be evaluated in the future allows loop invariant elimination and code motion. Those are all examples of what is currently done through the use of traditional data-flow analysis. On the other hand, static verification of dynamic properties extends data-flow analysis by providing an additional theoretical framework that allows the mathematical justification of data-flow analyzers, the design of new data-flow analyses and the handling of particular infinite sets of properties ([2], [3] and [4]). To further describe how static verification of dynamic properties works, we now consider a simple flowchart language as an example. This consists in: ! 32 bits integer variables and integers; ! arithmetic operations; ! assignments; ! conditionals and loops. In this language, states are pairs consisting of: ! An integer representing the current flowchart instruction to be executed ! A vector of integers in a n-dimensional state where n is the number of variables in program P We define what strongest global invariants SGI(k) are: SGI(k) is the set of all possible states that are at program point k and reachable in program P. For the flowchart language defined previously, it is a set of points in an n dimensional space. A run-time error is then triggered when SGI(k) intersects a forbidden zone. SGI(k) is the result of formal proof methods, or it can be expressed as least fixed-points of a monotonic operator on the lattice of a set of states. SGI(k) may thus be seen as the solution of a system of equations whose unknowns are sets of states. We use the Floyd/Park/Clarke method [5], [6] and [7] as follows: Step 1: Translate program P to a system: X1 = F1(X1,…,Xm) X2 = F2(X1,…,Xm) … Xm = Fm(X1,…,Xm) Step 2: Compute the least solution (V1,…,Vm) We do this by using a Kleene ascending sequence: Xi,0 =∅ Xi,k+1=Fi(X1,k,…,Xm,k) We now define the result: SGI(p)=Vp Let us consider an example of such a computation with the following program: K=ioread_i32(); 1. I=2; 2. J=K+5; 3. while (I<10) { 4. I=I+1; 5. J=J+3;Date : Nov. 27th 2003 © PolySpace Technologies 3/8 6. } 7. 8. … / (I-J) Here the non-obvious risk is a divide-by-zero. That is what we are going to check with the Floyd/Park/Clarke method. Step 1: Translate program P to a system We get the following set of equations: X0={(0,0,k) I k∈[-231,231-1]} X1={(2,j,k) I (i,j,k) ∈ X0} X2={(i,k+5,k) I (i,j,k) ∈ X1} X3= X2 ∪ X6 X4={(I+1,j,k) I (i,j,k) ∈ X3, i<10} X5={(i,j+3,k) I (i,j,k) ∈ X4} X6= X5 X7={(i,j,k) I (i,j,k) ∈ X3, i ≥10} X8={(i,j,k) I (i,j,k) ∈ X7, i-j≠0} Xerror={(i,j,k) I (i,j,k) ∈ X7, i-j =0} Step 2: Compute the least solution