Erlang on TOAST: Generating Erlang Stubs with Inline TOAST Monitors

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, which 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 processes that implement a TOAST protocol, 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 TOAST model 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 with respect to the source protocol, ensuring communication safety.