Erlang on TOAST: Generating Erlang Stubs with Inline TOAST Monitors
Implementing concurrent systems based on asynchronous communications is intrinsically complex. In this work, we consider the formal framework TOAST for timed asynchronous interactions featuring mixed-choice states. TOAST extends the theory of timed asynchronous session types to support modelling of communication protocols featuring timeouts, that despite being commonplace in practice were previously out of reach for session type theory. We present ongoing work towards a practical toolchain that (a) automates the generation of correct-by-construction program stubs with timeouts in Erlang from TOAST protocols, and (b) provides an inline monitoring framework for TOAST protocols integrated with Erlang supervisors. Our toolchain generates Erlang code with a close correspondence to the source protocol by building on a formal correspondence between session types and Communicating Finite State Machines. The monitoring framework can be configured to perform either runtime verification or enforcement of process behaviour against the source protocol, ensuring communication safety.
Mon 2 SepDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
16:00 - 17:30 | |||
16:00 30mTalk | Elixir-powered Low-income Animal Shelter Support: an Experience Report from Conception to Production Erlang | ||
16:30 30mTalk | The Benefits of Tierless Elixir/Potato for Engineering IoT Systems Erlang Solaris Li University of Glasgow, Phil Trinder University of Glasgow, Christophe De Troyer Vrije Universiteit Brussel, Mart Lubbers Radboud University Nijmegen, Adrian Ramsingh Sia Fusion Ltd | ||
17:00 30mTalk | Erlang on TOAST: Generating Erlang Stubs with Inline TOAST Monitors Erlang |