Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers

By Leslie Lamport. 2002

638 citations recorded by the source corpus.

View Paper: https://www.semanticscholar.org/paper/0170c2746dde3ed5bff4c2c1b0ccb3e0037cfe9e

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

Citations in the corpus

A computational model for TensorFlow: an introduction (2017, background): “It is presented in English, for the sake of readability, but it is as detailed as a logical speciﬁcation; indeed, it is largely a paraphrase of a logical formulation previously written in TLA [14].”
Component-Based Software Engineering (2005, background): “The same results can be found about transitions systems and the temporal logic of actions [ 22 ,25].”
IronFleet: proving practical distributed systems correct (2015, methodology): “Lamport [36] suggests that such properties take the form “if action A becomes always enabled, i.”
Rodin: an open toolset for modelling and reasoning in Event-B (2010, methodology): “The grammar has not been speciﬁed in Event-B, although, in principle this should be possible similarly to the technique proposed by Lamport based on TLA+ [28].”
Practical verification of decision-making in agent-based autonomous systems (2013, methodology): “Using standard assume-guarantee (or relyguarantee) approaches (Misra andChandy 1981; Jones 1983, 1986;Manna and Pnueli 1992; Lamport 2003), we need only check the internal operation of a single agent at a time and can then combine the results from the model checking using deductive methods to prove ”
Multifacet's general execution-driven multiprocessor simulator (GEMS) toolset (2005, methodology): “Cache Coherence Verification with TLA+.”
Modeling in event-b - system and software engineering by Jean-Raymond Abrial (2010, unknown): “敗は、モデルの誤りと不足が何であるかを知る重要な手がかりを与えてくれる。この本で使用する形式は Event-Bという名前である。Event-Bは B形式 [1]の拡張であると同時に単純化でもある。Bは 10年前に開発され、すでにいくつかの大きな産業プロジェクト [4, 3]で使われている。Event-B のような形式のコンセプトは目新しいものではない。Event-B の原型となる多数の形式――Action Systems [6]、TLA [2]、VDM [15]、UNITY [5]など――が長い時間をかけて提案されてきた。この本は例を中心に構成されている。それぞれの章は新しい例 (複数で”
In Search of an Understandable Consensus Algorithm (2014, methodology): “The formal specification [31] makes the information summarized in Figure 2 completely precise using the TLA+ specification language [17].”