Next: Introduction
Introduction to MSR(C)
Giorgio Delzanno
Dipartimento di Informatica e Scienze dell'Informazione
Università di Genova, Via Dodecaneso 35
16146 Genova, Italy
Abstract:
In recent works we have defined a general framework for the validation
of parameterized concurrent systems based on the combination of multiset
rewriting and constraints. The class of systems we are interested
in consists of concurrent systems parametric in the number of individual
components. Our framework provides the following features: (1) a specification
language for the class of concurrent systems taken into consideration; (2)
an assertional language to finitely represent infinite sets of configurations;
and (3) a sound and fully automatic verification method based on symbolic
state exploration. The verification procedure has been implemented in a
Constraint Logic Programming systems, namely Sicstus Prolog and the clp(Q,R)
library. CLP provides in fact all necessary operations to manipulate multisets
and constraints both as uninterpreted and interpreted objects. Operations
over constraints are delegated in fact to the clp(Q,R) library, and encapsulated
into Sicstus Prolog predicates. The method can be applied to solve validation
problems for communication protocols, and (potentially) of security and authentication
protocols and abstractions of concurrent programs. In this paper we overview
the main features of our framework and comment on some of the more interesting
applications.
Next: Introduction
Giorgio Delzanno 2003-02-03