Compositional protocol (..) communicating actors
summary
Claims an algorithmic notion of protocol composition that enforces three properties: behavior preservation, fairness (strong or weak vs strong fairness), and well assertiveness via three assertion kinds assert/require/consume. A prototype tool extracts protocols from Erlang gen_statem code, composes annotated session-type protocols, synthesizes duals, and generates Erlang OTP gen_statem stubs; strong-fairness composition can yield no interleavings while weak-fairness returns many. Demo shows extraction, composition, and stub generation working and plans include automatic assertion inference and code migration.
AI-written summary · about
chapters (11)
- 0:0001:15 - Contents - Laura Bocchi
- 1:1602:48 - Modeling Behaviour
- 4:2607:01 - A bad protocol ( in the harsh asynchronous world)
- 7:0209:21 - Good Protocols
- 9:2212:29 - Session Types
- 12:3014:11 - Context
- 14:1219:52 - Problem 1: Composition
- 19:5221"47 - Problem 2: Make it easy to (re-)engineer
- 21:4823:00 - In Summary
- 23:0131:30 - Demo Overview - Laura Voinea
- 31:4138:39 - QnA
related talks
39mProtocol engineering for communicating actors
18mHybrid Multiparty Session Types: Compositionality for Protocol Specification th...
31mCooperative Specification via Composition Control
22mCompositional Programming and Testing of Dynamic Distributed Systems
20mUnifying compositional verification and certified compilation with a three-dimensional(…)
32mMulticompatibility for Multiparty-Session Composition
31mCompositional Verification of Stigmergic Collective Systems
15mStatically Verified Refinements for Multiparty Protocols