AWSにおける形式手法 - masateruk’s blog

AWSにおける形式手法の記事（https://lamport.azurewebsites.net/tla/formal-methods-amazon.pdf）を読んだ。特に重要だと思われる示唆を3つあげると以下の通り。 産業界では長年形式手法は多大な工数をかけて比較的容易なコードの断片を検証するというイメージがあったが、これはまったくの誤り。現実の問題に適用可能である アマゾンでは10の現実のシステムに適用して、すべてで効果が得られた。難解なバグの発見したり、正当性を犠牲にすることなく確信を持って最適化を施せた 7つのチームでTLA+を使用。エンジニアは2−3週間で学習することができる 以下は、読んでいる途中で書きだした要点。 AWSでは2011年以降形式仕様とモデル検査を使用している 複雑な分散システムを検証するにあたって、従来の手法 ― 設計レビュー、コードレビュー、静的解析、ストレス

[yugui]

"「検証した設計から実行可能な正しいコードはどうやって得るのか？」と。答えは「得られない」だ。しかし、形式手法はいくつもの方法で助けてくれる。"

[lanius]

TLA+。

[masterq]

"検証は数学を使って推論してもいいし、モデル検査で検査してもいい"/"最初はAlloyを検討したが、自分たちのユースケースでは表現力が不足しているとしてTLA+を採用するに至る"

[taqpan]

https://en.wikipedia.org/wiki/TLA%2B

[moccos_info]

"エンジニアの先入観をさけるため、「形式」「検証」「証明」という用語は避けた"

[tmatsuu]

寡聞にして知らなかったのでちょっと調べてみる。TLA+とPlusCalか。

[Nnwww]

レビュー、静的解析、フォルトインジェクションをすり抜けるバグに対処し、設計をデバッグするという思想を2014年に実践済みなの最高過ぎない？

[karia]

“エンジニアの先入観をさけるため、「形式」「検証」「証明」という用語は避けた”

[yarumato]

“AWSは2011年以降、形式仕様TLA+を使用して難解な不具合発見したり確信を持って最適化。複雑な分散システム検証には従来のテストは不十分。検証した設計からコードは得られないが設計の網羅的理解を得る。3週で学習可”

[Nyoho]

形式手法

[mather314]

形式手法はずっとやってみたいと思ってる（本を買っただけ）

[kompiro]

https://masateruk.hatenablog.com/entry/2018/10/23/094048

[kenichiice]

TLA+

[ofsilvers]

おもしろい

[karahiyo]

“AWSでは2011年以降形式仕様とモデル検査を使用している ”

[benok]

興味深い

[mooz]

cool. 分散システムは形式手法と相性が良さそう。

[Dai_Kamijo]

AWSにおける形式手法 - masateruk’s blog — TAKAHASHI Kunihiko (@kunit) October 25, 2018 from Twitter https://twitter.com/Dai_Kamijo October 25, 2018 at 10:11AM via IFTTT

[otakumesi]

ミッションクリティカルなシステムで一つの失敗が多額の損失に繋がる場合には有効って感じなんですかね

[showyou]

TLA+

[yo_waka]

ほー...

[gfx]

うおっ…まじか…。

[igrep]

“TLA+ではシステムが持つべき特性と設計を同じ言語でかける。あらゆる抽象度で記述できて、検証は数学を使って推論してもいいし、モデル検査で検査してもいい”

[teppeis]

まじか

[rjj]

あわせて読みたい：あるソフトウェア工学者の失敗 日本のITは何故弱いか http://www.shayashi.jp/myfailures.pdf 「形式的検証の現実への適用例…良い応用例はあるが、労力がかかりすぎて適用して意味がある範囲があまりに狭い」

[y_uuki]

おもしろい

[el-condor]

興味深い。

[matsumoto_r]

面白い

[diizuka]

きになる

[t10471]

Alloyじゃないのかー。普通のwebサービスとかアプリでも有効なのかな？https://tnanjo.net/tla-plus-getting-started/