On the Existence of Network Invariants for Verifying Parameterized Systems? - Correct System Design: Recent Insights and Advances - page 178

Example A simple example of a parameterized system is the following simple
token-passing mutual exclusion algorithm. An arbitrary set of processes compete
for a critical resource. Access to the resource is modeled by a process being in its
critical section. In order to enter the critical section, a process must rst acquire
a token, which is passed in some arbitrary manner between components.

We model each process as a labeled transition system with three states: n (not
possessing the token), t (possessing the token), and c (in the critical section),
and two visible actions: send-token and rec-token . A state-transition diagram
of a process is given below:

rec-token

n c

￿￿
t

send-token

The synchronization predicate requires send-token and rec-token to occur in
synchronized pairs. In a network, all process are initialized in the state n , except
for one process, which starts in state t . There is no controller process. For this
particular example, we could imagine both an unordered and a linearly ordered
system topology (of course, any reasonable topology could be considered, but
that is not in the scope of this paper).

A correctness property for this system is mutual exclusion, formulated as the
invariant

8i 6 = j: : ( c [ i ] ^ c [ j ])

3 Methods for Verication of Invariants of Parameterized

Systems

In this section, we present the use of computational and of network invariants
in the verication of a parameterized system.

3.1 Computational Invariants

A parametrized system can be viewed as an (innite-state) program M (which

initially decides a value of ), to which standard verication methods can be

applied. A safety property in the form of an invariant can be proved in the
standard way by nding a computational (inductive) invariant for

n

. In order
to automate this method, we must nd a representation of (possibly innite)
sets of states of

M

] is nite-state, then in
the case of unstructured topology one might use constraints on the number of

M . For instance, if each component P [ i