APALACHE

Abstraction-based parameterized TLA+ checker: Bringing state-of-the-art model checking to TLA+


Downloads: unstable@github master@github (rarely updated!) Build status

Critical distributed systems are designed to tolerate faults of individual components: they must work even if some of their components fail. In APALACHE, we address three technical and methodological challenges:

  • Symbolic model checking techniques for TLA+.
  • Domain-specific abstractions for fault-tolerant TLA+ designs.
  • Parameterized model checking techniques for an unbounded number of components.

Some of the challenges were mentioned in the position paper (2015).

 

Bounded model checking modulo theories (BMCMT). As a first step towards more advanced techniques for TLA+, we are currently developing a symbolic model checker that is working under the following assumptions:

  1. As in TLC, all specification parameters are fixed and finite, e.g., the system is initialized integers, finite sets, and functions of finite domains and co-domains.
  2. As in TLC, all data structures evaluated during an execution are finite, e.g., a system specification cannot operate on the set of all integers.
  3. Only finite executions up to a given bound are analysed.

The current version of the tool will most likely crash on your own TLA+ code. When the tool is ready for early testing by the users, we will issue an announcement.

Given a TLA+ specification, with all parameters fixed, our model checker performs the following steps:

  1. BMCMT automatically extracts symbolic transitions from the specification (see our paper at ABZ’18). This allows us to partition the action Next into a conjunction of simpler actions A1, …, An.
  2. BMCMT translates the operators Init and A1, …, An to SMT formulas. This allows us to explore bounded executions with an SMT solver, for instance, with Microsoft Z3 or CVC4. For instance, a sequence of k steps, all of which execute action A1, will be encoded as Run(k) == [[Init(s0)]] ∧ [[A1(s0, s1)]] ∧ … ∧ [[A1(sk-1, sk)]]. To find an execution of length k leading to an unsafe state sk, one can add [[Bug(sk)]] to the formula Run(k). Here, [[_]] is the translation function from TLA+ to SMT. Importantly, the values for the states s0, …, sk are not enumerated as in TLC, but have to be found by the SMT solver.

This technique follows the approach of bounded model checking (BMC) that was pioneered by [Armin Biere, Alessandro Cimatti, Edmund Clarke, and Yunshan Zhu’99]. Bounded model checking was quite a success for bug finding and verification of C code, e.g., see the tool CBMC by Daniel Kroening et al. Whereas classical BMC uses of-the-shelf SAT solvers (Boolean logic), our tool encodes bounded model checking queries in SMT, which supports first-order theories of integers, uninterpreted functions, arrays, etc. The main challenge of our work lies in defining the translation function [[_]] to SMT. We are preparing a technical report on this topic.

We will give more details in the upcoming talk at the TLA+ community event.

Team

HOR_1499
ThanhHaiTran_Photo © Sara Meister jure

Related projects

Parameterized model checking of fault-tolerant distributed algorithms. To see the papers, benchmarks, and tools, check our Byzantine Model Checker .

Recent papers

