TLA +

TLA +
パラダイム	アクション
デザイン：	レスリー・ランポート
初登場	1999年4月23日[ 1 ] （1999年4月23日）
安定版リリース	TLA +2 / 2014 年 1 月 15 日[ 2 ] （2014年1月15日）
実装言語	ジャワ
OS	クロスプラットフォーム（マルチプラットフォーム）
ライセンス	MITライセンス[ 3 ]
ファイル名拡張子	.tla
Webサイト	tlapl.us​

TLA ^+は、レスリー・ランポートによって開発された形式仕様言語です。プログラム、特に並行システムや分散システムの設計、モデリング、ドキュメント作成、検証に用いられます。TLA ^{+は網羅的にテスト可能な}擬似コードであると考えられており^{[ 4 ]}、その使用法はソフトウェアシステムの設計図を描くことに例えられます^{[ 5 ]}。TLAはTemporal Logic of Actionsの略称です。

設計と文書化に関しては、TLA ^{+は非公式な}技術仕様と同じ目的を果たします。しかし、TLA ^+仕様は論理と数学の形式言語で記述されており、この言語で記述された仕様の精度は、システム実装が開始される前に設計上の欠陥を発見することを目的としています。^{[ 6 ]}

TLA ⁺仕様は形式言語で記述されているため、有限モデル検査に適しています。モデルチェッカーは、実行ステップ数までのすべての可能なシステム動作を検出し、安全性や活性といった望ましい不変性プロパティの違反を検査します。TLA ⁺仕様では、安全性（悪いことは起こらない）を定義するために基本集合論を使用し、活性（良いことは最終的に起こる）を定義するために時相論理を使用します。

TLA ^+は、アルゴリズムと数学定理の両方について、機械検証された正しさの証明を書くためにも用いられます。証明は、特定の定理証明器のバックエンドに依存しない、宣言的かつ階層的なスタイルで記述されます。TLA ⁺では、形式的および非形式的な構造化された数学的証明を記述できます。この言語はLaTeXに似ており、TLA ^+の仕様をLaTeX文書に変換するツールも存在します。^{[ 7 ]}

TLA ^+は、並行システムの検証手法に関する数十年にわたる研究を経て、1999年に導入されました。それ以来、IDEや分散モデルチェッカーを含むツールチェーンが開発されてきました。擬似コード風言語PlusCalは2009年に開発され、TLA ^+にトランスパイルでき、逐次アルゴリズムの仕様記述に役立ちます。TLA ⁺²は2014年に発表され、証明構造の言語サポートが拡張されました。現在のTLA ^{+の参考文献は、レスリー・ランポート著の『} The TLA ⁺ Hyperbook』です。

歴史

アミール・プヌエリは時相論理をコンピュータサイエンスに応用し、1996 年にチューリング賞を受賞しました。

現代の時相論理は1957年にアーサー・プライアによって開発され、当時は時制論理と呼ばれていました。時相論理のコンピュータサイエンスへの応用を真剣に研究したのはアミール・プヌエリが初めてでしたが、プライアはそれより10年前の1967年に、その用途について推測していました。

この種のシステム（離散時間に関するシステム）の有用性は、時間が離散的であるという深刻な形而上学的仮定には依存しません。これらのシステムは、一連の離散状態において次に何が起こるかだけを対象とする限定された議論分野、たとえばデジタルコンピュータの動作において適用可能です。

プヌエリはコンピュータプログラムの仕様記述と推論における時相論理の利用を研究し、 1977年に線形時相論理を導入した。LTLは並行プログラムの解析において重要なツールとなり、相互排他性やデッドロックの回避などの特性を容易に表現できるようになった。^{[ 8 ]}

プヌエリのLTL研究と並行して、研究者たちはマルチプロセスプログラムの検証にホーア論理を一般化しようと取り組んでいた。レスリー・ランポートは、相互排他性に関する論文を査読で誤りが見つかったことをきっかけに、この問題に興味を持つようになった。エド・アシュクロフトは1975年の論文「並列プログラムに関するアサーションの証明」で不変性を導入し、ランポートはこれを用いて1977年の論文「マルチプロセスプログラムの正しさの証明」でフロイドの手法を一般化した。ランポートの論文では、安全性と生存性も、それぞれ部分的正しさと停止性の一般化として導入された。^{[ 9 ]}この手法は、エドガー・ダイクストラと共同で1978年に発表した論文で、最初の並行ガベージコレクションアルゴリズムの検証に使用された。^{[ 10 ]}

