Automatically Validating Temporal Safety Properties of Interfaces

Abstract. 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 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 a number of 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.

• Type: Conference
• Year: 2001
• Where: SPIN
• Authors: Thomas Ball, Sriram K. Rajamani
• Keywords: Safety Properties, SLAM Toolkit, SPIN 2001, Temporal Safety Properties, Theoretical Computer Science