Automatically Validating Temporal Safety Properties of Interfaces

              Thomas Ball and Sriram K. Rajamani

Large-scale software has many components built by many programmers.
Integration testing of these components is impossible or ineffective
at best.  Property checking of interface usage provides a way to
partially validate such software. In this approach, an interface
provides a set of properties that all clients of the interface should
respect. An automatic analysis of the client code then validates that
it meets the properties, or provides examples of execution paths that
violate the properties.  The benefit of such an analysis is that
errors can be caught very early in the coding process.

We present a process for validating temporal safety properties of
software that uses a well-defined interface.  The process requires
only that the user state the property of interest.  It then
automatically creates abstractions of C code using iterative
refinement, based on the given property.  The process is realized in
the SLAM toolkit, which consists of a model checker, predicate
abstraction tool and predicate discovery tool. We have applied the
SLAM toolkit to Windows NT device drivers to validate critical safety
properties such as correct locking behavior.  We have found that the
process converges on a set of predicates powerful enough to validate
properties in just a few iterations.