ランポートがプヌエリのLTLに初めて出会ったのは、1978年にスタンフォード大学でスーザン・オウィッキが主催したセミナーでした。ランポートによると、「私は時相論理は実用的ではない抽象的なナンセンスだと考えていましたが、面白そうだったので参加しました。」1980年に彼は「『いつか』は『決してない』ではない」という論文を発表しました。これは時相論理の文献の中で最も頻繁に引用される論文の一つとなりました。^{[ 11 ]}ランポートはSRI在籍中に時相論理の仕様書の作成に取り組みましたが、そのアプローチは非実用的であることがわかりました。

TLA ^{+ は}、コンピューター科学者であり 2013 年のチューリング賞受賞者であるLeslie Lamportによって開発されました。

しかし、シュワルツ、メリアー＝スミス、フリッツ・フォークトが単純なFIFOキューの仕様を定めようと何日も費やし 、列挙した特性が十分かどうかを議論しているのを見て、私は時相論理に幻滅しました。時相特性の集合として仕様を記述することは、見た目は魅力的ですが、実際にはうまくいかないことに気づきました。^{[ 12 ]}

実用的な仕様記述法の探求は、1983年の論文「並行プログラミングモジュールの仕様記述」に結実し、この論文では、状態遷移をプライム付き変数とプライムなし変数のブール値関数として記述するという考え方が紹介されました。^{[ 12 ]}研究は1980年代を通して続けられ、ラムポートは1990年にアクションの時相論理に関する論文を発表し始めました。しかし、正式に導入されたのは1994年に「アクションの時相論理」が出版された時でした。TLAは時相式におけるアクションの使用を可能にし、ラムポートによれば「並行システムの検証で使用されるすべての推論を形式化し体系化するエレガントな方法を提供する」ものでした。^{[ 13 ]}

TLA仕様は主に通常の非時間的数学で構成されており、ラムポートは純粋に時間的な仕様よりも扱いやすいと考えた。TLAは、1999年に論文「TLA ^{+による並行システムの仕様化」で導入された仕様言語TLA +の数学的基盤を提供した。 [ 1 ]}同年、ユアン・ユーはTLA ^{+仕様用のTLC}モデルチェッカーを作成した。TLCは、コンパック製マルチプロセッサのキャッシュコヒーレンスプロトコルにおけるエラー検出に使用された。^{[ 14 ]}

ラムポート氏は2002年にTLA ⁺の完全な教科書『Specifying Systems: The TLA ⁺ Language and Tools for Software Engineers』を出版した。^{[ 15 ]} PlusCalは2009年に導入され、^{[ 16 ]} TLA ⁺証明システム（TLAPS）は2012年に導入された。 ^{[ 17 ]} TLA ⁺²は2014年に発表され、いくつかの言語構成要素が追加され、証明システムの言語内サポートが大幅に強化された。^{[ 2 ]ラムポート氏はTLA +}リファレンスの最新版『The TLA ⁺ Hyperbook』の作成に取り組んでいる。未完成の作品は公式ウェブサイトから入手できる。ラムポート氏はまた、 TLA ⁺ビデオコースも作成中で、その中で「プログラマーやソフトウェアエンジニアに独自のTLA ⁺仕様の書き方を教える一連のビデオ講義の始まりとなる進行中の作業」と説明されている。

言語

TLA ⁺仕様はモジュールで構成されています。モジュールは他のモジュールを拡張（インポート）して、その機能を利用することができます。TLA ⁺規格は活字体による数学記号で規定されていますが、既存のTLA ⁺ツールではLaTeX風のASCII形式の記号定義が使用されています。TLA ⁺では、定義が必要な用語がいくつか使用されています。

