先日、毎年恒例のなごや LT 大会 NGK2015B / 名古屋合同懇親会 2015 忘年会 で発表してきました。
www.slideshare.net
当日の動画は [3] NGK2015B（名古屋合同懇親会 2015 忘年会） - YouTube から見ることができます。
TL;DR
- AWS でインフラ運用中
- でも設定が
大人の都合でカオスになりがちだったりして辛い - よろしい、ならば形式手法だ
サンプルコードを動かしてみよう！
まずはインストールしてみる
公式ページ Alloy - download から、jar ファイルで提供されているものをダウンロードしましょう。
java -jar alloy4.2.jar
でウィンドウが起動すれば OK です。
なお、dmg 版も提供されていますが、Mac の人は（少なくとも現状）これをインストールしてはいけません。"Requires Java 6" と宣言している通り、内部のソルバ部分の実装が古い Java ランタイムに依存しているようで、Java 8 では起動できません。ちなみに現在 id:osiire さんが修正版を fork しています。
早速、検査してみる
今回の LT で使用したサンプルコードが Alloy による AWS セキュリティグループのモデリング · GitHub にあるので、手元にダウンロードして Alloy で開いてみましょう。
そしておもむろに Execute をクリック（または command + E）で
条件に合う設定が自動で探索されるはず。おめでとうございます。これであなたも立派な Alloy エンジニア！
ちょっと条件を変えてみる
Next を押すと、条件に合致する例が次々と表示されるのがわかると思います。しかし数が多すぎるし、各々の違いが解りにくいですね？
探索させる条件である run に対して、それぞれの要素（Alloy では atom と呼びます）の個数を制限することができます。以下のように変更して再度実行してみましょう。
run {
some disj i1, i2 : Instance, proto : Protocol, port : Port
| inboundOK[i1, i2, proto, port] &&
outboundOK[i1, i2, proto, port]
} for 2 Instance, 2 IP, 1 CIDR, 1 SecurityGroup, 2 Rule, 1 Port
ちょっとだけ図がすっきりしました。ちなみに、上記を 1 Rule にすると探索が失敗することも確認してみましょう。インスタンス間の通信が成立するためにはインバウンドルールとアウトバウンドルールが少なくとも 1 つずつ必要ですからね。
さて、セキュリティグループのルールに直接 CIDR を指定すると、何のサーバなのかわからないし、後々管理が辛くなりそうですね？「すべてのルールについて、source / destination は（CIDR ではなく）セキュリティグループ名で指定する」という制約を加えるには以下のようにすれば OK。
run {
some disj i1, i2 : Instance, proto : Protocol, port : Port
| inboundOK[i1, i2, proto, port] &&
outboundOK[i1, i2, proto, port]
Rule.(source + destination) in SecurityGroup
}
他にも思いつく制約をいろいろ試してみましょう。
そしてその先へ……
さて、Alloy を少し触ってみてちょっと面白そうだと思ったあなたに、第一にお勧めしたいのがこちら。
Alloy の背景にある関係モデルも含めてしっかり解説されており、密度の高い良書です。サンプルや練習問題も trivial なものから歯ごたえのあるものまで幅広く掲載されており、これを完全にフォローすれば Alloy を使う上でもはや不足はないと言ってよいでしょう。
また、書名に Alloy は入っていないのですが、こちらの書籍も面白いと思います。
Alloy そのものというよりは、実際の仕様や開発ライフサイクルに対してどのように形式手法が関わるのかについて焦点を当てた、より実務者向けの参考書です。
ところで自分はといえば、
例の Alloy 本はとてもよい教科書だと思うのだけれど、如何せん敷居が高い。いつかあのエッセンスを抽出したもっとフレンドリなチュートリアルを書きたい。
— チェシャ猫 (@y_taka_23) 2015, 10月 5みたいな野望があったりなかったりするのですが、それはまた別の話。
