Abstraction-based verification of parameterized networks
The thesis presents a method to verify parameterized networks of finite state processes. The method is based on three main ideas. The first one consists in modeling an infinite family of networks by a single WS1S transition system, that is, a transition system whose variables are set (2nd-order) variables and whose transitions are described in WS1S. Then, we present methods that allow to abstract a WS1S system into a finite state system that can be model-checked. Finally, in order to verify liveness properties, we present an algorithm that allows to enrich the abstract system with strong fairness conditions while preserving safety of the abstraction. We prove applicability of the method by verifying several examples. Moreover, we present generalizations that allow to verify networks of processes with unbounded state space or networks with tree topologies.