An optimal cut-off algorithm for parameterised refinement checking

Show full item record



Siirtola , A & Heljanko , K 2020 , ' An optimal cut-off algorithm for parameterised refinement checking ' , Science of Computer Programming , vol. 198 , 102517 .

Title: An optimal cut-off algorithm for parameterised refinement checking
Author: Siirtola, Antti; Heljanko, Keijo
Contributor organization: Department of Computer Science
Helsinki Institute for Information Technology
Date: 2020-10-15
Language: eng
Number of pages: 31
Belongs to series: Science of Computer Programming
ISSN: 0167-6423
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 there exists*for all* 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. (C) 2020 Elsevier B.V. All rights reserved.
Subject: Compositional verification
Parameterized systems
Satisfiability modulo theories
Automated verification
113 Computer and information sciences
Peer reviewed: Yes
Rights: cc_by_nc_nd
Usage restriction: openAccess
Self-archived version: acceptedVersion

Files in this item

Files Size Format View

There are no files associated with this item.

This item appears in the following Collection(s)

Show full item record