Refinement checking parameterised quorum systems

Siirtola, Antti (2018-06-25)
 
Avaa tiedosto
Lataukset: 

URL:
https://doi.org/10.1109/ACSD.2017.15

Siirtola, Antti
Institute of Electrical and Electronics Engineers
25.06.2018

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

https://rightsstatements.org/vocab/InC/1.0/
© 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/
doi:https://doi.org/10.1109/ACSD.2017.15
Näytä kaikki kuvailutiedot
Julkaisun pysyvä osoite on
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