CIVIT Pierre

PhD graduated
Team : NPA
Departure date : 01/16/2023

Supervision : Maria POTOP-BUTUCARU

Specification of dynamic probabilistic secure distributed systems

This thesis proposes a natural hierarchical model for dynamic probabilistic distributed systems. The model extends in an intuitive way the labeled transition systems that best capture the intuition of an object moving from one state to another. The model consists of 3 essential ingredients: (1) a parallel composition operation, noted ||, allowing to represent a new object A||B resulting from the interaction between two objects A and B, (2) a pre-order relation <=, where A <= B means that the object A implements the object B in the sense of an observational semantics, (3) the composability property for <=, that is A <= B implies C||A <= C||B, (4) a hierarchical structure, i.e. a system X, composed of objects interacting with each other and able to join and leave the system dynamically, is also an object of the model.
Furthermore, the thesis discusses the conditions to obtain (5) the monotonicity (with <=) of dynamic creation/destruction of objects, i.e., if (i) A <= B and (ii) X_A and X_B differ only by the fact that X_A dynamically creates and destroys the object A instead of dynamically creating and destroying the object B as X_B does, then (iii) X_A <= X_B. The model is declined in several variants: asynchronous, timed, bounded and allows a modular design and a refinement methodology based only on the notion of externally

Defence : 12/15/2022

Jury members :

Paul ATTIE, Professeur, Augusta University [Rapporteur]
Stephan MERZ, Chercheur senior, INRIA Nancy [Rapporteur]
Damien VERGNAUD, Professeur, Sorbonne Université
Hagit ATTIYA, Professeure, Technion University
Vincent GRAMOLI Professeur Associé, University of Sydney
Rachid GUERRAOUI Professeur, EPFL
Achour MOSTEFAOUI Professeur, Nantes Université
Maria POTOP-BUTUCARU, Professeure, Sorbonne Université

Departure date : 01/16/2023

2022 Publications