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.
Supported by the Vienna Science and Technology Fund (WWTF) through project APALACHE (ICT15-103) and the Austrian Science Fund (FWF) through Doctoral College LogiCS (W1255-N23).
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
A collection of \({\rm TLA}^{+}\) specifications. https://github.com/tlaplus/Examples/. Accessed 21 Oct 2017
Azmy, N., Merz, S., Weidenbach, C.: A rigorous correctness proof for pastry. In: Butler, M., Schewe, K.-D., Mashkoor, A., Biro, M. (eds.) ABZ 2016. LNCS, vol. 9675, pp. 86–101. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-33600-8_5
Beyer, D., Keremoglu, M.E.: CPAchecker: a tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 184–190. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_16
Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-49059-0_14
Biere, A., Heule, M., van Maaren, H.: Handbook of Satisfiability, vol. 185. IOS press, Amsterdam (2009)
Bracha, G., Toueg, S.: Asynchronous consensus and broadcast protocols. J. ACM 32(4), 824–840 (1985)
Chandra, T.D., Toueg, S.: Unreliable failure detectors for reliable distributed systems. J. ACM 43(2), 225–267 (1996)
Chaudhuri, K., Doligez, D., Lamport, L., Merz, S.: The TLA\(^{+}\) proof system: building a heterogeneous verification platform. In: Cavalcanti, A., Deharbe, D., Gaudel, M.-C., Woodcock, J. (eds.) ICTAC 2010. LNCS, vol. 6255, p. 44. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14808-8_3
Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752–794 (2003)
Conchon, S., Goel, A., Krstić, S., Mebsout, A., Zaïdi, F.: Cubicle: a parallel SMT-based model checker for parameterized systems. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 718–724. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31424-7_55
Dijkstra, E.W., Feijen, W.H., Van Gasteren, A.M.: Derivation of a termination detection algorithm for distributed computations. In: Broy, M. (ed.) Control Flow and Data Flow: concepts of distributed programming, pp. 507–512. Springer, Heidelberg (1986). https://doi.org/10.1007/978-3-642-82921-5_13
Gafni, E., Lamport, L.: Disk paxos. Distrib. Comput. 16(1), 1–20 (2003)
Guerraoui, R.: On the hardness of failure-sensitive agreement problems. Inf. Process. Lett. 79(2), 99–104 (2001)
Konnov, I., Lazić, M., Veith, H., Widder, J.: A short counterexample property for safety and liveness verification of fault-tolerant distributed algorithms. In: POPL, pp. 719–734 (2017)
Kroening, D., Tautschnig, M.: CBMC – C bounded model checker. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 389–391. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54862-8_26
Kukovec, J., Tran, T.H., Konnov, I.: Extracting symbolic transitions from \({\rm TLA}^{+}\) specifications (technical report 2018). http://forsyte.at/wp-content/uploads/abz2018_full.pdf. Accessed 7 Feb 2018
Lamport, L.: The part-time parliament. ACM TCS 16(2), 133–169 (1998)
Lamport, L.: Specifying systems: the \({\rm TLA}^{+}\) language and tools for hardware and software engineers. Addison-Wesley Longman Publishing Co., Inc., Boston (2002)
Merz, S.: The specification language \({\rm TLA}^{+}\). In: Bjørner, D., Henson, M.C. (eds.) Logics of specification languages. Monographs in Theoretical Computer Science (An EATCS Series), pp. 401–451. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-74107-7_8
Merz, S., Vanzetto, H.: Automatic verification of \({\rm TLA}^{+}\) proof obligations with SMT solvers. In: Bjørner, N., Voronkov, A. (eds.) LPAR 2012. LNCS, vol. 7180, pp. 289–303. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-28717-6_23
Merz, S., Vanzetto, H.: Harnessing SMT solvers for \({\rm TLA}^{+}\) proofs. ECEASST, 53 (2012). https://hal.inria.fr/hal-00760579
Moraru, I., Andersen, D.G., Kaminsky, M.: There is more consensus in Egalitarian parliaments. In: SOSP, pp. 358–372. ACM (2013)
Newcombe, C., Rath, T., Zhang, F., Munteanu, B., Brooker, M., Deardeuff, M.: How Amazon web services uses formal methods. Commun. ACM 58(4), 66–73 (2015)
Ongaro, D.: Consensus: bridging theory and practice. Ph.D. thesis, Stanford University (2014)
Raynal, M.: A case study of agreement problems in distributed systems: non-blocking atomic commitment. In: HASE, pp. 209–214 (1997)
Yu, Y., Manolios, P., Lamport, L.: Model checking TLA+ specifications. In: Pierre, L., Kropf, T. (eds.) CHARME 1999. LNCS, vol. 1703, pp. 54–66. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48153-2_6
Acknowledgments
We are grateful to Stephan Merz for insightful discussions on semantics of \(\textsc {TLA}^{+}\). We thank anonymous reviewers for their helpful suggestions.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG, part of Springer Nature
About this paper
Cite this paper
Kukovec, J., Tran, TH., Konnov, I. (2018). Extracting Symbolic Transitions from TLA\(^{+}\) Specifications. In: Butler, M., Raschke, A., Hoang, T., Reichl, K. (eds) Abstract State Machines, Alloy, B, TLA, VDM, and Z. ABZ 2018. Lecture Notes in Computer Science(), vol 10817. Springer, Cham. https://doi.org/10.1007/978-3-319-91271-4_7
Download citation
DOI: https://doi.org/10.1007/978-3-319-91271-4_7
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-91270-7
Online ISBN: 978-3-319-91271-4
eBook Packages: Computer ScienceComputer Science (R0)