Specifying and model checking distributed control algorithms at meta-level
Abstract: This paper proposes an approach to the specification and model checking of a large, important class of distributed algorithms called control algorithms (CAs), which are superimposed on underlying distributed systems (UDSs). The approach is based on rewriting logic by moving from its object level to the meta-level. We introduce the idea of specifying CAs as meta-programs that take the specifications of UDSs and automatically generate the specifications of the UDSs on which the CAs are superimposed (UDS-CAs). Due to many options, such as network topologies, even fixing the number of each kind of entities, such as mobile support stations (MSSs) and mobile hosts (MHs) in a mobile checkpointing algorithm, there are many instances of a UDS. To address the problem, we generate all possible initial states of a UDS for a fixed number of each kind of entities such that some constraints, such as MSSs strongly connected with a wired network, are fulfilled and conduct model checking for each of the initial states. We demonstrate the usefulness by reporting on a case study where a counterexample is found for some specific initial states but not for the other initial states, detecting a subtle flaw lurking in a mobile checkpointing algorithm
- Location
-
Deutsche Nationalbibliothek Frankfurt am Main
- Extent
-
Online-Ressource
- Language
-
Englisch
- Notes
-
The computer journal. - 65, 12 (2022) , 2998-3019, ISSN: 1460-2067
- Event
-
Veröffentlichung
- (where)
-
Freiburg
- (who)
-
Universität
- (when)
-
2024
- Creator
-
Doan, Thi Thu Ha
Ogata, Kazuhiro
- DOI
-
10.1093/comjnl/bxab122
- URN
-
urn:nbn:de:bsz:25-freidok-2482250
- Rights
-
Open Access; Der Zugriff auf das Objekt ist unbeschränkt möglich.
- Last update
-
14.08.2025, 10:47 AM CEST
Data provider
Deutsche Nationalbibliothek. If you have any questions about the object, please contact the data provider.
Associated
- Doan, Thi Thu Ha
- Ogata, Kazuhiro
- Universität
Time of origin
- 2024
Other Objects (12)
Efficient distributed bounded property checking
Complexity results for checking distributed implementability
A checking approach for distributed building data
Integrating Distributed Algorithms into Distributed Systems
Concepts, algorithms, and tools for model checking
Directed and Distributed Model Checking of B-Specifications
(4) Distributed Algorithms I
Approximating distributed graph algorithms
Optimal distributed covering algorithms
Communication-Efficient Probabilistic Algorithms: Selection, Sampling, and Checking
Specifying Speed Spacing
Improved distributed fractional coloring algorithms
Efficient distributed bounded property checking
Complexity results for checking distributed implementability
A checking approach for distributed building data
Integrating Distributed Algorithms into Distributed Systems
Concepts, algorithms, and tools for model checking
Directed and Distributed Model Checking of B-Specifications
(4) Distributed Algorithms I
Approximating distributed graph algorithms
Optimal distributed covering algorithms
Communication-Efficient Probabilistic Algorithms: Selection, Sampling, and Checking
Specifying Speed Spacing
Improved distributed fractional coloring algorithms
Efficient distributed bounded property checking
Complexity results for checking distributed implementability
A checking approach for distributed building data
Integrating Distributed Algorithms into Distributed Systems
Concepts, algorithms, and tools for model checking
Directed and Distributed Model Checking of B-Specifications
(4) Distributed Algorithms I
Approximating distributed graph algorithms
Optimal distributed covering algorithms
Communication-Efficient Probabilistic Algorithms: Selection, Sampling, and Checking
Specifying Speed Spacing