STeP Tutorial
Verification Diagrams
Introduction
Verification diagrams provide a graphical representation of the proof
of a temporal property. Intuitively, a verification diagram depicts the
flow of the program, distinguishing the computation components that are
relevant to the property of interest. Alternatively, the verification
diagram is an abstraction of the program, such that the set of
computations of a diagram is a superset of the computations of the
system, and a subset of the set of computations that satisfy the
temporal specification. Verification conditions are used to show that
this is indeed the case. In general we have to show Initiation,
that is, all initial states are covered by the diagram, and
Consecution, that is, from every node, every transition can
go somewhere within the diagram. Additional verification conditions
are required if fairness properties are represented in the diagram.
A verification diagram is a labeled graph, where each node is labeled
with an assertion, and possibly with propositions and ranking functions,
and each edge is labeled by a set of transitions. The assertions
labeling the node denote the set of states the program can be in when
it resides in that node. The edges represent transitions from one
set of states to another (or the same). The edge labeling is used to
represent fairness properties. Informally, when an edge is labeled by
a transition, it is guaranteed that the system cannot stay forever in
the source node, without taking that transition. Edges can be labeled
only by fair transitions.
Each node has an associated set of verification conditions as follows.
For a phi-node (a node labeled by assertion phi) and transition tau,
the verification condition associated with phi and tau is given by
{phi} tau {phi1 \/phi2 \/ ..... \/ phin}
where phi1..phin are the nodes reachable from the phi-node in one
step. In
invariance, wait-for, rank and chain diagrams all nodes have
implicit selfloops and thus the verification condition then becomes
{phi} tau {phi \/ phi1 \/phi2 \/ ..... \/ phin}
These verification conditions are the consecution conditions.
The intiation condition is given by
theta --> phi1 \/ ..... \/ phik
where phi1...phik are all nodes in the diagram.
Edge labelings give rise to additional verification conditions, which
will be given in detail in the chain, rank and generalized verification
diagram tutorials.
If all the
verification conditions associated with a verification diagram hold for
a system P, we say that the diagram is P-valid. A P-valid diagram
represents a superset of the computations of P.
The propositional labeling of the nodes relate the diagram to the
formula we want to prove.
The propositions are defined by assertions (that is, a
proposition p is true iff its defining assertion a(p) is true). To
ensure that the set of computations represented by the propositional
labeling includes the set of computations represented by the
assertional labeling, we have to show for each node labeled by a
proposition that the assertion defining the proposition is implied
by the assertion labeling the node. That is, for each node labeled
with assertion q and proposition p, where p is defined by a(p), we
have to show
q --> a(p)
These verification conditions are called satisfaction conditions.
Nodes not labeled by propositions have propositional labeling true.
Thus, their associated satisfaction condition is trivially valid.
Different types
Historically different types of verification diagrams were used for
certain classes of temporal properties. Invariance diagrams
were used for invariance properties, wait-for diagrams for
nested wait-for properties, and chain and rank
diagrams for response properties. However, these diagrams could not
be used to prove properties that could not be expressed by a formula
of one of these classes. To overcome this limitation, generalized
verification diagrams were introduced, which can be used to prove any
linear-time temporal property. However, because of the convenience of
the original diagrams, which really are special cases of generalized
verification diagrams, the original diagrams are still provided in
addition to the generalized verification diagrams.
This tutorial will focus mainly on the semantics of verification diagrams
rather than on the use of the verification diagram editor, which is
explained in the
basic
tutorial. However, for those diagrams not mentioned in the basic
tutorial, we will explain the relevant user interaction.
step-comments@cs.stanford.edu
Last modified: Tue Jul 28 22:15:54 PDT 1998