Projekte pro Jahr
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.
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 | |
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
- Allgemeine Computerwissenschaft
Fingerprint
Untersuchen Sie die Forschungsthemen von „Step-Wise Development of Provably Correct Actor Systems“. Zusammen bilden sie einen einzigartigen Fingerprint.Projekte
- 1 Abgeschlossen
-
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
Aktivitäten
- 1 Vortrag bei Konferenz oder Fachtagung
-
Step-wise Development of Provably Correct Actor Systems
Bernhard Aichernig (Redner/in)
25 Okt. 2021Aktivität: Vortrag oder Präsentation › Vortrag bei Konferenz oder Fachtagung › Science to science