Synthesis of Orchestrations and Choreographies: Bridging the Gap between Supervisory Control and Coordination of Services

TL;DR

This paper develops a unified framework for synthesizing orchestrations and choreographies of service contracts by adapting supervisory control theory, introducing a new controllability concept, and providing a generalized, abstract synthesis algorithm.

Contribution

It introduces a novel controllability notion and an abstract parametric synthesis algorithm that unify supervisory control and service coordination synthesis methods.

Findings

The modified synthesis algorithm produces the most permissive controllers for service orchestrations.

The abstract synthesis generalizes classical and service-specific synthesis approaches.

Concrete syntheses are shown to be in a refinement order, ensuring correctness.

Abstract

We present a number of contributions to bridging the gap between supervisory control theory and coordination of services in order to explore the frontiers between coordination and control systems. Firstly, we modify the classical synthesis algorithm from supervisory control theory for obtaining the so-called most permissive controller in order to synthesise orchestrations and choreographies of service contracts formalised as contract automata. The key ingredient to make this possible is a novel notion of controllability. Then, we present an abstract parametric synthesis algorithm and show that it generalises the classical synthesis as well as the orchestration and choreography syntheses. Finally, through the novel abstract synthesis, we show that the concrete syntheses are in a refinement order. A running example from the service domain illustrates our contributions.