Step-Wise Development of Provably Correct Actor Systems

Bernhard Aichernig; Benedikt Maderbacher

doi:10.1007/978-3-030-61362-4_25

Step-Wise Development of Provably Correct Actor Systems

Bernhard Aichernig^*, Benedikt Maderbacher

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference paper › peer-review

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 language	English
Title of host publication	Leveraging Applications of Formal Methods, Verification and Validation
Subtitle of host publication	Verification Principles - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Proceedings
Editors	Tiziana Margaria, Bernhard Steffen
Publisher	Springer Nature Switzerland AG
Pages	426-448
Number of pages	23
ISBN (Print)	9783030613617
DOIs	https://doi.org/10.1007/978-3-030-61362-4_25
Publication status	Published - Oct 2020

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	12476 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
General Computer Science

Access to Document

10.1007/978-3-030-61362-4_25Licence: Unspecified

Step-wise Development of Provably Correct Actor SystemsAccepted author manuscript, 368 KB

Cite this

Aichernig, B., & Maderbacher, B. (2020). Step-Wise Development of Provably Correct Actor Systems. In T. Margaria, & B. Steffen (Eds.), Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Proceedings (pp. 426-448). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12476 LNCS). Springer Nature Switzerland AG. https://doi.org/10.1007/978-3-030-61362-4_25

Step-Wise Development of Provably Correct Actor Systems. / Aichernig, Bernhard ; Maderbacher, Benedikt.
Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Proceedings. ed. / Tiziana Margaria; Bernhard Steffen. Springer Nature Switzerland AG, 2020. p. 426-448 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 12476 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference paper › peer-review

Aichernig, B & Maderbacher, B 2020, Step-Wise Development of Provably Correct Actor Systems. in T Margaria & B Steffen (eds), Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 12476 LNCS, Springer Nature Switzerland AG, pp. 426-448. https://doi.org/10.1007/978-3-030-61362-4_25

Aichernig B , Maderbacher B. Step-Wise Development of Provably Correct Actor Systems. In Margaria T, Steffen B, editors, Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Proceedings. Springer Nature Switzerland AG. 2020. p. 426-448. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-030-61362-4_25

Aichernig, Bernhard ; Maderbacher, Benedikt. / Step-Wise Development of Provably Correct Actor Systems. Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Proceedings. editor / Tiziana Margaria ; Bernhard Steffen. Springer Nature Switzerland AG, 2020. pp. 426-448 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{6fd99cc33ad540f1a8723348354f6369,

title = "Step-Wise Development of Provably Correct Actor Systems",

abstract = "Concurrent and distributed software is widespread, but isinherently complex. The Actor model avoids the common pitfall of sharedmutable state and interprocess communication is done via asynchronousmessage passing. Actors are used in Erlang, the Akka framework, andmany others. In this paper we discuss the formal development of actorsystems 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 stillpreserved. Agha{\textquoteright}s classical factorial algorithm serves as a demonstratingexample. To the best of our knowledge we are the first who formallyprove that his actor system computes factorials. We use Event-B as amodelling language together with interactive theorem proving and SMTsolving for verification.",

keywords = "Actors, Event-B, Formal method, Proof-based development, Refinement, Verification",

author = "Bernhard Aichernig and Benedikt Maderbacher",

year = "2020",

month = oct,

doi = "10.1007/978-3-030-61362-4_25",

language = "English",

isbn = "9783030613617",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Nature Switzerland AG",

pages = "426--448",

editor = "Tiziana Margaria and Bernhard Steffen",

booktitle = "Leveraging Applications of Formal Methods, Verification and Validation",

address = "Switzerland",

}

TY - GEN

T1 - Step-Wise Development of Provably Correct Actor Systems

AU - Aichernig, Bernhard

AU - Maderbacher, Benedikt

PY - 2020/10

Y1 - 2020/10

N2 - Concurrent and distributed software is widespread, but isinherently complex. The Actor model avoids the common pitfall of sharedmutable state and interprocess communication is done via asynchronousmessage passing. Actors are used in Erlang, the Akka framework, andmany others. In this paper we discuss the formal development of actorsystems 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 stillpreserved. Agha’s classical factorial algorithm serves as a demonstratingexample. To the best of our knowledge we are the first who formallyprove that his actor system computes factorials. We use Event-B as amodelling language together with interactive theorem proving and SMTsolving for verification.

AB - Concurrent and distributed software is widespread, but isinherently complex. The Actor model avoids the common pitfall of sharedmutable state and interprocess communication is done via asynchronousmessage passing. Actors are used in Erlang, the Akka framework, andmany others. In this paper we discuss the formal development of actorsystems 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 stillpreserved. Agha’s classical factorial algorithm serves as a demonstratingexample. To the best of our knowledge we are the first who formallyprove that his actor system computes factorials. We use Event-B as amodelling language together with interactive theorem proving and SMTsolving for verification.

KW - Actors

KW - Event-B

KW - Formal method

KW - Proof-based development

KW - Refinement

KW - Verification

UR - http://www.scopus.com/inward/record.url?scp=85097411062&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-61362-4_25

DO - 10.1007/978-3-030-61362-4_25

M3 - Conference paper

SN - 9783030613617

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 426

EP - 448

BT - Leveraging Applications of Formal Methods, Verification and Validation

A2 - Margaria, Tiziana

A2 - Steffen, Bernhard

PB - Springer Nature Switzerland AG

ER -

Step-Wise Development of Provably Correct Actor Systems

Abstract

Publication series

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Dependable Internet of Things