Step-Wise Development of Provably Correct Actor Systems

1Citations
Citations of this article
2Readers
Mendeley users who have this article in their library.
Get full text

Abstract

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.

Cite

CITATION STYLE

APA

Aichernig, B. K., & Maderbacher, B. (2020). Step-Wise Development of Provably Correct Actor Systems. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 12476 LNCS, pp. 426–448). Springer Science and Business Media Deutschland GmbH. https://doi.org/10.1007/978-3-030-61362-4_25

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free