Erla+: Translating TLA+ Models into Executable Actor-Based Implementations
This program is tentative and subject to change.
Distributed systems are notoriously difficult to design and implement correctly. Although formal methods provide rigorous approaches to verifying the adherence of a program to its specification, there still exists a gap between a formal model and implementation if the model and its implementation are only loosely coupled. Developers usually overcome this gap through manual effort, which may result in the introduction of unexpected bugs.
In this paper, we present Erla+, a translator that automatically translates models written in a subset of the PlusCal language to TLA+ for formal reasoning and produces executable Erlang programs in one run. Erla+ additionally provides new PlusCal primitives for actor-style modeling, thus clearly separating the modeled system from its environment.
We show the expressivity and strengths of Erla+ by applying it to representative use cases such as a Raft-based key-value store. Our evaluation shows that the implementations generated by Erla+ offer competitive performance against manually written and optimized state-of-the-art libraries.
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 |