Step-Wise Development of Provably Correct Actor Systems

Bernhard Aichernig*, Benedikt Maderbacher

*Korrespondierende/r Autor/-in für diese Arbeit

Publikation: Beitrag in Buch/Bericht/KonferenzbandBeitrag in einem KonferenzbandBegutachtung


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 intro-
duce details until the final model can be translated into an actor pro-
gram. 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.
TitelLeveraging Applications of Formal Methods, Verification and Validation
UntertitelVerification Principles - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Proceedings
Redakteure/-innenTiziana Margaria, Bernhard Steffen
Herausgeber (Verlag)Springer Nature Switzerland AG
ISBN (Print)9783030613617
PublikationsstatusVeröffentlicht - Okt. 2020


NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Band12476 LNCS
ISSN (Print)0302-9743
ISSN (elektronisch)1611-3349

ASJC Scopus subject areas

  • Theoretische Informatik
  • Informatik (insg.)


Untersuchen Sie die Forschungsthemen von „Step-Wise Development of Provably Correct Actor Systems“. Zusammen bilden sie einen einzigartigen Fingerprint.

Dieses zitieren