2018
[13] Extracting Symbolic Transitions from TLA+ Specifications
Jure Kukovec, Thanh-Hai Tran, Igor Konnov
Abstract State Machines, Alloy, B, TLA, VDM, and Z, pages 89-104, 2018.
[bibtex] [pdf] [doi]
[12]Reachability in Parameterized Systems: All Flavors of Threshold Automata
Jure Kukovec, Igor Konnov, Josef Widder
CONCUR 2018, 2018.
Note: (to appear)
[bibtex]
[11] BmcMT: Bounded Model Checking of TLA+ Specifications with SMT
Igor Konnov, Jure Kukovec, Thanh-Hai Tran
2018, Presentation at the TLA+ Community Meeting, Oxford, UK, July.
[bibtex] [pdf]
2017
[10] Synthesis of Distributed Algorithms with Parameterized Threshold Guards
Marijana Lazic, Igor Konnov, Josef Widder, Roderick Bloem
OPODIS, volume 95 of LIPIcs, pages 32:1-32:20, 2017.
[bibtex] [pdf]
[9] Accuracy of Message Counting Abstraction in Fault-Tolerant Distributed Algorithms
Igor V. Konnov, Josef Widder, Francesco Spegni, Luca Spalazzi
Verification, Model Checking, and Abstract Interpretation - 18th International Conference, VMCAI 2017, Paris, France, January 15-17, 2017, Proceedings, pages 347-366, 2017.
[bibtex] [pdf] [doi]
[8] On the completeness of bounded model checking for threshold-based distributed algorithms: Reachability
Igor V. Konnov, Helmut Veith, Josef Widder
Inf. Comput., volume 252, pages 95-109, 2017.
[bibtex] [pdf] [doi]
[7] A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms
Igor V. Konnov, Marijana Lazic, Helmut Veith, Josef Widder
Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017, pages 719-734, 2017.
Note: A pre-print including the proofs is available at http://arxiv.org/abs/1608.05327
[bibtex] [pdf]
[6]Para^2: Parameterized Path Reduction, Acceleration, and SMT for Reachability in Threshold-Guarded Distributed Algorithms
Igor Konnov, Marijana Lazic, Helmut Veith, Josef Widder
Formal Methods in System Design, 2017, Springer.
Note: to appear
[bibtex]
2016
[5] Decidability of Parameterized Verification
Roderick Bloem, Swen Jacobs, Ayrat Khalimov, Igor Konnov, Sasha Rubin, Helmut Veith, Josef Widder
ACM SIGACT News, volume 47, number 2, pages 53-64, jun 2016.
[bibtex] [pdf]
[4] Parameterized Systems in BIP: Design and Model Checking
Igor Konnov, Tomer Kotek, Qiang Wang, Helmut Veith, Simon Bliudze, Joseph Sifakis
27th International Conference on Concurrency Theory (CONCUR 2016) (Josée Desharnais, Radha Jagadeesan, eds.), volume 59 of Leibniz International Proceedings in Informatics (LIPIcs), pages 30:1-30:16, 2016, Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik.
[bibtex] [pdf]
[3] What You Always Wanted to Know About Model Checking of Fault-Tolerant Distributed Algorithms
Igor Konnov, Helmut Veith, Josef Widder
Perspectives of System Informatics: 10th International Andrei Ershov Informatics Conference, PSI 2015, in Memory of Helmut Veith, Kazan and Innopolis, Russia, August 24-27, 2015, Revised Selected Papers (Manuel Mazzara, Andrei Voronkov, eds.), volume 9609 of LNCS, pages 6-21, 2016, Springer International Publishing.
[bibtex] [pdf]
[2] A Short Counterexample Property for Safety and Liveness Verification of Fault-Tolerant Distributed Algorithms
Igor Konnov, Marijana Lazic, Helmut Veith, Josef Widder
arXiv/CoRR, volume 1608.05327, 2016.
Note: (accepted to POPL 2017)
[bibtex] [pdf]
2015
[1] Challenges in Model Checking of Fault-tolerant Designs in TLA+
Igor Konnov, Helmut Veith, Josef Widder
2015, Presentation at the 8th International Workshop on Exploiting Concurrency Efficiently and Correctly, San Francisco, CA, USA, July.
[bibtex] [pdf]

Contact

Address:
Igor Konnov
Technische Universität Wien
Institut für Logic and Computation 192/4
Favoritenstraße 9–11
1040 Wien
Austria

Room: HD 03 13 (how to get there)
Phone: +43 (1) 58801 – 184 807
Email: ta.etysrofnull@vonnok
Web: http://forsyte.at/~konnov/

Latest News

TU Vienna Honorary Doctorate to Ed Clarke

We are glad to announce that TU Vienna will award an honorary doctorate to Ed Clarke. Edmund M. Clarke is among the leading computer scientists of our times. As a professor at Harvard, and, since 1982, at Carnegie Mellon University, he and his group have not only laid the theoretical and logical foundations of model […]

Continue reading

Opening of Vienna Center for Logic and Algorithms (VCLA) on Jan 25

The Vienna Center for Logic and Algorithms is an initiative of the Faculty of Informatics and funded by a three-year competitive grant of Vienna University of Technology. Embedded into the primary research area Computational Intelligence and the funding priority Computational Logic of the Faculty, the center is promoting international scientific collaboration in logic and algorithms. […]

Continue reading

Full news archive