Towards Dynamic Updates in Service Composition

TL;DR

This paper explores verification techniques for adaptable processes that support dynamic updates, enabling more flexible and evolvable concurrent systems, and extends these ideas to distributed adaptability and choreography modifications.

Contribution

It introduces a core calculus for adaptable processes, analyzes verification problems, and extends the framework to distributed updates and multiparty interactions.

Findings

Decidability results for verification problems

Expressive temporal logic for adaptable processes

Extension of choreography theory with runtime updates

Abstract

We survey our results about verification of adaptable processes. We present 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, and so they are at the heart of the adaptation capabilities present in many modern concurrent systems. Adaptable processes have named scopes and are sensible to actions of dynamic update at runtime; this allows to express dynamic and static topologies of adaptable processes as well as different evolvability patterns for concurrent processes. We introduce a core calculus of adaptable processes and consider verification problems for them: first based on specific properties related to error occurrence, that we call bounded and eventual adaptation, and then by considering a simple yet expressive temporal logic over adaptable processes. We provide (un)decidability results of such verification problems over adaptable processes considering the spectrum of topologies/evolvability patterns introduced. We then consider distributed adaptability, where a process can update part of a protocol by performing dynamic distributed updates over a set of protocol participants. Dynamic updates in this context are presented as an extension of our work on choreographies and behavioural contracts in multiparty interactions. We show how update mechanisms considered for adaptable processes can be used to extend the theory of choreography and orchestration/contracts, allowing them to be modified at run-time by internal (self-adaptation) or external intervention.