Structural Invariants for the Verification of Systems with Parameterized Architectures

We consider parameterized concurrent systems consisting of a finite but unknown number of components, obtained by replicating a given set of finite state automata. Components communicate by executing atomic interactions whose participants update their states simultaneously. We introduce an interaction logic to specify both the type of interactions (e.g. rendezvous , broadcast) and the topology of the system (e.g. pipeline, ring). The logic can be easily embedded in monadic second logic of κ ≥ 1 successors (WSκS), and is therefore decidable. Proving safety properties of such a parameterized system, like deadlock freedom or mutual exclusion, requires to infer an inductive invariant that contains all reachable states of all system instances, and no unsafe state. We present a method to automatically synthesize inductive invariants directly from the formula describing the interactions , without costly fixed point iterations. We experimentally prove that this invariant is strong enough to verify many textbook examples, such as dining philosophers, mutual exclusion protocols, and concurrent systems with preemption and priorities, for an arbitrary number of components