DEHARBE Aurélien
Supervision : Michèle SORIA
Cosupervision : PESCHANSKI Fréderic
Resources analysis for concurrent and dynamic systems
Computer programs and systems have a growing need for dynamic resources: communication channels that are created and destroyed at will, connections to databases, memory areas, computational resources, etc. In this work, we are interested in both the qualitative and quantitative analysis of such resources in the context of concurrent and dynamic systems.
Our study is organized on the basis of a prototype programming language, named Piccolo, which was implemented in the context of the thesis. It allows one to program machines with multicore CPU using abstractions based on the picalculus process algebra. Piccolo programs are then very close to picalculus models that can be analyzed with verification tools.
In this work, we first address the issue of constructing explicit statespaces for picalculus processes. Given the expressivity of the formalism, this is in fact a nontrivial problem, especially when considering the case of labelled transition semantics. We propose a new algorithm (and a prototype tool) based on the symbolic transitions rather than the early semantics. We then observe experimentally an important reduction of the generated statespaces. We also introduce a variant of the picalculus, named slicepi, that provides an intermediate between the labelled transition semantics on the one side and the reduction semantics on the other side. This allows to "open up" some parts of a system while "keeping closed" the other parts, selectively.
The central part of the thesis is concerned with the development of a resource analysis framework for concurrent and dynamic systems. This framework is based, at the theoretical level, on a new model of automata, named nuautomata, that are a variant of the finite memory automata. They allow one to model the behavior of the systems from the point of view of their resource usage. We show how to obtain a nuautomaton from a picalculus (or slicepi) model, but their use is not restricted to the context of the process algebra. Based on this automatatheoretic foundation, we develop an algorithmic framework for the quantitative analysis of the nuautomata, and thus for the systems they model. In particular, we introduce the omniscient garbage collector (OGC) that is able to compute a worstcase minimal bound for the resource consumption of a system. A prototype tool has been developed to experiment the analysis algorithms in practice.
Defence : 09/21/2016  14h  Site Jussieu 2526/105
Jury members :
Hanna Klaudel, Université d'Évry [Rapporteur]
Daniele Varacca, Université Paris Est  Créteil [Rapporteur]
Béatrice Bérard, Université Pierre et Marie Curie
Ilaria Castellani, INRIA Sophia Antipolis
Cinzia Di Giusto, Université Nice Sophia Antipolis
Michèle Soria, Université Pierre et Marie Curie
Frédéric Peschanski, Université Pierre et Marie Curie
20142016 Publications

2016
 A. Deharbe : “Analyse statique de programmes concurrents et dynamiques”, thesis, defence 09/21/2016, supervision Soria, Michèle, cosupervision : Peschanski, Fréderic (2016)

2014
 A. Deharbe, F. Peschanski : “The Omniscient Garbage Collector : a Resource Analysis Framework”, ACSD 2014  14^{th} International Conference on Application of Concurrency to System Design, La Marsa, Tunisia, pp. 102111, (IEEE) (2014)
 A. Deharbe, F. Peschanski : “The Omniscient Garbage Collector: a Resource Analysis Framework”, (2014)