Deductive Verification of Modular Systems

Bernd Finkbeiner, Zohar Manna, Henny Sipma

Effective verification methods, both deductive and algorithmic, exist for the verification of global system properties. In this paper, we introduce a formal framework for the modular description and verification of parameterized fair transition systems. The framework allows us to apply existing global verification methods, such as verification rules and diagrams, in a modular setting. Transition systems and transition modules can be described by recursive module expressions, allowing the description of hierarchical systems of unbounded depth. Apart from the usual {\em parallel composition}, {\em hiding} and {\em renaming} operations, our module description language provides constructs to {\em augment} and {\em restrict} the module interface, capablilities that are essential for recursive descriptions. We present proof rules for property inheritance between modules. Finally, {\em module abstraction} and induction allow the verification of recursively defined systems. Our approach is illustrated with a recursively defined arbiter for which we verify mutual exclusion and eventual access.

Appeared in Compositionality: The Significant Difference, LNCS 1536, Springer Verlag, 1998.

Postscript, PDF. © 1998, Springer Verlag.

Last modified: Thu Mar 29 10:29:12 PST 2001