Multiparty message-passing protocols are notoriously difficult to design, due to interaction mismatches that lead to errors such as deadlocks. Existing protocol specification formats have been developed to prevent such errors (e.g. multiparty session types (MPST)). In order to further constrain protocols, specifications can be extended with refinements, i.e. logical predicates to control the behaviour of the protocol based on previous values exchanged. Unfortunately, existing refinement theories and implementations are tightly coupled with specification formats. This artifact accompanies [Martin Vassor and Nobuko Yoshida, 2024]. It presents an implementation of the framework presented in this paper.
@Article{vassor_et_al:DARTS.10.2.23, author = {Vassor, Martin and Yoshida, Nobuko}, title = {{Refinements for Multiparty Message-Passing Protocols: Specification-Agnostic Theory and Implementation (Artifact)}}, pages = {23:1--23:5}, journal = {Dagstuhl Artifacts Series}, ISBN = {978-3-95977-342-3}, ISSN = {2509-8195}, year = {2024}, volume = {10}, number = {2}, editor = {Vassor, Martin and Yoshida, Nobuko}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/DARTS.10.2.23}, URN = {urn:nbn:de:0030-drops-209212}, doi = {10.4230/DARTS.10.2.23}, annote = {Keywords: Message-Passing Concurrency, Session Types, Specification} }
8ef53937b5b645043e52feebff85092a
(Get MD5 Sum)
The artifact has been evaluated as described in the ECOOP 2024 Call for Artifacts and the ACM Artifact Review and Badging Policy.
Feedback for Dagstuhl Publishing