University of Oulu

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

Refinement checking parameterised quorum systems

Saved in:
Author: Siirtola, Antti1
Organizations: 1M3S research unit, Faculty of Information Technology and Electrical Engineering, University of Oulu
Format: article
Version: accepted version
Access: open
Online Access: PDF Full Text (PDF, 0.4 MB)
Persistent link:
Language: English
Published: Institute of Electrical and Electronics Engineers, 2017
Publish Date: 2019-07-12


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.

see all

ISBN: 978-1-5386-2867-6
ISBN Print: 978-1-5386-2868-3
Pages: 39 - 48
DOI: 10.1109/ACSD.2017.15
Host publication: 17th International Conference on Application of Concurrency to System Design, ACSD 2017 : proceedings
Host publication editor: Legay, Axel
Schneider, Klaus
Conference: International Conference on Application of Concurrency to System Design (ACSD)
Type of Publication: A4 Article in conference proceedings
Field of Science: 113 Computer and information sciences
Funding: The author would like to thankfully acknowledge funding from the ITEA 3 APPSTACLE research program funded by Tekes (Finnish Funding Agency for Technology and Innovation).
Copyright information: © 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.