Dynamic cut-off algorithm for parameterised refinement checking

Antti Siirtola*, Keijo Heljanko

*Tämän työn vastaava kirjoittaja

Tutkimustuotos: Artikkeli kirjassa/konferenssijulkaisussaConference contributionScientificvertaisarvioitu

1 Sitaatiot (Scopus)

Abstrakti

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.

AlkuperäiskieliEnglanti
OtsikkoFormal Aspects of Component Software - 15th International Conference, FACS 2018, Proceedings
Sivut256-276
Sivumäärä21
DOI - pysyväislinkit
TilaJulkaistu - 1 tammikuuta 2018
OKM-julkaisutyyppiA4 Artikkeli konferenssijulkaisuussa
TapahtumaInternational Conference on Formal Aspects of Component Software - Pohang, Etelä-Korea
Kesto: 10 lokakuuta 201812 lokakuuta 2018
Konferenssinumero: 15

Julkaisusarja

NimiLecture Notes in Computer Science
Vuosikerta11222
ISSN (painettu)0302-9743
ISSN (elektroninen)1611-3349

Conference

ConferenceInternational Conference on Formal Aspects of Component Software
LyhennettäFACS
MaaEtelä-Korea
KaupunkiPohang
Ajanjakso10/10/201812/10/2018

Sormenjälki Sukella tutkimusaiheisiin 'Dynamic cut-off algorithm for parameterised refinement checking'. Ne muodostavat yhdessä ainutlaatuisen sormenjäljen.

  • Siteeraa tätä

    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; Vuosikerta 11222). https://doi.org/10.1007/978-3-030-02146-7_13