Next: Implementation in CLP
Up: An Overview of MSR():
Previous: Symbolic Representation via Constrained
A Symbolic Verification Procedure
The next step toward an effective verification procedure consists
of defining a symbolic predecessor operator working on the
assertional language according to the rich denotation described in the previous section.
Let us first
introduce the notion of unification between two multisets of
atomic formulas (with distinct variables).
Firstly, given two atomic formulas
and
, we use as a shorthand for the
constraint
, provided and
. Unification is defined then as follows.
Below, given (e.g., a rule, constraint, or constrained
configuration) we call a variant of if is
obtained applying a renaming to , i.e. (a
renaming is a mapping from variables of to fresh
variables).
Let us give an example of application.
The new operator enjoys the following property.
In order to define a symbolic reachability algorithm,
we still need a comparison operator
between constrained configurations. We discuss next the general
requirements it should satisfy.
Based on this definition, we can define a symbolic backward
reachability procedure that we can use to check safety properties
whose negation can be expressed via an upward closed set of
configurations. We can rephrase the backward reachability
algorithm (which is parametric on the constraint system
and entailment relation ) in our setting, as follows.
Figure 6:
Symbolic Backward Reachability
|
In general, the algorithm is not terminating, since it is possible
to encode undecidable reachability problems (e.g. for two counter
machines) as verification problems of generic
specifications. However, following [1,18], if we can
prove that is a well-quasi ordering, then the
previous procedure turns out to be a complete algorithm to compute
. In order to check that a safety properties
holds we also need that the emptiness test for the
intersection with the initial states is decidable.
Next: Implementation in CLP
Up: An Overview of MSR():
Previous: Symbolic Representation via Constrained
Giorgio Delzanno
2003-02-03