• 状態– 変数への値の割り当て
• 行動– 一連の状態
• ステップ– 行動における連続した状態のペア
• スタッターステップ– 変数が変化しないステップ
• 次の状態関係- 変数がどのステップでどのように変化するかを説明する関係
• 状態関数- 次の状態関係ではない変数と定数を含む式
• 状態述語– ブール値の状態関数
• 不変– 到達可能なすべての状態において真である状態述語
• 時相式– 時相論理の文を含む表現

安全性

TLA ^+は、すべての正しいシステム動作の集合を定義することに重点を置きます。例えば、0と1の間を無限に刻む1ビットのクロックは、次のように定義できます。

可変クロック 初期化 == クロック \in {0, 1} ティック == IF clock = 0 THEN clock' = 1 ELSE clock' = 0 仕様 == Init /\ [][Tick]_<<clock>> 

次状態関係Tickは、クロックが0の場合クロック′（次状態におけるクロックの値）を1に設定し、クロックが1の場合クロック′を0に設定します。状態述語Initは、クロックの値が0または1の場合に真となります。Specは、1ビットクロックのすべての動作が最初にInitを満たし、すべてのステップがTickと一致するか、スタッターステップであることを示す時間式です。このような動作には次の2つがあります。

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

1 ビット クロックの安全性の特性 (到達可能なシステム状態のセット) は、仕様によって適切に説明されています。

ライブネス

上記の仕様では、1ビットクロックの異常な状態は許容されませんが、クロックが常に動作し続けるとは明記されていません。例えば、以下のような、常にカクカクする動作は許容されます。

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

刻みを刻まないクロックは役に立たないので、これらの動作は禁止されるべきです。解決策の一つはスタッタリングを無効にすることですが、TLA ⁺ではスタッタリングが常に有効である必要があります。スタッタリングは、仕様に記載されていないシステムの一部への変更を表し、改良に役立ちます。クロックが最終的に刻みを刻むことを保証するために、Tickに対して弱い公平性が主張されます。

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

ある動作に対する弱い公平性とは、その動作が継続的に有効である場合、最終的には必ず実行されることを意味します。Tickに対する弱い公平性では、ティック間のスタッターステップは有限個しか許容されません。Tickに関するこの時相論理ステートメントは、生存表明と呼ばれます。一般に、生存表明は機械閉包であるべきです。つまり、到達可能な状態の集合を制約するのではなく、可能な動作の集合のみを制約すべきです。^{[ 18 ]}

ほとんどの仕様では、活性特性の表明は要求されていません。安全性特性は、モデル検証とシステム実装のガイダンスの両方に十分です。^{[ 19 ]}

オペレーター

TLA ^+はZFに基づいているため、変数に対する演算には集合操作が含まれます。この言語には、集合の所属、和集合、積集合、差集合、べき集合、部分集合の演算子が含まれます。∨ 、∧ 、 ¬ 、⇒、↔、≡などの一階論理演算子に加え、全称量指定子∀および存在量指定子∃も含まれています。ヒルベルトのεは、任意の集合要素を一意に選択する CHOOSE 演算子として提供されています。実数、整数、自然数に対する算術演算子は、標準モジュールから利用できます。

TLA ⁺には時相論理演算子が組み込まれています。時相式は、 はPが常に真であることを意味し、はPが最終的に真であることを意味します。これらの演算子は、 と組み合わされて、 Pが無限に真であることを意味するか、最終的にはPが常に真であることを意味します。その他の時相演算子には、弱い公平性と強い公平性があります。弱い公平性 WF _e ( A ) は、アクションAが継続的に（つまり、中断なしで）有効になっている場合、最終的には必ず実行されることを意味します。強い公平性 SF _e ( A ) は、アクションAが継続的に（繰り返し、中断の有無にかかわらず）有効になっている場合、最終的には必ず実行されることを意味します。 ${\displaystyle \Box P}$ ${\displaystyle \Diamond P}$ ${\displaystyle \Box \Diamond P}$ ${\displaystyle \Diamond \Box P}$

TLA ⁺には時間的存在量化と普遍量化が含まれていますが、ツールからのサポートはありません。

