Verifying Safety Properties of Inductively Defined Parameterized Systems

TL;DR

This paper presents a new formal language based on term algebra for specifying and verifying safety properties of parameterized distributed systems with an unbounded number of components, using automata-theoretic methods.

Contribution

It introduces a novel specification language for infinite system families and a verification approach using decidable logic fragments and automata theory.

Findings

Automated synthesis of structural invariants for safety verification

Reduction of safety verification to WSkS satisfiability checking

Applicability to systems with unbounded components

Abstract

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 (mutual exclusion, absence of deadlocks). The invariants are defined using the WSkS 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 WSkS formula.