Orchestration synthesis for real-time service contracts

Service contracts offer a way to define the desired behavioural compliance of a composition of services, characterised by the fulfilment of all requirements (e.g. service requests) by obligations (e.g. service offers). Depending on their granularity, requirements may vary according to their criticality and contain real-time aspects (e.g. service expiration time). Synthesis of safe orchestrations, the standard method to refine spurious compositions into compliant ones, is of paramount importance. Ideally, safe orchestrations solve competition among matching requests/offers, respecting criticalities and time constraints, in the best possible way. The contribution of this paper is (i) the introduction of timed service contract automata, a novel formalisation of service contracts with (ii) real-time constraints and (iii) service requests with varying levels of criticality, and a means to compute their (iv) composition and (v) safe orchestration. Orchestration is based on the synthesis of the most permissive controller from supervisory control theory, computed using the concept of zones from timed games. An intuitive example illustrates the contribution.