Skip to main content
SpringerLink
Log in

The Specification Language TLA+

  • Chapter
  • First Online:
Logics of Specification Languages

Abstract

The specification language TLA+ was designed by Lamport for formally describing and reasoning about distributed algorithms. It is described in Lamport’s book Specifying Systems [29], which also gives good advice on how to make the best use of TLA+ and its supporting tools. Systems are specified in TLA+ as formulas of the Temporal Logic of Actions, TLA, a variant of linear-time temporal logic also introduced by Lamport [27]. The underlying data structures are specified in (a variant of) Zermelo-Fränkel set theory, the language accepted by most mathematicians as the standard basis for formalizing mathematics. This choice is motivated by a desire for conciseness, clarity, and formality that befits a language of formal specification where executability or efficiency are not of major concern. TLA+ specifications are organized in modules that can be reused independently.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 129.00
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 169.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 169.99
Price excludes VAT (USA)
  • Durable hardcover edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. M. Abadi. An axiomatization of Lamport’s Temporal Logic of Actions. In J.C.M. Baeten and J.W. Klop, editors, CONCUR’ 90, Theories of Concurrency: Unification and Extension, volume 458 of Lecture Notes in Computer Science, pages 57–69. Springer, 1990.

    Google Scholar 

  2. M. Abadi and L. Lamport. The existence of refinement mappings. Theoretical Computer Science, 81(2):253–284, May 1991.

    Article  MathSciNet  Google Scholar 

  3. M. Abadi and L. Lamport. An old-fashioned recipe for real time. ACM Trans-actions on Programming Languages and Systems, 16(5):1543–1571, Sept. 1994.

    Article  Google Scholar 

  4. M. Abadi and L. Lamport. Conjoining specifications. ACM Transactions on Programming Languages and Systems, 17(3):507–534, May 1995.

    Article  Google Scholar 

  5. M. Abadi and S. Merz. An abstract account of composition. In J. Wiedermann and P. Hajek, editors, Mathematical Foundations of Computer Science, volume 969 of Lecture Notes in Computer Science, pages 499–508. Springer, 1995.

    Google Scholar 

  6. M. Abadi and S. Merz. On TLA as a logic. In M. Broy, editor, Deductive Program Design, NATO ASI Series F, pages 235–272. Springer, 1996.

    Google Scholar 

  7. M. Abadi and G. Plotkin. A logical view of composition. Theoretical Computer Science, 114(1):3–30, June 1993.

    Article  MathSciNet  Google Scholar 

  8. J.-R. Abrial. The B-Book: Assigning Programs to Meanings. Cambridge University Press, 1996.

    Google Scholar 

  9. J.-R. Abrial. Extending B without changing it (for developing distributed systems). In H. Habrias, editor, 1st Conference on the B Method, pages 169–190. IRIN Institut de recherche en informatique de Nantes, 1996.

    Google Scholar 

  10. B. Alpern and F.B. Schneider. Defining liveness. Information Processing Letters, 21(4):181–185, Oct. 1985.

    Article  MathSciNet  Google Scholar 

  11. R. Back and J. von Wright. Refinement calculus—A systematic introduction. Springer, 1998.

    Google Scholar 

  12. E. Börger and R. Stärk. Abstract State Machines: A Method for High-Level System Design and Analysis. Springer, 2003.

    Google Scholar 

  13. D. Cansell, D. Méry and S. Merz. Diagram refinements for the design of reactive systems. Journal of Universal Computer Science, 7(2):159–174, 2001.

    MATH  Google Scholar 

  14. E.M. Clarke, O. Grumberg and D. Peled. Model Checking. MIT Press, Cambridge, Mass., 1999.

    Google Scholar 

  15. W.-P. de Roever, H. Langmaack, and A. Pnueli, editors. Compositionality: The Significant Difference, volume 1536 of Lecture Notes in Computer Science. Springer, 1998.

    Google Scholar 

  16. U. Engberg, P. Gronning and L. Lamport. Mechanical verification of concurrent systems with TLA. In Fourth International Conference on Computer-Aided Verification (CAV’ 92), volume 663 of Lecture Notes in Computer Science, pages 44–55. Springer, 1992.

    Google Scholar 

  17. L. Fejoz, D. Méry and S. Merz. Dixit: Visualizing predicate abstractions. In R. Bharadwaj and S. Mukhopadhyay, editors, Automatic Verification of Infinite-State Systems (AVIS 2005), Edinburgh, UK, Apr. 2005, pages 39–48. To appear in ENTCS.

    Google Scholar 

  18. D. Gries and F. B. Schneider. Avoiding the undefined by underspecification. In J. van Leeuwen, editor, Computer Science Today: Recent Trends and Developments, volume 1000 of Lecture Notes in Computer Science, pages 366–373. Springer., 1995.

    Google Scholar 

  19. G. E. Hughes and M. J. Cresswell. A New Introduction to Modal Logic. Routledge, 1996.

    Google Scholar 

  20. S. Kalvala. A formulation of TLA in Isabelle. Available at ftp://ftp.dcs.warwick.ac.uk/people/Sara.Kalvala/tla.dvi, Mar. 1995.

    Google Scholar 

  21. M. Kaminski. Invariance under stuttering in a temporal logic of actions. Theoretical Computer Science, 2006. To appear.

    Google Scholar 

  22. H. W. Kamp. Tense Logic and the Theory of Linear Order. PhD thesis, University of California at Los Angeles, 1968.

    Google Scholar 

  23. L. Lamport. The TLA home page. http://www.research.microsoft.com/users/lamport/tla/tla.html.

    Google Scholar 

  24. L. Lamport. Proving the correctness of multiprocess programs. IEEE Transactions on Software Engineering, SE-3(2):125–143, Mar. 1977.

    Article  MathSciNet  Google Scholar 

  25. L. Lamport. What good is temporal logic? In R. E. A. Mason, editor, Information Processing 83: Proceedings of the IFIP 9th World Congress, Paris, Sept. 1983, pages 657–668, 1983. North-Holland, 1983.

    Google Scholar 

  26. L. Lamport. How to write a long formula. Formal Aspects of Computing, 6(5):580–584, 1994.

    Article  Google Scholar 

  27. L. Lamport. The Temporal Logic of Actions. ACM Transactions on Program-ming Languages and Systems, 16(3):872–923, May 1994.

    Article  Google Scholar 

  28. L. Lamport. How to write a proof. American Mathematical Monthly, 102(7):600–608, 1995.

    Article  MathSciNet  Google Scholar 

  29. L. Lamport. Specifying Systems. Addison-Wesley., 2002.

    Google Scholar 

  30. L. Lamport. Real-time model checking is really simple. In D. Borrione and W. J. Paul, editors, Correct Hardware Design and Verification Methods (CHARME 2005), volume 3725 of Lecture Notes in Computer Science, pages 162–175. Springer, 2005.

    Google Scholar 

  31. L. Lamport. Checking a multithreaded algorithm with =+cal. In S. Dolev, editor, 20th International Symposium on Distributed Computing (DISC 2006), Stockholm, 2006. To appear.

    Google Scholar 

  32. A. C. Leisenring. Mathematical Logic and Hilbert’s ɛ-Symbol, University Mathematical Series. Macdonald, 1969.

    Google Scholar 

  33. Z. Manna and A. Pnueli. Verification of concurrent programs: The temporal framework. In R. Boyer and J. Moore, editors, The Correctness Problem in Computer Science, pages 215–273. Academic Press, London, 1982.

    Google Scholar 

  34. Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems: Specification. Springer, New York, 1992.

    Book  Google Scholar 

  35. S. Merz. Isabelle/TLA. Available at http://isabelle.in.tum.de/library/HOL/TLA, 1997. Revised 1999.

    Google Scholar 

  36. S. Merz. A more complete TLA. In J. Wing, J. Woodcock, and J. Davies, editors, FM’99: World Congress on Formal Methods, volume 1709 of Lecture Notes in Computer Science, pages 1226–1244. Springer, 1999.

    Google Scholar 

  37. A. Pnueli. The temporal logic of programs. In Proceedings of the 18th Annual Symposium on the Foundations of Computer Science, pages 46–57. IEEE, 1977.

    Google Scholar 

  38. A. N. Prior. Past, Present and Future. Clarendon Press, 1967.

    Google Scholar 

  39. A. P. Sistla, E. M. Clarke, N. Francez, and Y. Gurevich. Can message buffers be characterized in linear temporal logic? Information and Control, 63:88–112, 1984.

    Article  MathSciNet  Google Scholar 

  40. M. Spivey. The Z Notation: A Reference Manual. Prentice Hall, 1992.

    Google Scholar 

  41. P. Suppes. Axiomatic Set Theory. Dover, 1972.

    Google Scholar 

  42. M. Vardi. Branching vs. linear time: Final showdown. In T. Margaria and W. Yi, editors, Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2001), volume 2031 of Lecture Notes in Computer Science, pages 1–22. Springer, 2001. See http://www.cs.rice.edu/~vardi/papers/ for more recent versions of this paper.

    Google Scholar 

  43. Y. Yu, P. Manolios, and L. Lamport. Model checking TLA+ specifications. In L. Pierre and T. Kropf, editors, Correct Hardware Design and Verification Methods (CHARME’799), volume 1703 of Lecture Notes in Computer Science, pages 54–66. Springer, 1999.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. INRIA Lorraine, LORIA, 615 rue du Jardin Botanique, F-54602, Villers-lès-Nancy, France

    Stephan Merz

Authors
  1. Stephan Merz
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Informatics and Mathematical Modelling, Technical University of Denmark, 2800, Kgs. Lyngby, Denmark

    Dines Bjørner

  2. Department of Computer Science, University of Essex, Wivenhoe Park, CO4 3SQ, Colchester, UK

    Martin C. Henson

Rights and permissions

Reprints and permissions

Copyright information

© 2008 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Merz, S. (2008). The Specification Language TLA+ . In: Bjørner, D., Henson, M.C. (eds) Logics of Specification Languages. Monographs in Theoretical Computer Science. An EATCS Series. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-74107-7_8

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-74107-7_8

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-74106-0

  • Online ISBN: 978-3-540-74107-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation