CMU logo Wisconsin logo

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

Recent Events

  • MURI Review Meeting, November 30, 2005, Pittsburgh, PA. Presentations.

Past Events

MURI Documents Search:

Google


This project is funded by the Office of Naval Research under the Critical Infrastructure Protection and High Confidence, Adaptable Software (CIP/SW)  Research Program of the URI.

Project Manager: Dr. Ralph F. Wachter.

 


CMU-SCS Model Checking home page

 

     Please send any comments or suggestions about this website to Nishant Sinha or Stephen Magill.