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

On the Existence of Network Invariants for
Verifying Parameterized Systems ?

Parosh Aziz Abdulla and Bengt Jonsson

Dept. Computer Systems Uppsala University
P.O.Box 325, 751 05 Uppsala, Sweden
f parosh,bengt g @docs.uu.se

Abstract. Over the last decade, nite-state verication methods have
been developed to an impressive tool for analysis of complex programs,
such as protocols and hardware circuits. Partial-order reduction and
BDD-based symbolic model checking have been instrumental in this de-
velopment. Currently, much eort is devoted to advancing further the
power of automated verication to cover also innite-state systems. In
this paper, we consider the class of so-called parameterized systems , i.e.,
systems with many similar processes, in which the number of processes is
unbounded and their interconnection pattern may vary within the range
of some constraints. We partially review the use of induction over the
system structure for the verication of parameterized systems. Wolper
and Lovinfosse have introduced the term network invariant for the in-
duction hypothesis in such a proof by induction. They also observe that
well-behaved (e.g., nite-state) network invariants do not always exist,
even if the system itself satises the property to be veried. The main
contribution of the paper is to present some sucient conditions, under
which the existence of a nite-state network invariant is guaranteed. We
also relate the construction of network invariants to the search for stan-
dard inductive invariants. Two small examples of network invariants and
standard invariants for parameterized systems are included.

1 Introduction

One of the advantages of producing formal models of algorithms and systems
is the possibility to analyze and verify them in a rigorous way, in the best case
totally automatically by computer. For nondeterministic and parallel programs,
relevant verications include absence of deadlocks, or proving that all executions
of a program satisfy a desirable property expressed in temporal logic. Over the
last decade, impressive tools have been developed for verication of nite-state
systems. Partial-order reduction and BDD-based symbolic model checking have
been instrumental in this development.
? Supported in part by the Swedish Board for Industrial and Technical Development
(NUTEK) and by the Swedish Research Council for Engineering Sciences (TFR).