Basile D., Ter Beek M. H., Legay A., Traonouez L. M.
Orchestration Real-Time Services Synthesis Formal Methods Automata 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.
Source: 12th International Conference on Verification and Evaluation of Computer and Communication Systems (VECoS'18), pp. 31–47, Grenoble, France, 26-28/9/2018
Publisher: Springer, Berlin, DEU
@inproceedings{oai:it.cnr:prodotti:391614, title = {Orchestration synthesis for real-time service contracts}, author = {Basile D. and Ter Beek M. H. and Legay A. and Traonouez L. M.}, publisher = {Springer, Berlin, DEU}, doi = {10.1007/978-3-030-00359-3_3}, booktitle = {12th International Conference on Verification and Evaluation of Computer and Communication Systems (VECoS'18), pp. 31–47, Grenoble, France, 26-28/9/2018}, year = {2018} }