TLA
TLA stands for the Temporal Logic of Actions, but it has become a shorthand for referring to the TLA+ specification language and the PlusCal algorithm language, together with their associated tools. TLA+ is based on the idea that the best way to describe things formally is with simple mathematics, and that a specification language should contain as little as possible beyond what is needed to write simple mathematics precisely. TLA+ is especially well suited for writing high-level specifications of concurrent and distributed systems. PlusCal is an algorithm language that, at first glance, looks like a typical tiny toy programming language. However, a PlusCal expression can be any TLA+ expression, which means anything that can be expressed with mathematics. This makes PlusCal much more expressive than any (real or toy) programming language. A PlusCal algorithm is translated into a TLA+ specification, to which the TLA+ tools can be applied. The principal TLA+ tools are the TLC model checker and TLAPS, the TLA+ proof system. All the tools are normally used from the Toolbox, an IDE (integrated development environment). Go to the TLA home page to find out more about TLA.
Keywords for this software
References in zbMATH (referenced in 23 articles )
Showing results 1 to 20 of 23.
Sorted by year (- Konnov, Igor; Veith, Helmut; Widder, Josef: What you always wanted to know about model checking of fault-tolerant distributed algorithms (2016)
- von Rhein, Alexander; Thüm, Thomas; Schaefer, Ina; Liebig, Jörg; Apel, Sven: Variability encoding: from compile-time to load-time variability (2016)
- Lamport, Leslie: How to write a 21$^\textst$ century proof (2012)
- Li, Guodong; Palmer, Robert; DeLisi, Michael; Gopalakrishnan, Ganesh; Kirby, Robert M.: Formal specification of MPI 2.0: case study in specifying a practical concurrent programming API (2011)
- Liu, Xiaojun; Lee, Edward A.: CPO semantics of timed interactive actor networks (2008)
- Meseguer, José: The temporal logic of rewriting: A gentle introduction (2008)
- Banach, R.; Poppleton, M.; Jeske, C.; Stepney, S.: Engineering and theoretical underpinnings of retrenchment (2007)
- Helin, Joni: Combining deep and shallow embeddings. (2006)
- Armando, A.; Basin, D.; Boichut, Y.; Chevalier, Y.; Compagna, L.; Cuellar, J.; Hankes Drielsma, P.; Heám, P.C.; Kouchnarenko, O.; Mantovani, J.; Mödersheim, S.; von Oheimb, D.; Rusinowitch, M.; Santiago, J.; Turuani, M.; Viganò, L.; Vigneron, L.: The AVISPA tool for the automated validation of internet security protocols and applications (2005)
- Schellhorn, Gerhard: ASM refinement and generalizations of forward simulation in data refinement: a comparison (2005)
- Kroening, Daniel; Ouaknine, Joël; Seshia, Sanjit A.; Strichman, Ofer: Abstraction-based satisfiability solving of Presburger arithmetic (2004)
- Florescu, Daniela; Grünhagen, Andreas; Kossmann, Donald: XL: An XML programming language for web service specification and composition. (2003)
- Merz, Stephan; Wirsing, Martin; Zappe, Júlia: A spatio-temporal logic for the specification and refinement of mobile systems (2003)
- Padberg, J.; Urbášek, M.: Rule-based refinement of Petri nets: A survey (2003)
- Misra, Jayadev: A discipline of multiprogramming. Programming theory for distributed applications (2001)
- Pazos Arias, José J.; García Duque, Jorge: SCTL-MUS: A formal methodology for software development of distributed systems. A case study (2001)
- Vardi, Moshe Y.: Branching vs. linear time: Final showdown (2001)
- Anlauff, Matthias: Xasm -- an extensible, component-based abstract state machines language (2000)
- Butler, Michael: csp2B: A practical approach to combining CSP and B (2000)
- Alur, Rajeev; Henzinger, Thomas A.: Real-time system = discrete system + clock variables (1997)
Further publications can be found at: http://research.microsoft.com/en-us/um/people/lamport/tla/papers.html