Specification and Safety Verification of Parametric Hierarchical Distributed Systems

We introduce a term algebra as a new formal specification language for the coordinating architectures of distributed systems consisting of a finite yet unbounded number of components. The language allows to describe infinite sets of systems whose coordination between components share the same pattern, using inductive definitions similar to the ones used to describe algebraic data types or recursive data structures. Further, we give a verification method for the parametric systems described in this language, relying on the automatic synthesis of structural invariants that enable proving general safety properties (absence of deadlocks and critical section violations). The invariants are defined using the WS.S fragment of the monadic second order logic, known to be decidable by a classical automata-logic connection. This reduces the safety verification problem to checking satisfiability of a WS.S formula. We implemented the invariant synthesis method into a prototype tool and carried out verification experiments on a number of non-trivial models specified using the term algebra.