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 have implemented this work within our
concurrent C model checker, MAGIC, and checked a number of properties
of OpenSSL-0.9.6c (an open-source implementation of the SSL protocol)
and Micro-C/OS version 2 (a real-time operating system for
embedded applications). 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 report a bug
in the source code of Micro-C/OS version 2, which was found during our
experiments.
Proceedings of IFM 04, LNCS 2999, 2004. 20 pages.
PostScript /
PDF
© 2004
Springer-Verlag.