virtual seminar on zoom (see below)
20 novembre 2020 - 10h30
Structural Invariants for the Verification of Systems with (Recursively Defined) Parameterized Architectures
par Radu Iosif de VERIMAG/CNRS
Abstract: MOHYTOS Seminar
Zoom link https://us04web.zoom.us/j/76351337050?pwd=Z3JibVkw
Passcode: 7kFz1i
Joint work with Marius Bozga, Joseph Sifakis (VERIMAG), Javier Esparza and Christoph Welzel (TU Munich)
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). Proving safety properties of such a parameterized system, like deadlock freedom or mutual exclusion, requires inferring 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. 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. 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.
If time allows, in the second part of this talk I will describe 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.
