Extracting Symbolic Transitions from TLA+ Specifications

Abstract

In (\textsc {TLA}^{+}), a system specification is written as a logical formula that restricts the system behavior. As a logic, (\textsc {TLA}^{+}) does not have assignments and other imperative statements that are used by model checkers to compute the successor states of a system state. Model checkers compute successors either explicitly — by evaluating program statements — or symbolically — by translating program statements to an SMT formula and checking its satisfiability. To efficiently enumerate the successors, TLA’s model checker TLC introduces side effects. For instance, an equality (x' = e) is interpreted as an assignment of e to the yet unbound variable x. Inspired by TLC, we introduce an automatic technique for discovering expressions in (\textsc {TLA}^{+}) formulas such as (x' = e) and (x' \in {e_1, \dots , e_k}) that can be provably used as assignments. In contrast to TLC, our technique does not explicitly evaluate expressions, but it reduces the problem of finding assignments to the satisfiability of an SMT formula. Hence, we give a way to slice a (\textsc {TLA}^{+}) formula in symbolic transitions, which can be used as an input to a symbolic model checker. Our prototype implementation successfully extracts symbolic transitions from a few (\textsc {TLA}^{+}) benchmarks.

Document

If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.

Reference

% BibTex
@inproceedings{KukovecTK18,
  author       = {Jure Kukovec and
                  Thanh{-}Hai Tran and
                  Igor Konnov},
  editor       = {Michael J. Butler and
                  Alexander Raschke and
                  Thai Son Hoang and
                  Klaus Reichl},
  title        = {Extracting Symbolic Transitions from TLA\({}^{\mbox{+}}\) Specifications},
  booktitle    = {Abstract State Machines, Alloy, B, TLA, VDM, and {Z} - 6th International
                  Conference, {ABZ} 2018, Southampton, UK, June 5-8, 2018, Proceedings},
  series       = {Lecture Notes in Computer Science},
  volume       = {10817},
  pages        = {89--104},
  publisher    = {Springer},
  year         = {2018},
  url          = {https://doi.org/10.1007/978-3-319-91271-4\_7},
  doi          = {10.1007/978-3-319-91271-4\_7},
  timestamp    = {Thu, 18 Nov 2021 13:33:08 +0100},
  biburl       = {https://dblp.org/rec/conf/asm/KukovecTK18.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}