Adaptable Processes

Adaptable Processes
Mario Bravetti University of Bologna, Italy
Cinzia Di Giusto INRIA, France
Jorge A. Perez FCT UNL, Portugal
Gianluigi Zavattaro University of Bologna, Italy

We propose 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 behavior and location of running processes. As such, they are at the heart of the adaptation capabilities present in many modern concurrent systems. Adaptable processes have a location and are sensible to actions of dynamic update at runtime. This allows to express a wide range of evolvability patterns for processes. We introduce a core calculus of adaptable processes and propose two verification problems for them: bounded and eventual adaptation. While the former ensures that at most k consecutive errors will arise in future states, the latter ensures that if the system enters in an error state then it will eventually reach a correct state. We study the (un)decidability of these two adaptation properties in different fragments of the calculus. 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.
Download:
Conference Version (in Proc. of FMOODS-FORTE'11, Springer LNCS 6722): [PDF]
Extended and Revised Version, with proofs (79pp) ---DRAFT, 30/10/2011---: [PDF]

Steps on the Road to Component Evolvability
Mario Bravetti University of Bologna, Italy
Cinzia Di Giusto INRIA, France
Jorge A. Perez FCT UNL, Portugal
Gianluigi Zavattaro University of Bologna, Italy

We have recently developed a calculus for dynamically evolvable aggregations of components. The calculus extends CCS with primitives for describing components and their evolvability capabilities. Central to these novel primitives is a restricted form of higher-order communication of processes involved in update operations. The origins of our calculus for components can indeed be traced back to our own previous work on expressiveness and decidability results for core higher-order process calculi. Here we overview these previous works, and discuss the motivations and design decisions that led us from higher-order process calculi to calculi for component evolvability.
Download:
Final version, to appear in the Post-proceedings of FACS'10 (Springer LNCS 6921): [PDF]