The paper deals with the proof method of verification
by finitary abstraction (VFA), which presents a
feasible approach to the verification of the temporal properties of
(potentially infinitestate) reactive systems. The method consists of
a twostep process by which, in a first step, the system and its
temporal specification are jointly abstracted into a finitestate
system and a finitestate specification.
The second step uses model checking to establish the validity of the
abstracted property over the abstracted system.
The VFA method can be considered as a viable alternative to
verification by temporal deduction which, up to now, has been the main
method generally applicable for verification of infinitestate
systems.
The paper presents a general recipe for the joint abstraction, which
is shown to be sound , where soundness means that validity over the
abstract system implies validity over the concrete (original)
system. To make the method applicable for the verification of liveness
properties, pure abstraction is sometimes no longer adequate.
We show that by augmenting the system by an appropriate (and
standardly constructible) progress monitor , we obtain
an augmented system, whose computations are essentially the same as
the original system, and which may now be abstracted while preserving
the desired liveness properties. We refer to the extended method as
verification by augmented abstraction (VAA).
We then proceed to show that the VAA method is sound and complete for
proving all properties expressible by temporal logic (including both
safety and liveness).
Completeness establishes that whenever the property is valid, there
exists a finitary abstraction which abstracts the system, augmented by
an appropriate progress monitor, into a finitestate system which
validates the abstracted property.
Information and Computation, Special issue on Compositionality