TLA+: Difference between revisions

| paradigm = [[Action language|Action]]

| year = {{Start date and age|1999|04|23}}<ref name="tlaplus-original">

| last = Lamport

| first = Leslie

| accessdate = 8 May 2015}}

</ref> and its use likened to [[Technical drawing|drawing blueprints]] for software systems;<ref name="wired">

| last = Lamport

| first = Leslie

| authorlink = Leslie Lamport

| title = Why We Should Build Software Like We Build Houses

| publisher = [[Wired (magazine)|Wired]]

| date = 25 January 2013

| publisher = [[Addison-Wesley]]

| date = 18 June 2002

</ref>

 

| volume = 11

| pages = 43–63

| date = 2012

| url = http://research.microsoft.com/en-us/um/people/lamport/pubs/proof.pdf

| publisher = [[Springer Netherlands]]

| date = 1995

</ref>

 

 

TLA specifications mostly consisted of ordinary non-temporal mathematics, which Lamport found less cumbersome than a purely temporal specification. TLA provided a mathematical foundation to the specification language TLA⁺, introduced with the paper "Specifying Concurrent Systems with TLA⁺" in 1999.<ref name="tlaplus-original"/> Later that same year, Yuan Yu wrote the TLC [[model checker]] for TLA⁺ specifications; TLC was used to find errors in the [[cache coherence]] protocol for a [[Compaq]] multiprocessor.<ref name="tlcoriginal">

| last1 = Yu

| first1 = Yuan

| title = Model checking TLA⁺ specifications

| journal = Correct Hardware Design and Verification Methods

| pages = 54–66

| publisher = [[Springer-Verlag]]

| doi = 10.1007/3-540-48153-2_6

| url = http://research.microsoft.com/en-us/um/people/lamport/pubs/yuanyu-model-checking.pdf

</ref>

 

| date = 18 June 2002

| url = http://research.microsoft.com/en-us/um/people/lamport/tla/book.html

</ref> [[PlusCal]] was introduced in 2009,<ref name="pluscal-original">

| last = Lamport

| first = Leslie

| url = http://research.microsoft.com/en-us/um/people/lamport/pubs/pluscal.pdf

| doi = 10.1007/978-3-642-03466-4_2

</ref> and the TLA⁺ proof system (TLAPS) in 2012.<ref name="tlaps-survey"/> TLA⁺² was announced in 2014, adding some additional language constructs as well as greatly increasing in-language support for the proof system.<ref name="tla2guide" /> Lamport is engaged in creating an updated TLA⁺ reference, "The TLA⁺ Hyperbook". The incomplete work is [http://research.microsoft.com/en-us/um/people/lamport/tla/hyperbook.html available] from his official website. Lamport is also creating [http://lamport.azurewebsites.net/video/videos.html The TLA+ Video Course], described therein as "a work in progress that consists of the beginning of a series of video lectures to teach programmers and software engineers how to write their own TLA+ specifications".

 

| publisher = [[Addison-Wesley]]

| date = 18 June 2002

</ref>

 

| publisher = [[Addison-Wesley]]

| date = 18 June 2002

</ref>

 

| accessdate = 14 May 2015}}

</ref> TLA⁺ was used to write formal proofs of correctness for [[Paxos (computer science)#Byzantine Paxos|Byzantine Paxos]] and components of the [[Pastry (DHT)|Pastry distributed hash table]].<ref name="tlaps-survey">

| last1 = Cousineau

| first1 = Denis

| doi = 10.1007/978-3-642-32759-9_14

| url = http://research.microsoft.com/en-us/um/people/lamport/pubs/tlaps.pdf

</ref>

 

[[Amazon Web Services]] has used TLA⁺ since 2011. TLA⁺ model checking uncovered bugs in [[DynamoDB]], [[Amazon S3|S3]], [[Amazon Elastic Block Store|EBS]], and an internal distributed lock manager; some bugs required state traces of 35 steps. Model checking was also used to verify aggressive optimizations. In addition, TLA⁺ specifications were found to hold value as documentation and design aids.<ref name="awsorig"/><ref name="awschose">

| last = Chris

| first = Newcombe

| date = 2014

| doi = 10.1007/978-3-662-43652-3_3

</ref>