We present a framework for model checking concurrent software systems
which incorporates both states and events. Contrary to other
state/event approaches, our work also integrates two powerful
verification techniques, counterexample-guided abstraction refinement
and compositional reasoning. Our specification language is a
state/event extension of linear temporal logic, and allows us to
express many properties of software in a concise and intuitive
manner. We show how standard automata-theoretic LTL model checking
algorithms can be ported to our framework at no extra cost, enabling
us to directly benefit from the large body of research on efficient
LTL verification.
We also present an algorithm to detect deadlocks in concurrent
message-passing programs. Deadlock-freedom is not only an important
and desirable property in its own right, but is also a prerequisite
for the soundness of our model checking algorithm. Even though
deadlock is inherently non-compositional and is not preserved by
classical abstractions, our iterative algorithm employs both
(non-standard) abstractions and compositional reasoning to alleviate
the state space explosion problem. The resulting framework differs in
key respects from other instances of the counterexample-guided
abstraction refinement paradigm found in the literature.
We have implemented this work in the MAGIC verification tool for
concurrent C programs and performed tests on a broad set of
benchmarks. Our experiments show that this new approach not only eases
the writing of specifications, but also yields important gains both in
space and in time during verification. In certain cases, we even
encountered specifications that could not be verified using
traditional pure event-based or state-based approaches, but became
tractable within our state/event framework. We also recorded
substantial reductions in time and memory consumption when performing
deadlock-freedom checks with our new abstractions. Finally, we report
two bugs (including a deadlock) in the source code of Micro-C/OS
versions 2.0 and 2.7, which we discovered during our experiments.
Formal Aspects of Computing 17(4), 2005. 24 pages.
PostScript /
PDF
© 2005 Springer.