Protocol engineering for communicating actors
summary
Protocol models get extracted from Erlang gen_statem code into session types, composed algorithmically with three annotations assert/require/consume, and turned back into gen_statem stubs that keep annotations as comments. Composition enforces three properties preservation, fairness, well-assertiveness with both strong and weak interleaving modes, and duals are derived automatically for client code. The tool is implemented, handles asynchronous mailboxes, and aims to migrate handwritten local logic into newly composed protocols; code is available on GitHub.
AI-written summary · about
chapters (15)
- 0:00Start
- 0:20Protocol Engineering for Communicating Actors
- 1:21Example of Behavioral Model of Protocol
- 4:56Example of a Bad Protocol
- 5:54Asynchronous Communication via Mailboxes
- 9:21Session Types
- 12:32Banking Protocol
- 14:41Assertions
- 16:06Behavior Preservation
- 17:40Fairness
- 19:28Weak Fairness
- 21:48Summary
- 23:01Demo
- 24:45Overview of the Tool
- 25:12Extract the Protocol from the Erlang
related talks
39mCompositional protocol (..) communicating actors
18mHybrid Multiparty Session Types: Compositionality for Protocol Specification th...
45mTaming Distribution: Formal Protocols for Akka Typed
47mInteraction Protocols: It's all about good manners
20mMessage-Observing Sessions
15mStatically Verified Refinements for Multiparty Protocols
15mCAMP: Cost-Aware Multiparty Session Protocols
40mTypes and Erlang from Dialyzer to (...)