Movatterモバイル変換


[0]ホーム

URL:


Jump to content
WikipediaThe Free Encyclopedia
Search

TLA+

From Wikipedia, the free encyclopedia
(Redirected fromTLA+ Toolbox)
Formal specification language
TLA+
ParadigmAction
Designed byLeslie Lamport
First appearedApril 23, 1999; 25 years ago (1999-04-23)[1]
Stable release
TLA+2 / January 15, 2014; 11 years ago (2014-01-15)[2]
Implementation languageJava
OSCross-platform (multi-platform)
LicenseMIT License[3]
Filename extensions.tla
Websitetlapl.us

TLA+ is aformal specification language developed byLeslie Lamport. It is used for designing, modelling, documentation, and verification of programs, especiallyconcurrent systems anddistributed systems. TLA+ is considered to be exhaustively-testablepseudocode,[4] and its use likened todrawing blueprints for software systems;[5]TLA is anacronym forTemporal Logic of Actions.

For design and documentation, TLA+ fulfills the same purpose as informaltechnical specifications. However, TLA+ specifications are written in a formal language oflogic and mathematics, and the precision of specifications written in this language is intended to uncover design flaws before system implementation is underway.[6]

Since TLA+ specifications are written in a formal language, they are amenable to finitemodel checking. The model checker finds all possible system behaviours up to some number of execution steps, and examines them for violations of desiredinvariance properties such assafety andliveness. TLA+ specifications use basicset theory to define safety (bad things won't happen) andtemporal logic to define liveness (good things eventually happen).

TLA+ is also used to writemachine-checked proofs of correctness both foralgorithms and mathematical theorems. The proofs are written in a declarative, hierarchical style independent of any single theorem prover backend. Both formal and informal structured mathematical proofs can be written in TLA+; the language is similar toLaTeX, and tools exist to translate TLA+ specifications to LaTeX documents.[7]

TLA+ was introduced in 1999, following several decades of research into a verification method for concurrent systems. Ever since, a toolchain has been developed, including anIDE and a distributed model checker. The pseudocode-like languagePlusCal was created in 2009; ittranspiles to TLA+ and is useful for specifying sequential algorithms. TLA+2 was announced in 2014, expanding language support for proof constructs. The current TLA+ reference isThe TLA+ Hyperbook by Leslie Lamport.

History

[edit]
Portrait of an Israeli man in his sixties. His hair is short and balding, and he is wearing glasses with a dress shirt and jacket.
Amir Pnueli applied temporal logic to computer science, for which he received the 1996Turing Award.

Moderntemporal logic was developed byArthur Prior in 1957, then called tense logic. AlthoughAmir Pnueli was the first to seriously study the applications of temporal logic tocomputer science, Prior speculated on its use a decade earlier in 1967:

The usefulness of systems of this sort [on discrete time] does not depend on any serious metaphysical assumption that time is discrete; they are applicable in limited fields of discourse in which we are concerned only with what happens next in a sequence of discrete states, e.g. in the working of a digital computer.

Pnueli researched the use of temporal logic in specifying and reasoning about computer programs, introducinglinear temporal logic in 1977. LTL became an important tool for analysis of concurrent programs, easily expressing properties such asmutual exclusion and freedom fromdeadlock.[8]

Concurrent with Pnueli's work on LTL, academics were working to generalizeHoare logic for verification of multiprocess programs.Leslie Lamport became interested in the problem afterpeer review found an error in a paper he submitted on mutual exclusion. Ed Ashcroft introducedinvariance in his 1975 paper "Proving Assertions About Parallel Programs", which Lamport used to generalizeFloyd's method in his 1977 paper "Proving Correctness of Multiprocess Programs". Lamport's paper also introducedsafety andliveness as generalizations ofpartial correctness andtermination, respectively.[9] This method was used to verify the first concurrentgarbage collection algorithm in a 1978 paper withEdsger Dijkstra.[10]

Lamport first encountered Pnueli's LTL during a 1978 seminar atStanford organized bySusan Owicki. According to Lamport, "I was sure that temporal logic was some kind of abstract nonsense that would never have any practical application, but it seemed like fun, so I attended." In 1980 he published "'Sometime' is Sometimes 'Not Never'", which became one of the most frequently-cited papers in the temporal logic literature.[11] Lamport worked on writing temporal logic specifications during his time atSRI, but found the approach to be impractical:

Portrait of a Caucasian man in his seventies with medium-length gray hair and a full gray beard, wearing glasses and a T-shirt.
TLA+ was developed by computer scientist and 2013 Turing award recipientLeslie Lamport.

However, I became disillusioned with temporal logic when I saw how Schwartz, Melliar-Smith, and Fritz Vogt were spending days trying to specify a simpleFIFO queue – arguing over whether the properties they listed were sufficient. I realized that, despite its aesthetic appeal, writing a specification as a conjunction of temporal properties just didn't work in practice.[12]

His search for a practical method of specification resulted in the 1983 paper "Specifying Concurrent Programming Modules", which introduced the idea of describing state transitions as boolean-valued functions of primed and unprimed variables.[12] Work continued throughout the 1980s, and Lamport began publishing papers on thetemporal logic of actions in 1990; however, it was not formally introduced until "The Temporal Logic of Actions" was published in 1994. TLA enabled the use ofactions in temporal formulas, which according to Lamport "provides an elegant way to formalize and systematize all the reasoning used in concurrent system verification."[13]

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.[1] Later that same year, Yuan Yu wrote the TLCmodel checker for TLA+ specifications; TLC was used to find errors in thecache coherence protocol for aCompaq multiprocessor.[14]

Lamport published a full textbook on TLA+ in 2002, titled "Specifying Systems: The TLA+ Language and Tools for Software Engineers".[15]PlusCal was introduced in 2009,[16] and the TLA+ proof system (TLAPS) in 2012.[17] TLA+2 was announced in 2014, adding some additional language constructs as well as greatly increasing in-language support for the proof system.[2] Lamport is engaged in creating an updated TLA+ reference, "The TLA+ Hyperbook". The incomplete work isavailable from his official website. Lamport is also creatingThe 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".

Language

[edit]

TLA+ specifications are organized into modules. Modules can extend (import) other modules to use their functionality. Although the TLA+ standard is specified in typeset mathematical symbols, existing TLA+ tools useLaTeX-like symbol definitions inASCII. TLA+ uses several terms which require definition:

  • State – an assignment of values to variables
  • Behaviour – a sequence of states
  • Step – a pair of successive states in a behavior
  • Stuttering step – a step during which variables are unchanged
  • Next-state relation – a relation describing how variables can change in any step
  • State function – an expression containing variables and constants that is not a next-state relation
  • State predicate – a Boolean-valued state function
  • Invariant – a state predicate true in all reachable states
  • Temporal formula – an expression containing statements in temporal logic

Safety

[edit]

TLA+ concerns itself with defining the set of all correct system behaviours. For example, a one-bit clock ticking endlessly between 0 and 1 could be specified as follows:

VARIABLE clockInit == clock \in {0, 1}Tick == IF clock = 0 THEN clock' = 1 ELSE clock' = 0Spec == Init /\ [][Tick]_<<clock>>

The next-state relationTick setsclock′ (the value ofclock in the next state) to 1 ifclock is 0, and 0 ifclock is 1. The state predicateInit is true if the value ofclock is either 0 or 1.Spec is a temporal formula asserting all behaviours of one-bit clock must initially satisfyInit and have all steps either matchTick or be stuttering steps. Two such behaviours are:

0 -> 1 -> 0 -> 1 -> 0 -> ...1 -> 0 -> 1 -> 0 -> 1 -> ...

The safety properties of the one-bit clock – the set of reachable system states – are adequately described by the spec.

Liveness

[edit]

The above spec disallows strange states for the one-bit clock, but does not say the clock will ever tick. For example, the following perpetually-stuttering behaviours are accepted:

0 -> 0 -> 0 -> 0 -> 0 -> ...1 -> 1 -> 1 -> 1 -> 1 -> ...

A clock which does not tick is not useful, so these behaviours should be disallowed. One solution is to disable stuttering, but TLA+ requires stuttering always be enabled; a stuttering step represents a change to some part of the system not described in the spec, and is useful forrefinement. To ensure the clock must eventually tick, weakfairness is asserted forTick:

Spec == Init /\ [][Tick]_<<clock>> /\ WF_<<clock>>(Tick)

Weak fairness over an action means if that action is continuously enabled, it must eventually be taken. With weak fairness onTick only a finite number of stuttering steps are permitted between ticks. This temporal logical statement aboutTick is called a liveness assertion. In general, a liveness assertion should bemachine-closed: it shouldn't constrain the set of reachable states, only the set of possible behaviours.[18]

Most specifications do not require assertion of liveness properties. Safety properties suffice both for model checking and guidance in system implementation.[19]

Operators

[edit]

TLA+ is based onZF, so operations on variables involve set manipulation. The language includes setmembership,union,intersection,difference,powerset, andsubset operators.First-order logic operators such as,,¬,,, are also included, as well asuniversal andexistential quantifiers and.Hilbert'sε is provided as the CHOOSE operator, which uniquely selects an arbitrary set element. Arithmetic operators overreals,integers, andnatural numbers are available from the standard modules.

Temporal logic operators are built into TLA+. Temporal formulas useP{\displaystyle \Box P} to meanP is always true, andP{\displaystyle \Diamond P} to meanP is eventually true. The operators are combined intoP{\displaystyle \Box \Diamond P} to meanP is true infinitely often, orP{\displaystyle \Diamond \Box P} to mean eventuallyP will always be true. Other temporal operators include weak and strong fairness. Weak fairness WFe(A) means if actionA is enabledcontinuously (i.e. without interruptions), it must eventually be taken. Strong fairness SFe(A) means if actionA is enabledcontinually (repeatedly, with or without interruptions), it must eventually be taken.

Temporal existential and universal quantification are included in TLA+, although without support from the tools.

User-defined operators are similar tomacros. Operators differ from functions in that their domain need not be a set: for example, theset membership operator has thecategory of sets as its domain, which isnot a valid set in ZFC (since its existence leads toRussell's paradox). Recursive and anonymous user-defined operators were added in TLA+2.

Data structures

[edit]

The foundational data structure of TLA+ is the set. Sets are either explicitly enumerated or constructed from other sets using operators or with{x\in S : p} wherep is some condition onx, or{e : x\in S} wheree is some function ofx. The uniqueempty set is represented as{}.

Functions in TLA+ assign a value to each element in their domain, a set.[S -> T] is the set of all functions with f[x] inT, for eachx in thedomain setS. For example, the TLA+ functionDouble[x \in Nat] == x*2 is an element of the set[Nat -> Nat] soDouble \in [Nat -> Nat] is a true statement in TLA+. Functions are also defined with[x \in S |-> e] for some expressione, or by modifying an existing function[f EXCEPT ![v1] = v2].

Records are a type of function in TLA+. The record[name |-> "John", age |-> 35] is a record with fields name and age, accessed withr.name andr.age, and belonging to the set of records[name : String, age : Nat].

Tuples are included in TLA+. They are explicitly defined with<<e1,e2,e3>> or constructed with operators from the standard Sequences module. Sets of tuples are defined byCartesian product; for example, the set of all pairs of natural numbers is definedNat \X Nat.

Standard modules

[edit]

TLA+ has a set of standard modules containing common operators. They are distributed with the syntactic analyzer. The TLC model checker uses Java implementations for improved performance.

  • FiniteSets: Module for working withfinite sets. ProvidesIsFiniteSet(S) andCardinality(S) operators.
  • Sequences: Defines operators ontuples such asLen(S),Head(S),Tail(S),Append(S, E),concatenation, andfilter.
  • Bags: Module for working withmultisets. Provides primitive set operation analogues and duplicate counting.
  • Naturals: Defines theNatural numbers along with inequality and arithmetic operators.
  • Integers: Defines theIntegers.
  • Reals: Defines theReal numbers along with division andinfinity.
  • RealTime: Provides definitions useful inreal-time system specifications.
  • TLC: Provides utility functions for model-checked specifications, such as logging and assertions.

Standard modules are imported with theEXTENDS orINSTANCE statements.

Tools

[edit]

IDE

[edit]
TLA+ Toolbox
TLA+ IDE in typical use showing spec explorer on the left, editor in the middle, and parse errors on the right.
Original author(s)Simon Zambrovski, Markus Kuppe, Daniel Ricketts
Developer(s)Hewlett-Packard,Microsoft
Initial releaseFebruary 4, 2010; 15 years ago (2010-02-04)
Stable release
1.7.2 Theano / February 2, 2022; 3 years ago (2022-02-02)
Preview release
1.8.0 Clarke / December 6, 2020; 4 years ago (2020-12-06)
Repositorygithub.com/tlaplus/tlaplus
Written inJava
Available inEnglish
TypeIntegrated development environment
LicenseMIT License
Websiteresearch.microsoft.com/en-us/um/people/lamport/tla/toolbox.html

Anintegrated development environment is implemented on top ofEclipse. It includes an editor with error andsyntax highlighting, plus aGUI front-end to several other TLA+ tools:

  • The SANY syntactic analyzer, which parses and checks the spec for syntax errors.
  • TheLaTeX translator, to generatepretty-printed specs.
  • The PlusCal translator.
  • The TLC model checker.
  • The TLAPS proof system.

The IDE is distributed inThe TLA Toolbox.

Model checker

[edit]
Finite state machine diagram of one-bit clock
States and transitions discovered by TLC for the one-bit clock.

The TLCmodel checker builds afinite state model of TLA+ specifications for checkinginvariance properties. TLC generates a set of initial states satisfying the spec, then performs abreadth-first search over all defined state transitions. Execution stops when all state transitions lead to states which have already been discovered. If TLC discovers a state which violates a system invariant, it halts and provides a state trace path to the offending state. TLC provides a method of declaring model symmetries to defend againstcombinatorial explosion.[14] It alsoparallelizes the state exploration step, and can run in distributed mode to spread the workload across a large number of computers.[20]

As an alternative to exhaustive breadth-first search, TLC can use depth-first search or generate random behaviours. TLC operates on a subset of TLA+; the model must be finite and enumerable, and some temporal operators are not supported. In distributed mode TLC cannot check liveness properties, nor check random or depth-first behaviours. TLC isavailable as a command line tool or bundled with the TLA toolbox.

Proof system

[edit]

The TLA+ Proof System, or TLAPS,mechanically checks proofs written in TLA+. It was developed at theMicrosoft Research-INRIA Joint Centre to prove correctness of concurrent and distributed algorithms. The proof language is designed to be independent of any particular theorem prover; proofs are written in a declarative style, and transformed into individual obligations which are sent to back-end provers. The primary back-end provers areIsabelle and Zenon, with fallback toSMT solversCVC3,Yices, andZ3. TLAPS proofs are hierarchically structured, easing refactoring and enabling non-linear development: work can begin on later steps before all prior steps are verified, and difficult steps are decomposed into smaller sub-steps. TLAPS works well with TLC, as the model checker quickly finds small errors before verification is begun. In turn, TLAPS can prove system properties which are beyond the capabilities of finite model checking.[17]

TLAPS does not currently support reasoning with real numbers, nor most temporal operators. Isabelle and Zenon generally cannot prove arithmetic proof obligations, requiring use of the SMT solvers.[21] TLAPS has been used to prove correctness ofByzantine Paxos, the Memoir security architecture, components of thePastry distributed hash table,[17] and the Spire consensus algorithm.[22] It is distributed separately from the rest of the TLA+ tools and is free software, distributed under theBSD license.[23] TLA+2 greatly expanded language support for proof constructs.

Industry use

[edit]

AtMicrosoft, a critical bug was discovered in theXbox 360 memory module during the process of writing a specification in TLA+.[24] TLA+ was used to write formal proofs of correctness forByzantine Paxos and components of thePastry distributed hash table.[17]

Amazon Web Services has used TLA+ since 2011. TLA+ model checking uncovered bugs inDynamoDB,S3,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.[4][25]

Microsoft Azure used TLA+ to designCosmos DB, a globally-distributed database with five differentconsistency models.[26][27]

Altreonic NV used TLA+ tomodel checkOpenComRTOS.

Examples

[edit]

Akey-value store withsnapshot isolation:

--------------------------- MODULE KeyValueStore ---------------------------CONSTANTS   Key,            \* The set of all keys.            Val,            \* The set of all values.            TxId            \* The set of all transaction IDs.VARIABLES   store,          \* A data store mapping keys to values.            tx,             \* The set of open snapshot transactions.            snapshotStore,  \* Snapshots of the store for each transaction.            written,        \* A log of writes performed within each transaction.            missed          \* The set of writes invisible to each transaction.----------------------------------------------------------------------------NoVal ==    \* Choose something to represent the absence of a value.    CHOOSE v : v \notin ValStore ==    \* The set of all key-value stores.    [Key -> Val \cup {NoVal}]Init == \* The initial predicate.    /\ store = [k \in Key |-> NoVal]        \* All store values are initially NoVal.    /\ tx = {}                              \* The set of open transactions is initially empty.    /\ snapshotStore =                      \* All snapshotStore values are initially NoVal.        [t \in TxId |-> [k \in Key |-> NoVal]]    /\ written = [t \in TxId |-> {}]        \* All write logs are initially empty.    /\ missed = [t \in TxId |-> {}]         \* All missed writes are initially empty.    TypeInvariant ==    \* The type invariant.    /\ store \in Store    /\ tx \subseteq TxId    /\ snapshotStore \in [TxId -> Store]    /\ written \in [TxId -> SUBSET Key]    /\ missed \in [TxId -> SUBSET Key]    TxLifecycle ==    /\ \A t \in tx :    \* If store != snapshot & we haven't written it, we must have missed a write.        \A k \in Key : (store[k] /= snapshotStore[t][k] /\ k \notin written[t]) => k \in missed[t]    /\ \A t \in TxId \ tx : \* Checks transactions are cleaned up after disposal.        /\ \A k \in Key : snapshotStore[t][k] = NoVal        /\ written[t] = {}        /\ missed[t] = {}OpenTx(t) ==    \* Open a new transaction.    /\ t \notin tx    /\ tx' = tx \cup {t}    /\ snapshotStore' = [snapshotStore EXCEPT ![t] = store]    /\ UNCHANGED <<written, missed, store>>Add(t, k, v) == \* Using transaction t, add value v to the store under key k.    /\ t \in tx    /\ snapshotStore[t][k] = NoVal    /\ snapshotStore' = [snapshotStore EXCEPT ![t][k] = v]    /\ written' = [written EXCEPT ![t] = @ \cup {k}]    /\ UNCHANGED <<tx, missed, store>>    Update(t, k, v) ==  \* Using transaction t, update the value associated with key k to v.    /\ t \in tx    /\ snapshotStore[t][k] \notin {NoVal, v}    /\ snapshotStore' = [snapshotStore EXCEPT ![t][k] = v]    /\ written' = [written EXCEPT ![t] = @ \cup {k}]    /\ UNCHANGED <<tx, missed, store>>    Remove(t, k) == \* Using transaction t, remove key k from the store.    /\ t \in tx    /\ snapshotStore[t][k] /= NoVal    /\ snapshotStore' = [snapshotStore EXCEPT ![t][k] = NoVal]    /\ written' = [written EXCEPT ![t] = @ \cup {k}]    /\ UNCHANGED <<tx, missed, store>>    RollbackTx(t) ==    \* Close the transaction without merging writes into store.    /\ t \in tx    /\ tx' = tx \ {t}    /\ snapshotStore' = [snapshotStore EXCEPT ![t] = [k \in Key |-> NoVal]]    /\ written' = [written EXCEPT ![t] = {}]    /\ missed' = [missed EXCEPT ![t] = {}]    /\ UNCHANGED storeCloseTx(t) ==   \* Close transaction t, merging writes into store.    /\ t \in tx    /\ missed[t] \cap written[t] = {}   \* Detection of write-write conflicts.    /\ store' =                         \* Merge snapshotStore writes into store.        [k \in Key |-> IF k \in written[t] THEN snapshotStore[t][k] ELSE store[k]]    /\ tx' = tx \ {t}    /\ missed' =    \* Update the missed writes for other open transactions.        [otherTx \in TxId |-> IF otherTx \in tx' THEN missed[otherTx] \cup written[t] ELSE {}]    /\ snapshotStore' = [snapshotStore EXCEPT ![t] = [k \in Key |-> NoVal]]    /\ written' = [written EXCEPT ![t] = {}]Next == \* The next-state relation.    \/ \E t \in TxId : OpenTx(t)    \/ \E t \in tx : \E k \in Key : \E v \in Val : Add(t, k, v)    \/ \E t \in tx : \E k \in Key : \E v \in Val : Update(t, k, v)    \/ \E t \in tx : \E k \in Key : Remove(t, k)    \/ \E t \in tx : RollbackTx(t)    \/ \E t \in tx : CloseTx(t)        Spec == \* Initialize state with Init and transition with Next.    Init /\ [][Next]_<<store, tx, snapshotStore, written, missed>>----------------------------------------------------------------------------THEOREM Spec => [](TypeInvariant /\ TxLifecycle)=============================================================================

See also

[edit]

References

[edit]
  1. ^abLamport, Leslie (January 2000).Specifying Concurrent Systems with TLA+(PDF). NATO Science Series, III: Computer and Systems Sciences. Vol. 173. Amsterdam: IOS Press. pp. 183–247.ISBN 978-90-5199-459-9. Retrieved22 May 2015.
  2. ^abLamport, Leslie (15 January 2014)."TLA+2: A Preliminary Guide"(PDF). Retrieved2 May 2015.
  3. ^"Tlaplus Tools - License".CodePlex.Microsoft,Compaq. 8 April 2013. Retrieved10 May 2015.[permanent dead link]https://tlaplus.codeplex.com/license[permanent dead link]
  4. ^abNewcombe, Chris; Rath, Tim; Zhang, Fan; Munteanu, Bogdan; Brooker, Marc; Deardeuff, Michael (29 September 2014)."Use of Formal Methods at Amazon Web Services"(PDF).Amazon. Retrieved8 May 2015.
  5. ^Lamport, Leslie (25 January 2013)."Why We Should Build Software Like We Build Houses".Wired. Retrieved7 May 2015.
  6. ^Lamport, Leslie (18 June 2002)."7.1 Why Specify".Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers.Addison-Wesley. p. 75.ISBN 978-0-321-14306-8.Having to describe a design precisely often reveals problems - subtle interactions and "corner cases" that are easily overlooked.
  7. ^Lamport, Leslie (2012)."How to Write a 21st Century Proof"(PDF).Journal of Fixed Point Theory and Applications.11:43–63.doi:10.1007/s11784-012-0071-6.ISSN 1661-7738.S2CID 121557270. Retrieved23 May 2015.
  8. ^Øhrstrøm, Peter; Hasle, Per (1995). "3.7 Temporal Logic and Computer Science".Temporal Logic: From Ancient Ideas to Artificial Intelligence. Studies in Linguistics and Philosophy. Vol. 57.Springer Netherlands. pp. 344–365.doi:10.1007/978-0-585-37463-5.ISBN 978-0-7923-3586-3.
  9. ^Lamport, Leslie."The Writings of Leslie Lamport: Proving the Correctness of Multiprocess Programs". Retrieved22 May 2015.
  10. ^Lamport, Leslie."The Writings of Leslie Lamport: On-the-fly Garbage Collection: an Exercise in Cooperation". Retrieved22 May 2015.
  11. ^Lamport, Leslie."The Writings of Leslie Lamport: 'Sometime' is Sometimes 'Not Never'". Retrieved22 May 2015.
  12. ^abLamport, Leslie."The Writings of Leslie Lamport: Specifying Concurrent Programming Modules". Retrieved22 May 2015.
  13. ^Lamport, Leslie."The Writings of Leslie Lamport: The Temporal Logic of Actions". Retrieved22 May 2015.
  14. ^abYu, Yuan; Manolios, Panagiotis;Lamport, Leslie (1999). "Model Checking TLA+ Specifications".Correct Hardware Design and Verification Methods(PDF). Lecture Notes in Computer Science. Vol. 1703.Springer-Verlag. pp. 54–66.doi:10.1007/3-540-48153-2_6.ISBN 978-3-540-66559-5. Retrieved14 May 2015.
  15. ^Lamport, Leslie (18 June 2002).Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers.Addison-Wesley.ISBN 978-0-321-14306-8.
  16. ^Lamport, Leslie (2 January 2009)."The PlusCal Algorithm Language"(PDF).Theoretical Aspects of Computing - ICTAC 2009. Lecture Notes in Computer Science. Vol. 5684.Springer Berlin Heidelberg. pp. 36–60.doi:10.1007/978-3-642-03466-4_2.ISBN 978-3-642-03465-7. Retrieved10 May 2015.
  17. ^abcdCousineau, Denis; Doligez, Damien;Lamport, Leslie; Merz, Stephan; Ricketts, Daniel; Vanzetto, Hernán (1 January 2012). "TLA+ Proofs".FM 2012: Formal Methods(PDF). Lecture Notes in Computer Science. Vol. 7436.Springer Berlin Heidelberg. pp. 147–154.doi:10.1007/978-3-642-32759-9_14.ISBN 978-3-642-32758-2.S2CID 5243433. Retrieved14 May 2015.
  18. ^Lamport, Leslie (18 June 2002)."8.9.2 Machine Closure".Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers.Addison-Wesley. p. 112.ISBN 978-0-321-14306-8.We seldom want to write a specification that isn't machine closed. If we do write one, it's usually by mistake.
  19. ^Lamport, Leslie (18 June 2002)."8.9.6 Temporal Logic Considered Confusing".Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers.Addison-Wesley. p. 116.ISBN 978-0-321-14306-8.Indeed, [most engineers] can get along quite well with specifications of the form (8.38) that express only safety properties and don't hide any variables.
  20. ^Markus A. Kuppe (3 June 2014).Distributed TLC (Recording of technical talk). TLA+ Community Event 2014, Toulouse, France.{{cite AV media}}: CS1 maint: location (link)
  21. ^"Unsupported TLAPS features".TLA+ Proof System.Microsoft Research -INRIA Joint Centre. Retrieved14 May 2015.
  22. ^Koutanov, Emil (12 July 2021)."Spire: A Cooperative, Phase-Symmetric Solution to Distributed Consensus".IEEE Access.9.IEEE:101702–101717.Bibcode:2021IEEEA...9j1702K.doi:10.1109/ACCESS.2021.3096326.S2CID 236480167.
  23. ^TLA+ Proof System
  24. ^Leslie Lamport (3 April 2014).Thinking for Programmers (at 21m46s) (Recording of technical talk). San Francisco:Microsoft. Retrieved14 May 2015.
  25. ^Chris, Newcombe (2014). "Why Amazon Chose TLA+".Abstract State Machines, Alloy, B, TLA, VDM, and Z. Lecture Notes in Computer Science. Vol. 8477.Springer Berlin Heidelberg. pp. 25–39.doi:10.1007/978-3-662-43652-3_3.ISBN 978-3-662-43651-6.
  26. ^Lardinois, Frederic (10 May 2017)."With Cosmos DB, Microsoft wants to build one database to rule them all".TechCrunch. Retrieved10 May 2017.
  27. ^Leslie Lamport (10 May 2017).Foundations of Azure Cosmos DB with Dr. Leslie Lamport (Recording of interview).Microsoft Azure. Retrieved10 May 2017.
Retrieved from "https://en.wikipedia.org/w/index.php?title=TLA%2B&oldid=1269943185#IDE"
Categories:
Hidden categories:

[8]ページ先頭

©2009-2025 Movatter.jp