ユーザー定義演算子はマクロに似ています。演算子は関数とは異なり、定義域が集合である必要はありません。例えば、集合の所属演算子は集合のカテゴリを定義域としますが、これはZFCでは有効な集合ではありません（その存在はラッセルのパラドックスにつながるため）。再帰演算子と匿名ユーザー定義演算子はTLA ⁺²で追加されました。

データ構造

^{TLA +}の基本的なデータ構造は集合です。集合は明示的に列挙されるか、演算子 または を用いて他の集合から構築されます。ここでpはxに関する何らかの条件、またはeはxに関する何らかの関数です。唯一の空集合は と表されます。 {x \in S : p}{e : x \in S}{}

TLA ^+の関数は、定義域の各要素（集合）に値を割り当てます。は、定義域集合Sの各xに対して、 Tに f[ x ][S -> T]を持つすべての関数の集合です。例えば、TLA ⁺関数は集合 の要素であるため、 TLA ⁺では は真です。関数は、何らかの式eに対して で定義されるか、既存の関数 を変更することによっても定義されます。 Double[x \in Nat] == x*2[Nat -> Nat]Double \in [Nat -> Nat][x \in S |-> e][f EXCEPT ![v1] = v2]

レコードはTLA ⁺における関数の一種です。レコード[name |-> "John", age |-> 35]は、フィールド名と年齢を持つレコードであり、およびでアクセスされr.name、r.ageレコード集合に属します[name : String, age : Nat]。

タプルはTLA ⁺に含まれています。タプルは標準のSequencesモジュールの演算子を用いて明示的に定義または構築されます。タプルの集合は直積によって定義されます。例えば、すべての自然数のペアの集合は として定義されます。 <<e1,e2,e3>>Nat \X Nat

標準モジュール

TLA ^+には、一般的な演算子を含む標準モジュールのセットが用意されています。これらは構文解析器とともに配布されます。TLCモデルチェッカーは、パフォーマンス向上のためにJava実装を使用しています。

• FiniteSets :有限集合を扱うためのモジュール。IsFiniteSet (S)およびCardinality(S)演算子を提供します。
• シーケンス: Len(S)、Head(S)、Tail(S)、Append(S, E)、concatenation、filterなどのタプルの演算子を定義します。
• Bags :多重集合を扱うためのモジュール。基本的な集合演算の類似機能と重複カウント機能を提供します。
• 自然数:自然数、不等式、算術演算子を定義します。
• 整数:整数を定義します。
• 実数:除算と無限大とともに実数を定義します。
• RealTime :リアルタイム システムの仕様に役立つ定義を提供します。
• TLC : ログ記録やアサーションなどのモデルチェック仕様のユーティリティ関数を提供します。

標準モジュールは、EXTENDSorINSTANCEステートメントを使用してインポートされます。

ツール

IDE

TLA +ツールボックス
TLA + IDE の典型的な使用法では、左側に仕様エクスプローラー、中央にエディター、右側に解析エラーが表示されます。
原作者	サイモン・ザンブロフスキー、マルクス・クッペ、ダニエル・リケッツ
開発者	ヒューレット・パッカード、マイクロソフト
初回リリース	2010年2月4日 （2010年2月4日）
安定版リリース	1.7.2 Theano / 2022年2月2日 ( 2022-02-02 )
プレビューリリース	1.8.0 クラーク / 2020年12月6日 ( 2020-12-06 )
書かれた	ジャワ
入手可能な	英語
タイプ	統合開発環境
ライセンス	MITライセンス
Webサイト	研究.microsoft .com /en-us /um /people /lamport /tla /toolbox .html
リポジトリ	github .com /tlaplus /tlaplus

統合開発環境はEclipse上に実装されています。エラーと構文の強調表示機能を備えたエディタに加え、他のTLA ⁺ツール へのGUIフロントエンドが含まれています。

• SANY 構文アナライザーは、仕様を解析して構文エラーをチェックします。
• きれいに印刷される仕様を生成するLaTeXトランスレータ。
• PlusCal 翻訳機。
• TLC モデルチェッカー。
• TLAPS 証明システム。

IDE はTLA Toolboxで配布されます。

モデルチェッカー

1 ビット クロックに対して TLC によって検出された状態と遷移。

