Soutenance d'habilitation à diriger des recherches de Gwen Salaün

Gwen Salaün soutiendra le 22 novembre 2011 à 14 h
au Grand Amphithéâtre de l'INRIA Rhône-Alpes
655, avenue de l'Europe 38330 Montbonnot Saint Martin

une habilitation à diriger des recherches de l'Université de Grenoble,
intitulée :

"Process Calculi: Bridges and Application to Distributed Systems"

COMPOSITION DU JURY :

• M. Roland Groz, professeur, Grenoble INP (président du jury)
  
• M. Farhad Arbab, directeur de recherche, CWI, Amsterdam (rapporteur)
  
• Mme Marie-Claude Gaudel, professeur émerite à l'Université de Paris-Sud (rapporteur)
  
• M. Gianluigi Zavattaro, maître de conférences à l'Université de Bologne (rapporteur)
  
• M. Jeff Magee, professeur à l'Imperial College, Londres (examinateur)
  
• M. Jean-Bernard Stefani, directeur de recherche INRIA (examinateur)
  

La soutenance sera naturellement suivie d'un pot, à côté de l'amphithéâtre, auquel vous êtes tous cordialement invités.

ABSTRACT:

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.

Back to the VASY Home Page