Compositional protocol engineering for communicating actors | Laura Bocchi & Laura Voinea

In systems of communicating processes or actors, data types can be used to discipline the sorts of sent and received messages. Session types, in addition, can describe specific causalities and patterns among different send/receive actions (like application-level protocols). I will give an overview on recent and ongoing research about writing “good protocols” using session types and session types to yield correct implementations.    

I will then focus on modular composition of protocols.  Real-world communication protocols are often built out of simpler protocols that cater for some specific functionality (e.g., banking, authentication) or operate at different levels of abstraction (e.g., HTTP, POP). However much of the work used for program verification (e.g., session types) treat protocols as monolithic units.  

I will show an approach to protocol composition, including a tool that extracts models from concurrent Erlang code into a protocol language based on session types, implements an algorithmic notion of protocol composition, and provides code generation from protocols. The purpose is greater modularisation and code reuse.