January 20, 2014

Cinzia Di Giusto (équipe COSMO, IBISC, Université d'Evry)

I will introduce the concept of adaptable processes as a way of overcoming the limitations that process calculi have for describing patterns of dynamic process evolution. Such patterns rely on direct ways of controlling the behaviour and location of running processes, and so they are at the heart of the adaptation capabilities present in many modern concurrent systems such as workflows or cloud computing scenarios. Rather than a specification language, our calculus intends to be a basis for investigating the fundamental properties of evolvable processes and for developing richer languages with evolvability capabilities.

I will present a core calculus of adaptable processes and propose a framework for verifying and ensuring properties of the designed systems along two directions. First, I will show two specific verification problems and a way of generalising them. The verification properties ensures that the number of consecutive erroneous states that can be traversed during a computation is bound by some given number k, or that a state without errors will be eventually reached. We study the (un)decidability of these two problems and their generalisation in several variants of the calculus. Finally, I will propose a type system for statically ensuring that well typed processes guarantee safe and secure updates: for instance, we guarantee that no active protocol is interrupted by an update.