An optimal cut-off algorithm for parameterised refinement checking
|Author:||Siirtola, Antti1; Heljanko, Keijo2,3|
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
|Online Access:||PDF Full Text (PDF, 11.1 MB)|
|Persistent link:|| http://urn.fi/urn:nbn:fi-fe2020081359426
|Publish Date:|| 2022-07-13
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.
Science of computer programming
|Type of Publication:||
A1 Journal article – refereed
|Field of Science:||
113 Computer and information sciences
The research is partly funded by Academy of Finland projects 313469 and 277522.
|Academy of Finland Grant Number:||
313469 (Academy of Finland Funding decision)
277522 (Academy of Finland Funding decision)
© 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/