TLA+ 関連リンク集

#verification

Info

順次, 書き足していく

Learning TLA+

公式ページにあるリンク集.

https://lamport.azurewebsites.net/tla/learning.html

Examples

Paxos, Raft, MongoDB なども紹介されてる. TLA+ 力のステップアップになりそう.

https://github.com/tlaplus/Examples

Learn TLA+ (Web Book)

https://learntla.com/introduction/

PlusCal Manual

TLA+ 言語と違って, 普通のプログラミング言語みたいに書ける PlusCal というのがある. それには C-version と P-version があって, お好みで.

• https://lamport.azurewebsites.net/tla/p-manual.pdf
• https://lamport.azurewebsites.net/tla/c-manual.pdf

Specifying Systems

Lamport 本人が書いた入門書で, 360 頁くらい.

https://lamport.azurewebsites.net/tla/book.html

Safety, Liveness, and Fairness

• stuttering insensitive について
• WF, SF Oprators について

など.

https://lamport.azurewebsites.net/tla/safety-liveness.pdf

いつか読む

• Real-Time Model Checking is Really Simple
• A Formal Analysis of the Web Services Atomic Transaction Protocol with UPPAAL
• Specifying time-sensitive systems with TLA+

---

Posted: 2020-07-28
Last update: 2021-03-02