Compositional Verification by Model Checking for Counter-Examples
Compositional Verification by Model Checking for Counter-Examples
Files
Publication or External Link
Date
1998-10-15
Authors
Tevfik Bultan ,
Fischer, Jeffrey
Gerber, Richard
Advisor
Citation
DRUM DOI
Abstract
Many concurrent systems are required to maintain certain safety and
liveness properties. One emerging method of achieving confidence in such
systems is to statically verify them using "model checking". In this
approach an abstract, finite-state model of the system is constructed;
then an automatic check is made to ensure that the requirements are
satisfied by the model. In practice, however, this method is limited by
the "state space explosion problem".
We have developed a compositional method that directly addresses this
problem in the context of multi-tasking programs. Our solution depends on
three key space-saving ingredients: (1) checking for counter-examples,
which leads to simpler search algorithms; (2) automatic extraction of
interfaces, which allows a refinement of the finite model -- even before
its communicating partners have been compiled; and (3) using propositional
"strengthening assertions" for the sole purpose of reducing state space.
In this paper we present our compositional approach, and describe the
software tools that support it.
(Also cross-referenced as UMIACS-TR-95-98)