Model-based Testing of Practical Distributed Systems in Actor Model
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , |
|---|---|
| Format: | Preprint |
| Publié: |
2025
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866917135297544192 |
|---|---|
| author | Kokorin, Ilya Chernatskiy, Evgeny Aksenov, Vitaly |
| author_facet | Kokorin, Ilya Chernatskiy, Evgeny Aksenov, Vitaly |
| contents | Designing and implementing distributed systems correctly can be quite challenging. Although these systems are often accompanied by formal specifications that are verified using model-checking techniques, a gap still exists between the implementation and its formal specification: there is no guarantee that the implementation is free of bugs.
To bridge this gap, we can use model-based testing. Specifically, if the model of the system can be interpreted as a finite-state automaton, we can generate an exhaustive test suite for the implementation that covers all possible states and transitions.
In this paper, we discuss how to efficiently generate such a test suite for distributed systems written in the actor model. Importantly, our approach does not require any modifications to the code or interfering with the distributed system execution environment. As an example, we verified an implementation of a replication algorithm based on Viewstamped Replication, which is used in a real-world system. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2512_08698 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Model-based Testing of Practical Distributed Systems in Actor Model Kokorin, Ilya Chernatskiy, Evgeny Aksenov, Vitaly Distributed, Parallel, and Cluster Computing Designing and implementing distributed systems correctly can be quite challenging. Although these systems are often accompanied by formal specifications that are verified using model-checking techniques, a gap still exists between the implementation and its formal specification: there is no guarantee that the implementation is free of bugs. To bridge this gap, we can use model-based testing. Specifically, if the model of the system can be interpreted as a finite-state automaton, we can generate an exhaustive test suite for the implementation that covers all possible states and transitions. In this paper, we discuss how to efficiently generate such a test suite for distributed systems written in the actor model. Importantly, our approach does not require any modifications to the code or interfering with the distributed system execution environment. As an example, we verified an implementation of a replication algorithm based on Viewstamped Replication, which is used in a real-world system. |
| title | Model-based Testing of Practical Distributed Systems in Actor Model |
| topic | Distributed, Parallel, and Cluster Computing |
| url | https://arxiv.org/abs/2512.08698 |