Automata for Specifying and Orchestrating Service Contracts
Davide Basile, Pierpaolo Degano, Gian-Luigi Ferrari (Universit\`a di, Pisa, Italy)

TL;DR
This paper introduces automata-based methods for formally specifying and orchestrating multi-party service contracts, ensuring request satisfaction and goal achievement, with techniques for static analysis and violation detection.
Contribution
It presents a novel automata framework for service contracts, including static orchestration and violation detection, integrating Linear Programming for asynchronous scenarios.
Findings
Automata effectively specify service contracts and guarantee request satisfaction.
The approach can detect contract violations and identify responsible principals.
Linear Programming techniques enable analysis in asynchronous settings.
Abstract
An approach to the formal description of service contracts is presented in terms of automata. We focus on the basic property of guaranteeing that in the multi-party composition of principals each of them gets his requests satisfied, so that the overall composition reaches its goal. Depending on whether requests are satisfied synchronously or asynchronously, we construct an orchestrator that at static time either yields composed services enjoying the required properties or detects the principals responsible for possible violations. To do that in the asynchronous case we resort to Linear Programming techniques. We also relate our automata with two logically based methods for specifying contracts.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
