ウィリアムのいたずらの、まちあるき、たべあるき

仕様の正しさを示す手法の一つとして、形式手法を利用する方法がある。
一般的にはその手法として、ＶＤＭ、Ｂ（Ｅｖｅｎｔ－Ｂ）、Ｚ、Ｃｏｑ、Ａｌｌｏｙとかの形式仕様記述言語を使って、数学的に確認する方法と、ＳＰＩＮ、UPPAALなどのモデルチェッキング（モデル検査：モデルを作ってしらみつぶしに調べる）方法がよくしれれている。

だけど、ＡｍａｚｏｎはＴＬＡ＋というのを使っているらしい。

・・・で、ＴＬＡ＋って何？。どこに分類されるもの？

と思ったら、酒匂さんが発表してたみたい

成功した形式手法導入調査例の分析と発見
https://www.ipa.go.jp/files/000005473.pdf

の７シート目
「論理アプローチ」
だそうな・・・ＲＴＬと一緒・・・ってよくわからん。ＲＴＬ知らん。

ということで、気を取り直して、
ＴＬＡ＋そのものがどうなっているんだろう
って調べてみると、これは熊澤さんが書いていた。

GSLetterNeo vol.130 2019 年 5 月
形式手法コトハジメ –TLA+ Toolbox を使って
https://www2.sra.co.jp/Portals/0/files/gsletter/pdf/GSLetterNeoVol130.pdf

ざっくり雰囲気はわかったけど・・・いまいちわからん・・・

やっぱＡｍａｚｏｎといえばＤｅｖｅｌｏｐｅｒｓ．ＩＯだよね。素直に見てみる。

[TLA+] TLA+と形式仕様言語 [目的と準備]
https://dev.classmethod.jp/articles/what-is-tlaplus/

TLA+が形式仕様記述で、これで記述したものをTLC Model Checkerでモデル検査できる。
・・・なるほど、わかった！
やっぱＡｍａｚｏｎといえばＤｅｖｅｌｏｐｅｒｓ．ＩＯだね！

Ｐ．Ｓ　これ調べれる間に、蓮尾 一郎が様相論理について、やさしく書いてあるものを見つけたんでＵＲＬをメモ。

モデル検査入門
http://www.kurims.kyoto-u.ac.jp/~cs/lecture2009/lecture09ModelChecking.pdf