TLCモデルチェッカーは、不変性プロパティを検査するためのTLA ⁺仕様の有限状態モデルを構築します。TLCは仕様を満たす初期状態のセットを生成し、定義されたすべての状態遷移に対して幅優先探索を実行します。すべての状態遷移がすでに発見されている状態につながると、実行は停止します。TLCがシステム不変条件に違反する状態を発見した場合、TLCは停止し、問題のある状態への状態トレースパスを提供します。TLCは、組み合わせ爆発を防ぐため、モデルの対称性を宣言する方法を提供します。^{[ 14 ]}また、状態探索ステップを並列化し、多数のコンピュータにワークロードを分散するために分散モードで実行できます。^{[ 20 ]}

TLCは、網羅的な幅優先探索の代替として、深さ優先探索を使用したり、ランダムな動作を生成したりできます。TLCはTLA ⁺のサブセットで動作します。モデルは有限かつ列挙可能である必要があり、一部の時間演算子はサポートされていません。分散モードでは、TLCは活性プロパティをチェックできず、ランダムまたは深さ優先動作もチェックできません。TLCはコマンドラインツールとして、またはTLAツールボックスにバンドルされて提供されます。

証明システム

TLA ⁺証明システム（TLAPS）は、 TLA ⁺で記述された証明を機械的に検証します。これは、並行および分散アルゴリズムの正しさを証明するために、 Microsoft Research - INRIA Joint Centreで開発されました。この証明言語は、特定の定理証明器に依存しないように設計されており、証明は宣言的なスタイルで記述され、個々の義務に変換されてバックエンド証明器に送られます。主要なバックエンド証明器はIsabelleとZenonで、 SMTソルバーであるCVC3、Yices、Z3がフォールバックとして使用されます。TLAPSの証明は階層的に構造化されており、リファクタリングを容易にし、非線形開発を可能にします。つまり、すべての先行ステップが検証される前に後のステップの作業を開始でき、難しいステップはより小さなサブステップに分解されます。TLAPSはTLCと相性が良く、モデルチェッカーは検証開始前に小さなエラーを迅速に検出します。その結果、TLAPSは有限モデル検査の能力を超えるシステム特性を証明できます。^{[ 17 ]}

TLAPSは現在、実数やほとんどの時間演算子を使った推論をサポートしていません。IsabelleとZenonは一般に算術証明義務を証明できないため、SMTソルバーを使用する必要があります。^{[ 21 ]} TLAPSは、ビザンチンPaxos、Memoirセキュリティアーキテクチャ、Pastry分散ハッシュテーブルのコンポーネント、^{[ 17 ]}、およびSpireコンセンサスアルゴリズムの正しさを証明するために使用されてきました。^{[ 22 ]} TLAPSは、他のTLA ^{+ツールとは別に配布されており、} BSDライセンスの下で配布されるフリーソフトウェアです。^{[ 23 ]} TLA ^+2では、証明構造の言語サポートが大幅に拡張されました。

産業用途

マイクロソフトでは、TLA ⁺で仕様を書いている途中で、Xbox 360のメモリモジュールに重大なバグが発見された。^{[ 24 ]} TLA ^+はビザンチン・パクソスとPastry分散ハッシュテーブルのコンポーネントの正当性の正式な証明を書くために使われた。^{[ 17 ]}

Amazon Web Servicesは2011年からTLA ^{+を使用しています。TLA +モデル検査により、} DynamoDB、S3、EBS 、そして内部分散ロックマネージャにバグが発見されました。バグによっては、35ステップの状態トレースが必要でした。モデル検査は、積極的な最適化の検証にも使用されました。さらに、TLA ⁺仕様はドキュメント作成や設計支援としての価値を持つことが分かりました。^{[ 4 ] [ 25 ]}

Microsoft AzureはTLA ^{+を使用して、5つの異なる}整合性モデルを備えたグローバル分散データベースであるCosmos DBを設計しました。^{[ 26 ] [ 27 ]}

Altreonic NV は、TLA ^{+を使用して}OpenComRTOS のモデルチェックを 行いました。

例

スナップショット分離を備えたキーバリューストア:

