TLA+
Temporal Logic of Actions
https://lamport.azurewebsites.net/tla/tla.html
https://w.atwiki.jp/tlaplus/
動的なシステムの振る舞いを記述するための 形式仕様言語
並行システム や 分散システム の 時間的特性 が記述可能
競合状態 や デッドロック、ライブロック などを発見することが可能
特徴
時相論理: システムの時間的変化を数学的に記述できる
アクション指向: 状態変化を Actions として定義する
並行性 の明示的サポート: 複数 プロセス の相互作用を記述可能
活性・安全性の検証: 「悪いことは起こらない」「良いことはいずれ起こる」を証明
基本構文要素
Variables（変数）: システムの 状態
Constants（定数）: システムの パラメータ
Type Invariants（型不変条件）: 変数の型制約
Actions（アクション）: 状態の変化
時間と状態遷移
Initial State（初期状態）
State Transitions（状態遷移）
Next State Transitions（次遷移状態）
活性と安全性の検証
Safety Property（安全プロパティ）: 「悪いことは起こらない」
Liveness Property（活性プロパティ）: 「良いことは最終的に起きる」
Specification（仕様）: 全体の動作定義
TLC（TLA+ Model Checker）を使えば実行することが可能