Erlang on TOAST: Generating Erlang Stubs with Inline TOAST Monitors
This program is tentative and subject to change.
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.
This program is tentative and subject to change.
Mon 2 SepDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
14:00 - 15:30 | |||
14:00 30mTalk | Erla+: Translating TLA+ Models into Executable Actor-Based Implementations Erlang Marian Hristov University of Kaiserslautern-Landau, Annette Bieniusa University of Kaiserslautern-Landau | ||
14:30 30mTalk | Erlang on TOAST: Generating Erlang Stubs with Inline TOAST Monitors Erlang | ||
15:00 30mTalk | Is this really a refactoring? Automated equivalence checking for Erlang projects Erlang Bendegúz Seres Eötvös Loránd University, Dániel Horpácsi Eötvös Loránd University, Simon Thompson IOHK, University of Kent, and ELTE |