| Autor: |
Aleksey Polyakov, Elisey Nigodin, Elena Polupanova, Pavel Usov |
| Jazyk: |
ruština |
| Rok vydání: |
2022 |
| Předmět: |
|
| Zdroj: |
Современные информационные технологии и IT-образование, Vol 18, Iss 1, Pp 54-61 (2022) |
| Druh dokumentu: |
article |
| ISSN: |
2411-1473 |
| DOI: |
10.25559/SITITO.18.202201.54-61 |
| Popis: |
This article is devoted to verification of the bully election algorithm for distributed systems with TLA+ and PlusCal. In this work, we show an overview of the basic information about distributed systems, then we show definition of election algorithms for distributed systems, after that we provide a full description of the bully election algorithm for distributed systems. Later in this article, we show the model of the distributed algorithm created with TLA+ and PlusCal. Then we describe the main parts of this model. Next, we illustrate results of verification of this model. The verification was done using TLC ‒ a model checker and simulator for executable TLA+ specifications. As a result of the verification, it was possible to establish that the declared properties of safety and liveness are fully satisfied for all possible states of the system. |
| Databáze: |
Directory of Open Access Journals |
| Externí odkaz: |
|
