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
Reﬁnement checking parameterised quorum systems
1M3S research unit, Faculty of Information Technology and Electrical Engineering, University of Oulu
|Online Access:||PDF Full Text (PDF, 0.4 MB)|
|Persistent link:|| http://urn.fi/urn:nbn:fi-fe2019071223093
|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.
|Pages:||39 - 48|
17th International Conference on Application of Concurrency to System Design, ACSD 2017 : proceedings
|Host publication editor:||
17th International Conference on Application of Concurrency to System Design (ACSD 2017)
|Type of Publication:||
A4 Article in conference proceedings
|Field of Science:||
113 Computer and information sciences
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).
© 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.