Step-Wise Development of Provably Correct Actor Systems

摘要

Concurrent and distributed software is widespread, but is inherently complex. The Actor model avoids the common pitfall of shared mutable state and interprocess communication is done via asynchronous message passing. Actors are used in Erlang, the Akka framework, and many others. In this paper we discuss the formal development of actor systems via refinement. We start with an abstract specification and introduce details until the final model can be translated into an actor program. In each refinement, we show that the abstract properties are still preserved. Agha's classical factorial algorithm serves as a demonstrating example. To the best of our knowledge we are the first who formally prove that his actor system computes factorials. We use Event-B as a modelling language together with interactive theorem proving and SMT solving for verification.