ウィリアムのいたずらの開発?日記

ウィリアムのいたずらがコンピューター関係(本家廃止後はその他も)について思ったことを好き勝手に書いているブログです。

AmazonがTLA+っていう形式手法を使っていることはわかったけど・・・TLA+って何者?

2020-05-22 08:47:52 | Weblog
仕様の正しさを示す手法の一つとして、形式手法を利用する方法がある。
一般的にはその手法として、VDM、B(Event-B)、Z、Coq、Alloyとかの形式仕様記述言語を使って、数学的に確認する方法と、SPIN、UPPAALなどのモデルチェッキング(モデル検査:モデルを作ってしらみつぶしに調べる)方法がよくしれれている。

だけど、AmazonはTLA+というのを使っているらしい。

・・・で、TLA+って何?。どこに分類されるもの?

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

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


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

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

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


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

やっぱAmazonといえばDevelopers.IOだよね。素直に見てみる。

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


TLA+が形式仕様記述で、これで記述したものをTLC Model Checkerでモデル検査できる。
・・・なるほど、わかった!
やっぱAmazonといえばDevelopers.IOだね!

P.S これ調べれる間に、蓮尾 一郎が様相論理について、やさしく書いてあるものを見つけたんでURLをメモ。

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

この記事についてブログを書く
« 文春砲、炸裂ですね!でも、... | トップ | 世界初のコロナ文学 »
最新の画像もっと見る

Weblog」カテゴリの最新記事