--------------------------- モジュール KeyValueStore --------------------------- 定数 Key、\* すべてのキーのセット。 Val、\* すべての値のセット。 TxId \* すべてのトランザクション ID のセット。 VARIABLES ストア、\* キーを値にマッピングするデータ ストア。 tx, \* 開いているスナップショットトランザクションのセット。 snapshotStore、\* 各トランザクションのストアのスナップショット。 written、\* 各トランザクション内で実行された書き込みのログ。 欠落 \* 各トランザクションに対して非表示の書き込みセット。 ---------------------------------------------------------------------------- NoVal == \* 値の欠如を表すものを選択します。 v を選択: v \notin Val Store == \* すべてのキー値ストアのセット。 [キー -> 値 \cup {NoVal}] Init == \* 初期述語。 /\ store = [k \in Key |-> NoVal] \* すべてのストア値は最初は NoVal です。 /\ tx = {} \* オープントランザクションのセットは最初は空です。 /\ snapshotStore = \* すべての snapshotStore 値は最初は NoVal です。 [t \in TxId |-> [k \in キー |-> NoVal]] /\ written = [t \in TxId |-> {}] \* すべての書き込みログは最初は空です。 /\ missed = [t \in TxId |-> {}] \* 失敗した書き込みはすべて最初は空です。 TypeInvariant == \* 型不変。 /\ ストア \ ストア内 /\ tx \subseteq TxId /\ snapshotStore \in [TxId -> ストア] /\ 書き込まれた \in [TxId -> SUBSET Key] /\ が見つかりません \in [TxId -> SUBSET Key] トランザクションライフサイクル == /\ \A t \in tx : \* store != snapshot かつ、まだ書き込んでいない場合は、書き込みを逃したことになります。 \A k \in キー: (store[k] /= snapshotStore[t][k] /\ k \notin written[t]) => k \in missed[t] /\ \A t \in TxId \ tx : \* トランザクションが破棄後にクリーンアップされているかどうかを確認します。 /\ \A k \in キー: snapshotStore[t][k] = NoVal /\ 書かれた[t] = {} /\ ミス[t] = {} OpenTx(t) == \* 新しいトランザクションを開きます。 /\ t \notin tx /\ tx' = tx \cup {t} /\ snapshotStore' = [snapshotStore EXCEPT ![t] = store] /\ 変更なし <<書き込まれた、見逃された、保存>> Add(t, k, v) == \* トランザクション t を使用して、キー k の下のストアに値 v を追加します。 /\ t \in tx /\ スナップショットストア[t][k] = NoVal /\ snapshotStore' = [snapshotStore 例外 ![t][k] = v] /\ written' = [ただし ![t] = @ \cup {k} を除く] /\ 変更なし <<tx、ミス、ストア>> Update(t, k, v) == \* トランザクション t を使用して、キー k に関連付けられた値を v に更新します。 /\ t \in tx /\ snapshotStore[t][k] \notin {NoVal, v} /\ snapshotStore' = [snapshotStore 例外 ![t][k] = v] /\ written' = [ただし ![t] = @ \cup {k} を除く] /\ 変更なし <<tx、ミス、ストア>> Remove(t, k) == \* トランザクション t を使用して、ストアからキー k を削除します。 /\ t \in tx /\ スナップショットストア[t][k] /= 値なし /\ snapshotStore' = [snapshotStore EXCEPT ![t][k] = NoVal] /\ written' = [ただし ![t] = @ \cup {k} を除く] /\ 変更なし <<tx、ミス、ストア>> RollbackTx(t) == \* 書き込みをストアにマージせずにトランザクションを閉じます。 /\ t \in tx /\ tx' = tx \ {t} /\ snapshotStore' = [snapshotStore EXCEPT ![t] = [k \in Key |-> NoVal]] /\ written' = [write EXCEPT ![t] = {}] /\ missed' = [missed EXCEPT ![t] = {}] /\ 変更なしストア CloseTx(t) == \* トランザクション t を閉じ、書き込みをストアにマージします。 /\ t \in tx /\ missed[t] \cap written[t] = {} \* 書き込み-書き込み競合の検出。 /\ store' = \* snapshotStore の書き込みをストアにマージします。 [k \in Key |-> IF k \in written[t] THEN snapshotStore[t][k] ELSE store[k]] /\ tx' = tx \ {t} /\ missed' = \* 他の開いているトランザクションの失敗した書き込みを更新します。 [otherTx \in TxId |-> IF otherTx \in tx' THEN missed[otherTx] \cup written[t] ELSE {}] /\ snapshotStore' = [snapshotStore EXCEPT ![t] = [k \in Key |-> NoVal]] /\ written' = [write EXCEPT ![t] = {}] Next == \* 次の状態の関係。 \/ \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 == \* Init で状態を初期化し、Next で遷移します。 初期化 /\ [][次へ]_<<ストア、トランザクション、スナップショットストア、書き込み済み、欠落>> ---------------------------------------------------------------------------- 定理仕様 => [](TypeInvariant /\ TxLifecycle) ============================================================================= 

