Refinement checking parameterised quorum systems
Siirtola, Antti (2018-06-25)
A. Siirtola, "Refinement Checking Parameterised Quorum Systems," 17th International Conference on Application of Concurrency to System Design (ACSD 2017), Zaragoza, Spain, 2017, pp. 39-48. doi:10.1109/ACSD.2017.15
© 2017 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works.
https://rightsstatements.org/vocab/InC/1.0/
https://urn.fi/URN:NBN:fi-fe2019071223093
Tiivistelmä
Abstract
Many fault-tolerant algorithms are based on decisions made by a quorum of nodes. Since the algorithms are utilised in safety critical applications such as distributed databases, it is necessary to make sure that they operate reliably under every possible scenario. We introduce a generic compositional formalism, based on parameterised labelled transition systems, which allows us to express safety properties of parameterised quorum systems. We prove that any parameterised verification task expressible in the formalism collapses into finitely many finite state refinement checking problems. The technique is implemented in a tool, which performs the verification completely automatically. As an example, we prove the leader election phase of the Raft consensus algorithm correct for an arbitrary number of terms and for a cluster of any size.
Kokoelmat
- Avoin saatavuus [31939]
Samankaltainen aineisto
Näytetään aineisto, joilla on samankaltaisia nimekkeitä, tekijöitä tai asiasanoja.
-
Network orchestration and system dynamics modelling in developing innovative decision support systems for policy makers
Pikkarainen, Minna; Gomes, Julius Francis; Ranta, Jukka; Ylén, Peter; Iivari, Marika; Hurmelinna-Laukkanen, Piia
Open innovation. Bridging theory and practice : 5 (World Scientific, 30.06.2020) -
Drivers of the innovation system and role of knowledge application in regional innovation system — case Oulu region, Finland
Longi, Henna; Niemelä, Sami
Arctic and North -
Thermodynamic description of ternary Fe–B–X systems. Part 8 : Fe–B–Mo, with extension to quaternary Fe–B–Cr–Mo system
Miettinen, Jyrki; Visuri, Ville-Valtteri; Fabritius, Timo
Archives of metallurgy and materials : 1 (Polish Academy of Sciences, 22.12.2020)