AGERE!@SPLASH2015 Talk
Actario: A Framework for Reasoning About Actor Systems
Shohei Yasutake & Takuo Watanabe
5th International Workshop on Programming based on Actors, Agents, and Decentralized Control (AGERE!@SPLASH 2015), Pittsburgh, Oct. 26, 2015.
Abstract
The two main characteristics of the Actor model are asynchronous message passing and dynamic system topology. The latter relies on the on-the-fly creation of actor names that often complicates the formal treatment of systems described in the Actor model. In this paper, we introduce Actario, a formalization of the Actor model in Coq. Actario incorporates a name creation mechanism that is formally proved to generate a consistent set of actor names. The mechanism helps proper handling of names in modeling and reasoning about actor-based systems. Actario also provides a code extraction mechanism that generates Erlang programs.