## Modularization and Abstraction: The Keys to Formal Verification

*
Y. Kesten, and
A. Pnueli*
In spite of the impressive progress in the development of the two main
methods for formal verification of reactive systems -- Model Checking
(in particular symbolic) and Deductive Verification, they are still
limited in their ability to handle large systems. It is generally
recognized that the only way these methods can ever scale up is by
the extensive use of abstraction and modularization, which breaks the
task of verifying a large system into several smaller tasks of
verifying simpler systems.

In this methodological paper, we review the two main tools of
compositionality and abstraction in the framework of linear temporal
logic. We illustrate the application of these two methods for the
reduction of an infinite-state system into a finite-state system that
can then be verified using model checking.

The modest technical contributions contained in this paper are a full
formulation of abstraction when applied to a system with both weak and
strong fairness requirements and to a general temporal formula, and
a presentation of a compositional framework for shared variables and
its application for forming {\em network invariants}.

L. Brim, J. Gruska, and J. Zlatuska, editors,
*The 23rd International Symposium on Mathematical Foundations of
Computer Science* (MFCS 1998), volume 1450
of *Lecture Notes in Computer Science*, pages
54-71. Springer-Verlag, 1998.

PostScript updated, improved, and extended text.
© 1998 Springer-Verlag.