Soutenance d'habilitation à diriger des recherches de Gwen Salaün
Gwen Salaün soutiendra le 22 novembre 2011 à 14 h
une habilitation à diriger des recherches de l'Université de Grenoble,
"Process Calculi: Bridges and Application to Distributed Systems"
COMPOSITION DU JURY :
La soutenance sera naturellement suivie d'un pot, à côté de l'amphithéâtre, auquel vous êtes tous cordialement invités.
Process calculi are abstract description languages for specifying concurrent systems. The process algebra community has proposed many different calculi in the last 25 years, and implemented several toolboxes to support the verification of systems specified with them. However, although they are based on the same kernel of operators, there is no connection between these calculi and there are very few bridges between existing verification toolboxes. I will present some translations between process calculi in order to reduce the gap between these formalisms and to provide some bridges between existing toolboxes to make their combined use possible.
Formal techniques and tools are well established for designing critical systems. However, they are seldom used by engineers for the design and development of more conventional software. I will present some applications of formal methods to building and verifying distributed applications. I will present first how process algebraic techniques have been successfully applied to the verification of cloud computing protocols. Second, I will show how they can be very helpful in supporting the construction of distributed systems by reusing and composing existing components and services. More precisely, I will present some model-based techniques for compatibility checking, adaptor generation, and checking the realizability of choreography specifications.