Why PolySpace Verification Uses Approximations
What is Static Verification
PolySpace software uses static verification to
prove the absence of runtime errors. Static verification derives the
dynamic properties of a program without actually executing it. This
differs significantly from other techniques, such as runtime debugging,
in that the verification it provides is not based on a given test
case or set of test cases. The dynamic properties obtained in the
PolySpace verification are true for all executions of the software.
PolySpace verification works by approximating the software under
verification, using safe and representative approximations of software
operations and data.
For example, consider the following code:
for (i=0 ; i<1000 ; ++i)
{ tab[i] = foo(i);
}To check that the variable 'i' never overflows the range of
'tab' a traditional approach would be to enumerate each possible value
of 'i'. One thousand checks would be needed.
Using the static verification approach, the variable 'i' is
modelled by its variation domain. For instance the model of 'i' is
that it belongs to the [0..999] static interval. (Depending on the
complexity of the data, convex polyhedrons, integer lattices and more
elaborated models are also used for this purpose).
Any approximation leads by definition to information loss. For
instance, the information that 'i' is incremented by one every cycle
in the loop is lost. However the important fact is that this information
is not required to ensure that no range error will occur; it is only
necessary to prove that the variation domain of 'i' is smaller than
the range of 'tab'. Only one check is required to establish that –
and hence the gain in efficiency compared to traditional approaches.
Static code verification does have an exact solution, but that
solution is generally not practical, as it would generally require
the enumeration of all possible test cases. As a result, approximation
is required.
Back to Top
Exhaustiveness
Nothing is lost in terms of exhaustiveness. The reason is that
PolySpace works by performing upper approximations. In other words,
the computed variation domain of any program variable is always a
superset of its actual variation domain. The direct consequence is
that no runtime error (RTE) item to be checked can be missed by PolySpace.
Back to Top
 | Approximations Used During Verification | | Approximations Made by PolySpace Verification |  |
Store 
