## Temporal Verification by Diagram Transformations

*
Luca de Alfaro,
Zohar Manna,
*
This paper presents a methodology for the verification of temporal
properties of systems based on the gradual construction and
algorithmic checking of *fairness diagrams*. Fairness diagrams
correspond to abstractions of the system and its progress properties,
and have a simple graphical representation.

In the proposed methodology, a proof of a temporal property consists of
a chain of diagram transformations, starting from a diagram representing
the original system and ending with a diagram that either corresponds
directly to the specification, or that can be shown to satisfy it by
purely algorithmic methods. Each diagram transformation captures a
natural step of the gradual process of system analysis and proof
discovery. The structure of fairness diagrams simplifies reasoning
about progress properties, and the graphical representation provided
by the diagrams enables the user to direct the construction of the
proof. The resulting methodology is complete for proving specifications
written in first-order linear-time temporal logic, provided no
temporal operator appears in the scope of a quantifier.

In *8th International Conference on Computer-Aided Verification*,
LNCS vol. 1102, pp. 287-299, Springer-Verlag, July 1996.

Postscript,
PDF.
© 1996, Springer Verlag.

Last modified: Thu Mar 29 18:21:49 PST 2001