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

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

Publikation: Beitrag in Buch/Bericht/Konferenzband › Beitrag in einem Konferenzband › Begutachtung

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.

Originalsprache	englisch
Titel	Leveraging Applications of Formal Methods, Verification and Validation
Untertitel	Verification Principles - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Proceedings
Redakteure/-innen	Tiziana Margaria, Bernhard Steffen
Herausgeber (Verlag)	Springer Nature Switzerland AG
Seiten	426-448
Seitenumfang	23
ISBN (Print)	9783030613617
DOIs	https://doi.org/10.1007/978-3-030-61362-4_25
Publikationsstatus	Veröffentlicht - Okt. 2020

Publikationsreihe

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

ASJC Scopus subject areas

Theoretische Informatik
Informatik (insg.)

Zugriff auf Dokument

10.1007/978-3-030-61362-4_25Lizenz: Nicht definiert

Step-wise Development of Provably Correct Actor SystemsAkzeptiertes Autorenmanuskript, 368 KB

Andere Dateien und Links

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

Verlaesslichkeit im Internet der Dinge
Boano, C. A., Kubin, G., Bloem, R., Horn, M., Pernkopf, F., Zakany, N., Mangard, S., Witrisal, K., Römer, K. U., Aichernig, B., Bösch, W., Baunach, M. C., Tappler, M., Malenko, M., Weiser, S., Eichlseder, M., Leitinger, E., Grosinger, J., Großwindhager, B., Ebrahimi, M., Alothman Alterkawi, A. B., Knoll, C., Teschl, R., Saukh, O., Rath, M., Steinberger, M., Steinbauer-Wagner, G. & Tranninger, M.
1/01/16 → 31/03/22
Projekt: Forschungsprojekt

Step-wise Development of Provably Correct Actor Systems
Bernhard Aichernig (Redner/in)
25 Okt. 2021
Aktivität: Vortrag oder Präsentation › Vortrag bei Konferenz oder Fachtagung › Science to science

Dieses zitieren

Aichernig, B., & Maderbacher, B. (2020). Step-Wise Development of Provably Correct Actor Systems. in T. Margaria, & B. Steffen (Hrsg.), Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles - 9th International Symposium on Leveraging Applications of Formal Methods, ISoLA 2020, Proceedings (S. 426-448). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 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. Hrsg. / Tiziana Margaria; Bernhard Steffen. Springer Nature Switzerland AG, 2020. S. 426-448 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Band 12476 LNCS).

Publikation: Beitrag in Buch/Bericht/Konferenzband › Beitrag in einem Konferenzband › Begutachtung

Aichernig, B & Maderbacher, B 2020, Step-Wise Development of Provably Correct Actor Systems. in T Margaria & B Steffen (Hrsg.), 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), Bd. 12476 LNCS, Springer Nature Switzerland AG, S. 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, Hrsg., 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. S. 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. Hrsg. / Tiziana Margaria ; Bernhard Steffen. Springer Nature Switzerland AG, 2020. S. 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

Publikationsreihe

ASJC Scopus subject areas

Zugriff auf Dokument

Andere Dateien und Links

Fingerprint

Projekte

Verlaesslichkeit im Internet der Dinge

Aktivitäten

Step-wise Development of Provably Correct Actor Systems

Dieses zitieren