Model Checking is a method for verifying properties of finite-state concurrent systems. In model checking, specifications are expressed in temporal logic, a formalism for reasoning about the ordering of events in time without introducing time explicitly. The concurrent system is modeled by a finite-state machine. An efficient state-space exploration procedure is used to determine automatically if a specification is satisfied by the state-machine model. If the specification is not satisfied, a counterexample execution trace is generated that shows why the specification is not satisfied. Without employing a formally based technique such as model checking, the tools available for establishing whether a system assembled from a collection of components possesses, or does not possess, a given property can only be addressed informally, and hence, unreliably.
Model checking has been applied successfully for hardware designs and various kinds of protocols. Many features of software including dynamic thread creation, heap storage allocation and destructive updating of structure fields, however, create considerable difficulties for any method that tries to check program properties. Because of the complexity of the situation, it is necessary to harness the results that have been obtained in recent years in the static-analysis community.
The CMU-Wisconsin software model checking project will employ methods both from static analysis and from model checking to verify properties of software. In particular, we will employ static analysis as a tool to construct abstract models on which model checking will be performed subsequently.
The project’s quadchart (updated 09/04): MURI Conference Working Group
MURI Documents Search: