Step-Wise Development of Provably Correct Actor Systems

Bernhard Aichernig*, Benedikt Maderbacher

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference paper

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 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.
Original languageEnglish
Title of host publicationLeveraging Applications of Formal Methods, Verification and Validation
Subtitle of host publicationVerification Principles - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Proceedings
EditorsTiziana Margaria, Bernhard Steffen
PublisherSpringer Nature Switzerland AG
Pages426-448
Number of pages23
ISBN (Print)9783030613617
DOIs
Publication statusPublished - Oct 2020

Publication series

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

Keywords

  • Actors
  • Event-B
  • Formal method
  • Proof-based development
  • Refinement
  • Verification

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint

Dive into the research topics of 'Step-Wise Development of Provably Correct Actor Systems'. Together they form a unique fingerprint.

Cite this