Introduction

In this paper we describe a general framework for the automatic verification of concurrent systems parametric in the number of individual components. Our framework extends multiset rewriting over first order atomic formulas (MSR), a paradigm proposed in [11], with the notion of constraints peculiar of Constraint Logic Programming [22]. While multiset rewriting allows to specify concurrent processes in a natural way, constraints can be used to declaratively represent the relationship among their internal data. The combination of multisets and constraints is also important to define symbolic data structures to represent infinite sets of system configurations. The relationship between multiset rewriting and concurrency can be well illustrated by reasoning in terms of Petri Nets. Petri Nets can be viewed in fact as multiset rewriting systems defined over a finite alphabet $\Sigma$. The symbols in $\Sigma$ represent the set of places of a Petri Net. A Petri Net marking can be modeled as a multiset of symbols from $\Sigma$: $k$ occurrences of the symbol $p$ in the multiset correspond to $k$ tokens in the place $p$. As a consequence, Petri Net transitions can be modeled as multiset rewriting rules over symbols in $\Sigma$. Finally, a sequence of rewriting steps can be viewed as the sequence of markings generating by an execution of the corresponding Petri Net. Multiset rewriting over first-order atomic formulas (MSR) [11] naturally extends this connection to Petri Nets with colored tokens, the colors being first-order terms attached to atomic formulas representing tokens. It is important to note that in this setting rewriting is restricted to multisets of atomic formulas only. Intuitively, a multiset of atomic formulas is interpreted as a pool of active and concurrently executing processes. Atomic formulas denote the current state of individual processes. In [14,8], we proposed a generalization of the MSR formalism in which multiset rewriting rules (over first-order atomic formulas) are annotated with constraints. The resulting language scheme, called MSR(${\mathscr C}$), is parametric on the constraint system ${\mathscr C}$. MSR(${\mathscr C}$) provides a clear separation between process structure and declarations of data relations. One of the advantages of this conceptual separation is a major modularity of the resulting specifications. The logic obtained by combining multisets and constraints can be naturally used to reason about system properties. Specifically, several correctness properties can be verified by searching for error traces following the so-called backward reachability search scheme. The idea here is to first isolate the set of configurations that represent possible violations and then to generate all possible preconditions for those configurations to occur. If the initial states do not satisfy any of those preconditions than the violations will never occur, and thus the system is proved to be correct. A particularly interesting class of safety properties are those whose violations can be expressed via upward-closed sets of configurations, i.e., that can be represented via minimal violations. Our symbolic representation of upward-closed sets of configurations is based on the notion of constrained configuration introduced in [14] to deal with asynchronous systems, i.e. multisets of first-order atomic formulas, annotated with constraints. Multisets represent minimal requirements about the distribution of tokens in the net, whereas constraints provide a natural symbolic representation for relations over data of different processes. Based on this rich assertional language, we provide symbolic operations needed to implement backward reachability, namely we define a symbolic predecessor operator, which is sound and complete for any constraint system. The interest of this method is that allows to study properties that do not depend on the number of processes generated during a computation. We will clarify this point in this survey by discussing the application to a mutual exclusion protocol designed for client-server systems in which the number of clients is not bounded a priori. We have implemented our automated verification method and applied it to analyze several practical case-studies. In general the method works without guarantees of termination. However, several techniques like static analysis and abstract interpretation can be applied to enforce termination on specific case studies. Furthermore, soundness ensures that error-traces will eventually be found: the prototype we used to implement the method performs a breadth-first symbolic backward exploration of the state space. Termination can be shown only for special subclasses of MSR(${\mathscr C}$)-specifications [15]. As an implementation platform we have used a Constraint Logic Programming system, namely the clp(Q,R) library of Sicstus Prolog. CLP provides built-in operations and data structures to implement multiset-based operations (unification, efficient list representations and operations). Furthermore, it allows to handle constraints both as interpreted and uninterpreted objects. When queried, the clp(Q,R) solver provides operations like satisfiability, entailment, and projections that (via the encapsulation predicates peculiar of Sictus Prolog) can be embedded into procedure used for symbolic backward search. In this paper we will give an overview of the general framework, the corresponding verification methodology. Finally, we will discuss issues about the CLP implementation and some of practical applications of the framework.