University of Oulu

Siirtola A., Heljanko K. (2018) Dynamic Cut-Off Algorithm for Parameterised Refinement Checking. In: Bae K., Ölveczky P. (eds) Formal Aspects of Component Software. FACS 2018. Lecture Notes in Computer Science, vol 11222. Springer, Cham

Dynamic cut-off algorithm for parameterised refinement checking

Saved in:
Author: Siirtola, Antti1; Heljanko, Keijo2,3,4
Organizations: 1Faculty of Information Technology and Electrical Engineering, M3S Research Group, University of Oulu
2Department of Computer Science, Aalto University
3Department of Computer Science, University of Helsinki
4Helsinki Institute for Information Technology (HIIT)
Format: article
Version: accepted version
Access: embargoed
Persistent link: http://urn.fi/urn:nbn:fi-fe2018102238576
Language: English
Published: Springer Nature, 2018
Publish Date: 2019-10-05
Description:

Abstract

The verification of contemporary software systems is challenging, because they are heavily parameterised containing components, the number and connections of which cannot be a priori fixed. 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 system topology, the connections between the components. We aim to solve a verification task in the parameterised LTS formalism by determining cut-offs for the parameters. As the main contribution, we convert this problem into the unsatisfiability of a first-order formula and provide a SAT modulo theories (SMT)-based semi-algorithm for dynamically, i.e., iteratively, computing the cut-offs. The algorithm will always terminate for 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 Raft consensus algorithm and prove a cut-off of three servers which we conjecture to be the optimal one.

see all

Series: Lecture notes in computer science
ISSN: 0302-9743
ISSN-E: 1611-3349
ISSN-L: 0302-9743
ISBN: 978-3-030-02146-7
ISBN Print: 978-3-030-02145-0
Issue: 11222
Pages: 256 - 276
DOI: 10.1007/978-3-030-02146-7_13
OADOI: https://oadoi.org/10.1007/978-3-030-02146-7_13
Host publication: Formal aspects of component software : 15th International Conference, FACS 2018, Pohang, South Korea, October 10–12, 2018, proceedings
Host publication editor: Bae, Kyungmin
Ölveczky, Peter Csaba
Conference: 15th International Conference on Formal Aspects of Component Software (FACS 2018)
Type of Publication: A4 Article in conference proceedings
Field of Science: 113 Computer and information sciences
Subjects:
Copyright information: © Springer Nature Switzerland AG 2018. This is a post-peer-review, pre-copyedit version of an article published in Lecture Notes in Computer Science. The final authenticated version is available online at: http://dx.doi.org/10.1007/978-3-030-02146-7_13