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.