読者です 読者をやめる 読者になる 読者になる

チェシャ猫の消滅定理

数学にプログラミング、素敵なもの何もかも。

JAWS FESTA 東海道 2016 で形式手法によるネットワーク設計について話してきました

先日行われた JAWS FESTA 東海道 2016 で登壇してきました。

www.slideshare.net

テーマは以前 AWS Summit で発表したものと同じですが、前回が 5 分の LT だったのに比べて今回は 25 分の枠を頂きました。そこで、形式手法を用いる動機を中心に据えた前回と比較して、以下のような実践的なトピックを充実させてあります。

  • Alloy を使うためにの最低限必要な言語機能を知る
  • シンプルな Web サーバ周りのネットワークについて、仕様から設計を導出する

ちなみに前回の AWS Summit 2016 での発表に関してはこちらから。

ccvanishing.hateblo.jp

寄せられた質問

発表後に頂いたいくつかコメントや質問について、ここで説明しておきます。

「全探索」と言っているが、無限の範囲を探索するのは不可能なのでは?

はい、その通りです。Alloy におけるシグネチャは有限集合でしかありえないので、探索はその範囲に限られます。例えば、

run fooPred for 5

とすると各シグネチャの要素数が 5 個以下の場合を探索します。デフォルトは 3 です。

とはいえ、資料中に登場する 3 個の要素を持つ 2 種類のシグネチャ間の関係だけを考えるケースでさえ、考えうる関係の数は 2 の 3 * 3 乗で 512 通りもあります。実用的なモデルを書こうと思えば場合の数は急激に増えていくため、人力でテストケースを組むことを考えれば Alloy も捨てたものではありません。

ちなみにこのような Alloy の設計思想は「もし仕様バグが存在するなら、それは比較的小さなモデルの時点ですでに問題になるはずだ」というアイデアで正当化されています。この考え方は 小スコープ仮説 (small scope hypothesis) と呼ばれています。

AWS リソースを自前でモデル化するのは辛そう。ライブラリ化の予定は?

できたら面白いとは思っていますが、現実的には厳しそうです。

これは、ライブラリを作成しようと思うと、必然的に個別事例では必要のない部分(例えばセキュリティグループのみ考えてネットワーク ACL は使わない、など)までモデルに含まれてしまうためです。Alloy のモデルは関係が必ず集合に結びつく形で定義されているため合成可能性に乏しく、必要な要素のみライブラリから取り出して使用することが困難なのです。

現時点では、個別にそのとき必要な部分を取捨選択してモデル化するのが妥協案だと思います。

Alloy を勉強しようと思ったら何から始めるのがいい?

毎回名前を挙げていますが、以下の書籍がおすすめです。初見だと多少記述がとっつきづらく感じるかもしれませんが、実際に Alloy を動かしつつ読むと理解が深まるでしょう。なおこの本の内容を把握したら後は慣れの問題です。

estore.ohmsha.co.jp

おわりに

今回の発表、実は当初はここまで Alloy に特化せず、参照した論文中で述べられている AWS 内での取り組みをもう少し前面に出そうかと思っていました。スライドの途中で TLA+ の名前が出てくるのは名残です。

ただ TLA+ は完全にオートマトン型の典型的なモデル検査器であり、AWS使う側 とは相性があまり良くなかったため、具体的な内容は結局すべて外してしまいました。その分 Alloy についてはこの発表を聞いた人がとりあえず触ってみる程度のことは説明できたので、まあ結果オーライかなとは思います。

ところで、今年もまた名古屋のコミュニティ合同忘年会 NGK2016B がありますね? 自分はここ数年連続して色々なモデル検査ツールの発表をしているのですが、それはまた別の話。