Dynamic cut-off algorithm for parameterised refinement checking

Tutkimustuotos: Artikkeli kirjassa/konferenssijulkaisussavertaisarvioitu

Standard

Dynamic cut-off algorithm for parameterised refinement checking. / Siirtola, Antti; Heljanko, Keijo.

Formal Aspects of Component Software - 15th International Conference, FACS 2018, Proceedings. Springer Verlag, 2018. s. 256-276 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vuosikerta 11222 LNCS).

Tutkimustuotos: Artikkeli kirjassa/konferenssijulkaisussavertaisarvioitu

Harvard

Siirtola, A & Heljanko, K 2018, Dynamic cut-off algorithm for parameterised refinement checking. julkaisussa Formal Aspects of Component Software - 15th International Conference, FACS 2018, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vuosikerta. 11222 LNCS, Springer Verlag, Sivut 256-276, Pohang, Etelä-Korea, 10/10/2018. https://doi.org/10.1007/978-3-030-02146-7_13

APA

Siirtola, A., & Heljanko, K. (2018). Dynamic cut-off algorithm for parameterised refinement checking. teoksessa Formal Aspects of Component Software - 15th International Conference, FACS 2018, Proceedings (Sivut 256-276). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vuosikerta 11222 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-030-02146-7_13

Vancouver

Siirtola A, Heljanko K. Dynamic cut-off algorithm for parameterised refinement checking. julkaisussa Formal Aspects of Component Software - 15th International Conference, FACS 2018, Proceedings. Springer Verlag. 2018. s. 256-276. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-030-02146-7_13

Author

Siirtola, Antti ; Heljanko, Keijo. / Dynamic cut-off algorithm for parameterised refinement checking. Formal Aspects of Component Software - 15th International Conference, FACS 2018, Proceedings. Springer Verlag, 2018. Sivut 256-276 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

Bibtex - Lataa

@inproceedings{68ea097071a546d4abf1b10924a92b92,
title = "Dynamic cut-off algorithm for parameterised refinement checking",
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.",
keywords = "Compositional verification, Cut-off, First-order logic, Labelled transition systems, Parameterized systems, Refinement checking, Safety properties, Satisfiability modulo theories",
author = "Antti Siirtola and Keijo Heljanko",
year = "2018",
month = "1",
day = "1",
doi = "10.1007/978-3-030-02146-7_13",
language = "English",
isbn = "9783030021450",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "256--276",
booktitle = "Formal Aspects of Component Software - 15th International Conference, FACS 2018, Proceedings",
address = "Germany",

}

RIS - Lataa

TY - GEN

T1 - Dynamic cut-off algorithm for parameterised refinement checking

AU - Siirtola, Antti

AU - Heljanko, Keijo

PY - 2018/1/1

Y1 - 2018/1/1

N2 - 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.

AB - 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.

KW - Compositional verification

KW - Cut-off

KW - First-order logic

KW - Labelled transition systems

KW - Parameterized systems

KW - Refinement checking

KW - Safety properties

KW - Satisfiability modulo theories

UR - http://www.scopus.com/inward/record.url?scp=85055093514&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-02146-7_13

DO - 10.1007/978-3-030-02146-7_13

M3 - Conference contribution

SN - 9783030021450

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 256

EP - 276

BT - Formal Aspects of Component Software - 15th International Conference, FACS 2018, Proceedings

PB - Springer Verlag

ER -

ID: 29118431