Interface Automata for Choreographies
Hao Zeng, Alexander Kurz, Emilio Tuosto

TL;DR
This paper introduces group interface automata as a new local model for choreographies, providing a method to verify well-formed global views in message-passing applications using pomset semantics.
Contribution
It presents a novel local model and verification method for global choreographies, enhancing the analysis of message-passing systems.
Findings
Introduces group interface automata for local choreography modeling
Proposes a new verification method for well-formed global views
Utilizes pomset semantics for formal analysis
Abstract
Choreographic approaches to message-passing applications can be regarded as an instance of the model-driven development principles. Choreographies specify interactions among distributed participants coordinating among themselves with message-passing at two levels of abstractions. A global view of the application is specified with a model that abstracts away from asynchrony while a local view of the application specifies the communication pattern of each participant. Noteworthy, the latter view can typically be algorithmically obtained by projection of the global view. A crucial element of this approach is to verify the so-called well-formed conditions on global views so that its projections realise a sound communication protocol. We introduce a novel local model, group interface automata, to represent the local view of choreographies and propose a new method to verify the…
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.
