Room 206 (2nd floor, badged access)
4 avril 2019 - 14h00
Checking Deadlock-Freedom of Parametric Component-Based Systems
par Radu IOSIF de VERIMAG
Abstract: We consider concurrent systems consisting of a finite but unknown number of components, that are replicated instances of a given set of finite state automata. The components communicate by executing interactions which are simultaneous atomic state changes of a set of components. We specify both the type of interactions (e.g. rendez-vous, broadcast) and the topology (i.e. architecture) of the system (e.g. pipeline, ring) via a decidable interaction logic, which is embedded in the classical weak sequential calculus of one successor (WS1S). Proving correctness of such system for safety properties, such as deadlock freedom or mutual exclusion, requires the inference of an inductive invariant that subsumes the set of reachable states and avoids the unsafe states. Our method synthesizes such invariants directly from the formula describing the interactions, without costly fixed point iterations. We applied our technique to the verification of several textbook examples, such as dining philosophers, mutual exclusion protocols and concurrent systems with preemption and priorities.
This is joint work with Marius Bozga and Joseph Sifakis. A short version of this talk will be presented at TACAS'19
