|
|||||||||||
 |
|||||||||||
|
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 Review Meeting, Februrary 15, 2005, Arlington, Virginia. Presentations.
- MURI Review Meeting, August 16, 2004, Annapolis, Maryland. Presentations.
- MURI Review Meeting, November 12-13, 2003, Baltimore, Maryland Details. Presentations
- MURI Review Meeting, July 22-23, 2003, Pittsburgh, PA. Details. Presentations.
MURI Documents Search:
 |
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