The paper considers the problem of uniform verification of
parameterized systems by symbolic model checking, using formulas in
FS1S (a syntactic variant of the 2nd order logic WS1S) for the symbolic
representation of sets of states. The technical difficulty addressed in this
work is that, in many cases, standard modelchecking computations fail
to converge.
Using the tool tlv[P], we formulated a general approach to the
acceleration
of the transition relations, allowing an unbounded number of different
processes to change their local state (or interact with their neighbor)
in a single step. We demonstrate that this acceleration process solves
the difficulty and enables an efficient symbolic modelchecking of many
parameterized systems such as mutualexclusion and tokenpassing pro
tocols for any value of N, the parameter specifying the size of
the system.
Most previous approaches to the uniform verification of parameterized
systems, only considered safety properties of such systems. In
this paper, we present an approach to the verification of liveness
properties
and demonstrate its application to prove accessibility properties of the
considered protocols.
Proc. 12th Conference on Computer Aided Verification