A Logic-Based Approach to Model Checking of
Parameterized and
Infinite-State Systems
PhD thesis, DISI, University of Genova, June 2002
By Marco Bozzano
Abstract
The aim of this thesis is to investigate the problem of verification
for concurrent systems. In particular, a major problem in verification
is
that of validating systems, e.g. protocols, which are parametric,
in the sense that the number of entities taking part in a given run is
not
fixed a priori. Typically, such kind of systems are also
infinite-state, in that they use data structures containing
possibly
unbounded data values.
In this thesis we tackle the problem of verification using a logical
approach. In particular, the leading thread of this work will be a
specification language based on a fragment of Girard's linear logic,
which we will show to have direct connections with classical
formalisms like high-level nets or rewriting.
By combining the power of logical connectives with the flexibility of
rewriting, we are able to nicely model local and global transitions,
and to elegantly express new data generation. Reasoning on
heterogeneous
domains can also be achieved via specialized constraint solvers.
We show how this language can be used both for the specification and
the
analysis of parametric systems. In particular, we present a
verification
procedure which resembles classical symbolic model checking algorithms
for infinite-state systems, and is well-suited to study system
properties like safety, e.g. mutual exclusion.
Technically, our verification procedure uses a fixpoint computation
strategy which is based on a new bottom-up semantics for a
fragment
of linear logic. We illustrate our methodology presenting different
examples coming from concurrency theory, like a parameterized version
of the ticket mutual-exclusion protocol, and from
security, like authentication protocols.
Download: .pdf
Back to Marco Bozzano's Homepage
Last Updated: 26 August 2003