Structural Invariants for the Verification of Systems
with Parameterized Architectures
Marius Bozga 1 , Javier Esparza 2 , Radu Iosif 1 , Joseph Sifakis 1
and Christoph Welzel 2
1 Univ. Grenoble Alpes, CNRS, Grenoble INP , Verimag
2 Technische Universit¨ at M¨ unchen
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. rendez-vous, broadcast) and the topology of the system (e.g. pipeline,
ring). The logic can be easily embedded in monadic second order 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 safety properties of a large number of systems, including
textbook examples (dining philosophers, synchronization schemes), classical mutual
exclusion algorithms, cache-coherence protocols and self-stabilization algorithms, for
an arbitrary number of components.
1 Introduction
The problem of parameterized verification asks whether a system composed of n replicated processes is safe, for all n ≥ 2. By safety we mean that every execution of the
system stays clear of a set of global error configurations, such as deadlocks or mutual
exclusion violations. Even if we assume each process to be finite-state and every interaction to be a synchronization of actions without exchange of data, ranging over large or
infinite domains, the problem remains challenging because we ask for a general proof
of safety that works for any number of processes.
Parameterized verification is undecidable, even if processes only manipulate data
from a bounded domain [6]. Various restrictions of communication and architecture 3
define decidable subproblems [18,31,27,5]. Seminal works consider rendez-vous communication, with participants placed in a ring [18,27] or a clique [31] of arbitrary size.
Recently, MSO-definable graphs (with bounded tree- and clique-width) and point-topoint rendez-vous communication have been considered [5]. Most approaches to define decidable problems focus on manually proving a cut-off bound c ≥ 2 such that
Institute of Engineering Univ. Grenoble Alpes
3 We use the term architecture for the shape of the graph along which the interactions take place.
c
The Author(s) 2020
A. Biere and D. Parker (Eds.): TACAS 2020, LNCS 12078, pp. 228–246, 2020.
https://doi.org/10.1007/978-3-030-45190-5 13
TACAS
Evaluation
Artifact
2020
Accepted
with Parameterized Architectures
Marius Bozga 1 , Javier Esparza 2 , Radu Iosif 1 , Joseph Sifakis 1
and Christoph Welzel 2
1 Univ. Grenoble Alpes, CNRS, Grenoble INP , Verimag
2 Technische Universit¨ at M¨ unchen
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. rendez-vous, broadcast) and the topology of the system (e.g. pipeline,
ring). The logic can be easily embedded in monadic second order 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 safety properties of a large number of systems, including
textbook examples (dining philosophers, synchronization schemes), classical mutual
exclusion algorithms, cache-coherence protocols and self-stabilization algorithms, for
an arbitrary number of components.
1 Introduction
The problem of parameterized verification asks whether a system composed of n replicated processes is safe, for all n ≥ 2. By safety we mean that every execution of the
system stays clear of a set of global error configurations, such as deadlocks or mutual
exclusion violations. Even if we assume each process to be finite-state and every interaction to be a synchronization of actions without exchange of data, ranging over large or
infinite domains, the problem remains challenging because we ask for a general proof
of safety that works for any number of processes.
Parameterized verification is undecidable, even if processes only manipulate data
from a bounded domain [6]. Various restrictions of communication and architecture 3
define decidable subproblems [18,31,27,5]. Seminal works consider rendez-vous communication, with participants placed in a ring [18,27] or a clique [31] of arbitrary size.
Recently, MSO-definable graphs (with bounded tree- and clique-width) and point-topoint rendez-vous communication have been considered [5]. Most approaches to define decidable problems focus on manually proving a cut-off bound c ≥ 2 such that
Institute of Engineering Univ. Grenoble Alpes
3 We use the term architecture for the shape of the graph along which the interactions take place.
c
The Author(s) 2020
A. Biere and D. Parker (Eds.): TACAS 2020, LNCS 12078, pp. 228–246, 2020.
https://doi.org/10.1007/978-3-030-45190-5 13
TACAS
Evaluation
Artifact
2020
Accepted