参照

• 連続したプロセスの伝達
• Alloy（仕様言語）
• Bメソッド
• 計算ツリーロジック
• プラスカル
• 時相論理
• 行動の時間的論理
• Z表記

参考文献

1. ランポート、レスリー（2000年1月）。TLA ⁺による並行システムの仕様策定（PDF） 。NATO科学シリーズIII：コンピュータとシステム科学。第173巻。アムステルダム：IOSプレス。pp.  183– 247。ISBN 978-90-5199-459-9. 2015年5月22日閲覧。
2. Lamport, Leslie (2014年1月15日). 「TLA ⁺² : 予備ガイド」(PDF) . 2015年5月2日閲覧。
3. "Tlaplus Tools - License" . CodePlex . Microsoft , Compaq . 2013年4月8日. 2015年5月10日閲覧。https://tlaplus.codeplex.com/license
4. Newcombe, Chris; Rath, Tim; Zhang, Fan; Munteanu, Bogdan; Brooker, Marc; Deardeuff, Michael (2014年9月29日). 「Amazon Web Servicesにおける形式手法の活用」(PDF) . Amazon . 2015年5月8日閲覧。
5. ランポート、レスリー（2013年1月25日）「なぜ私たちは家を建てるようにソフトウェアを作るべきなのか」 Wired誌。 2015年5月7日閲覧。
6. ランポート、レスリー（2002年6月18日）「7.1 なぜ仕様を定めるのか」『システムの仕様策定：ハードウェアおよびソフトウェアエンジニアのためのTLA ⁺言語とツール』アディソン・ウェズリー社、p.75、ISBN 978-0-321-14306-8設計を正確に記述しなければならない場合、見落としがちな微妙な相互作用や「コーナーケース」などの問題が明らかになることがよくあります。
7. ランポート、レスリー(2012). 「21世紀の証明の書き方」(PDF) . Journal of Fixed Point Theory and Applications . 11 : 43–63 . doi : 10.1007/s11784-012-0071-6 . ISSN 1661-7738 . S2CID 121557270. 2015年5月23日閲覧.  
8. Øhrstrøm, Peter; Hasle, Per (1995). 「3.7 時相論理とコンピュータサイエンス」時相論理：古代思想から人工知能へ言語学・哲学研究 第57巻シュプリンガー・オランダpp.  344– 365. doi : 10.1007/978-0-585-37463-5 . ISBN 978-0-7923-3586-3。
9. ランポート、レスリー. 「レスリー・ランポートの著作：マルチプロセスプログラムの正しさの証明」 . 2015年5月22日閲覧。
10. ランポート、レスリー. 「レスリー・ランポートの著作：オンザフライ・ガベージコレクション：協力の実践」 . 2015年5月22日閲覧。
11. ランポート、レスリー。「レスリー・ランポートの著作：「いつか」は「決してない」ではないこともある. 2015年5月22日閲覧。
12. Lamport, Leslie . 「The Writings of Leslie Lamport: Specifying Concurrent Programming Modules」 . 2015年5月22日閲覧。
13. ランポート、レスリー. 「レスリー・ランポートの著作：行為の時間的論理」 . 2015年5月22日閲覧。
14. Yu, Yuan; Manolios, Panagiotis; Lamport, Leslie (1999). 「モデル検査TLA ⁺仕様」.正しいハードウェア設計と検証手法(PDF) . コンピュータサイエンス講義ノート. 第1703巻. Springer-Verlag . pp.  54– 66. doi : 10.1007/3-540-48153-2_6 . ISBN 978-3-540-66559-5. 2015年5月14日閲覧。
15. ランポート、レスリー（2002年6月18日） 『システムの仕様定義：ハードウェアおよびソフトウェアエンジニアのためのTLA ⁺言語とツール』アディソン・ウェズリー社、ISBN 978-0-321-14306-8。
16. ランポート、レスリー(2009年1月2日). 「PlusCalアルゴリズム言語」(PDF) .コンピューティングの理論的側面 - ICTAC 2009.コンピュータサイエンス講義ノート. 第5684巻.シュプリンガー・ベルリン・ハイデルベルク. pp.  36– 60. doi : 10.1007/978-3-642-03466-4_2 . ISBN 978-3-642-03465-7. 2015年5月10日閲覧。
17. クズノー、ドゥニ;ダミアン・ドリゲス。レスリー・ランポート;メルツ、ステファン。リケッツ、ダニエル。ヴァンゼット、エルナン（2012 年 1 月 1 日） 「TLA ⁺証明」。FM 2012: 形式的手法(PDF)。コンピューターサイエンスの講義ノート。 Vol. 7436.シュプリンガー ベルリン ハイデルベルク。 pp.  147–154。土井: 10.1007/978-3-642-32759-9_14。ISBN 978-3-642-32758-2. S2CID  5243433 . 2015年5月14日閲覧。
18. ランポート、レスリー（2002年6月18日）「8.9.2 マシンクロージャ」『システムの仕様定義：ハードウェアおよびソフトウェアエンジニアのためのTLA ⁺言語とツール』アディソン・ウェズリー社、112ページ。ISBN 978-0-321-14306-8機械に閉じていない仕様を書きたいと思うことは滅多にありません。もし書いてしまうとしたら、それはたいてい間違いです。
19. ランポート、レスリー（2002年6月18日）「8.9.6 時相論理の混乱」 『システムの仕様策定：ハードウェア・ソフトウェアエンジニアのためのTLA ⁺言語とツール』アディソン・ウェズリー社、116ページ。ISBN 978-0-321-14306-8実際、[ほとんどのエンジニア]は、安全性の特性のみを表現し、変数を隠さない形式(8.38)の仕様で問題なく対応できます。
20. Markus A. Kuppe (2014年6月3日). Distributed TLC (技術講演の録音). TLA ⁺ Community Event 2014, トゥールーズ, フランス.{{cite AV media}}: CS1 メンテナンス: 場所 (リンク)
21. 「サポートされていないTLAPS機能」 . TLA ⁺ Proof System . Microsoft Research - INRIA Joint Centre . 2015年5月14日閲覧。
22. Koutanov, Emil (2021年7月12日). 「Spire: 分散型コンセンサスのための協調的かつ位相対称なソリューション」 . IEEE Access . 9. IEEE : 101702–101717 . Bibcode : 2021IEEEA...9j1702K . doi : 10.1109/ACCESS.2021.3096326 . S2CID 236480167 . 
23. TLA ⁺証明システム
24. Leslie Lamport (2014年4月3日). Thinking for Programmers (21分46秒あたり) (技術講演の録音). サンフランシスコ: Microsoft . 2015年5月14日閲覧。
25. Chris, Newcombe (2014). 「AmazonがTLA ⁺を選んだ理由」.抽象ステートマシン、Alloy、B、TLA、VDM、Z . コンピュータサイエンス講義ノート. 第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 (2017年5月10日). 「MicrosoftはCosmos DBで、すべてを統括する単一のデータベースの構築を目指している」 . TechCrunch . 2017年5月10日閲覧。
27. Leslie Lamport (2017年5月10日). 「Azure Cosmos DBの基礎：Leslie Lamport博士による」（インタビューの録音）. Microsoft Azure . 2017年5月10日閲覧。

「 https://en.wikipedia.org/w/index.php?title=TLA%2B&oldid=1333814310」より取得