University of Oulu

Siirtola, A., & Heljanko, K. (2020). An optimal cut-off algorithm for parameterised refinement checking. Science of Computer Programming, 198, 102517. https://doi.org/10.1016/j.scico.2020.102517

An optimal cut-off algorithm for parameterised refinement checking

Saved in:
Author: Siirtola, Antti1; Heljanko, Keijo2,3
Organizations: 1University of Oulu, Faculty of Information Technology and Electrical Engineering, Finland
2University of Helsinki, Department of Computer Science, Finland
3Helsinki Institute for Information Technology (HIIT), Finland
Format: article
Version: accepted version
Access: embargoed
Persistent link: http://urn.fi/urn:nbn:fi-fe2020081359426
Language: English
Published: Elsevier, 2020
Publish Date: 2022-07-13
Description:

Abstract

The verification of contemporary distributed software systems is challenging, because they are heavily parameterised, containing components whose number and connections cannot be a priori fixed. In this work, we consider the multi-parameterised verification of safety properties by refinement checking in the context of labelled transition systems (LTSs). The LTSs are parameterised by using first-order constructs, sorts, variables, and predicates, while preserving compositionality. This allows us to parameterise not only the number of replicated components but also the communication topology of the system. Our approach to solving a verification task in the parameterised LTS formalism is to determine a finite cut-off set of parameter values such that in order to prove a parameterised system implementation correct with respect to its specification, it is sufficient to consider only finitely many instances of the parameterised system generated by the parameter values in the cut-off set.

In the conference version of this work, we converted the problem of determining a finite cut-off set into the unsatisfiability of a first-order formula and provided a satisfiability modulo theories (SMT)-based semi-algorithm for dynamically, i.e., iteratively, computing a cut-off set. In this article, we present a new version of the algorithm and prove that the cut-off sets computed by this new algorithm are optimal. Hence, we call the new version the optimal cut-off algorithm. The algorithm will always terminate for system topologies expressible in the ∃∗∀∗ fragment of first-order logic. It also enables us to consider systems with topologies beyond this fragment, but for these systems, the algorithm is not guaranteed to terminate. We have implemented the approach on top of the Z3 SMT solver and successfully applied it to several system models. As a running example, we consider the leader election phase of the generalised (Byzantine) Raft consensus algorithm and prove the optimal cut-off set of six (respectively, thirteen) parameter values corresponding to instances up to three (respectively, four) servers. To the best of our knowledge, this is the first time a Byzantine variant of the parameterised Raft leader election is automatically verified.

see all

Series: Science of computer programming
ISSN: 0167-6423
ISSN-E: 1872-7964
ISSN-L: 0167-6423
Volume: 198
Article number: 102517
DOI: 10.1016/j.scico.2020.102517
OADOI: https://oadoi.org/10.1016/j.scico.2020.102517
Type of Publication: A1 Journal article – refereed
Field of Science: 113 Computer and information sciences
Subjects:
Funding: The research is partly funded by Academy of Finland projects 313469 and 277522.
Academy of Finland Grant Number: 313469
277522
Detailed Information: 313469 (Academy of Finland Funding decision)
277522 (Academy of Finland Funding decision)
Copyright information: © 2020. This manuscript version is made available under the CC-BY-NC-ND 4.0 license http:/creativecommons.org/licenses/by-nc-nd/4.0/
  https://creativecommons.org/licenses/by-nc-nd/4.0/