| Abstract |
We investigate the foundations of the specification language MSR(C),
that combines multiset rewriting over first order atomic formulas
and a generic constraints system C, and of a corresponding verification
procedure for checking safety properties.
Our method has been applied to the analysis of
mutual exclusion, cache coherence and security protocols.
All the case-studies belong to a class of concurrent systems for which
verification is often undecidable.
Indeed their state-space is infinite in more than one dimension:
they are parametric in the number of components (processes/sessions) and
have local data defined over infinite domains.
Our verification procedure is based on symbolic backward exploration.
Infinite sets of configurations of an MSR(C) specification
are represented symbolically via assertions defined over multisets and constraints.
Constraints and term manipulation operations are combined together in order to
effectively manipulate assertions.
All operations are defined for a generic constraint system C.
By a careful choice of the constraints system and of the syntax
of rules, we isolate a new class of constraint multiset rewriting specifications
(hence of infinite-state systems) for which verification of safety
properties is decidable.
Decidability is obtained by applying the theory of well and better quasi orderings.
|
