In spite of the impressive progress in the development of the two main
methods for formal verification of reactive systems -- Symbolic Model
Checking 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 break the task of verifying a
large system into several smaller tasks of verifying simpler
systems.
In this 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
infinitestate system into a finitestate system that can then be
verified using model checking.
The 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 network invariants.
International Journal on Software Tools for Technology Transfer (STTT)