Orchestrated Session Compliance
Franco Barbanera (Dipartimento di Matematica e Informatica, University, of Catania), Steffen van Bakel (Department of Computing, Imperial College, London), Ugo de'Liguoro (Dipartimento di Informatica, University of Torino)
TL;DR
This paper introduces a formal framework for orchestrated session compliance in client/server interactions, enabling guaranteed message delivery and bounded buffering through decidable procedures for synthesizing and verifying orchestrators.
Contribution
It defines orchestrated compliance in session contracts and provides algorithms to synthesize and verify orchestrators ensuring message delivery and bounded buffering.
Findings
Decidability of orchestrated compliance relation
Procedures for synthesizing compliant orchestrators
Verification method for orchestrator behavior
Abstract
We investigate the notion of orchestrated compliance for client/server interactions in the context of session contracts. Devising the notion of orchestrator in such a context makes it possible to have orchestrators with unbounded buffering capabilities and at the same time to guarantee any message from the client to be eventually delivered by the orchestrator to the server, while preventing the server from sending messages which are kept indefinitely inside the orchestrator. The compliance relation is shown to be decidable by means of 1) a procedure synthesising the orchestrators, if any, making a client compliant with a server, and 2) a procedure for deciding whether an orchestrator behaves in a proper way as mentioned before.
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.