OAuth2 のフローを Alloy Analyzer でモデリングする - 詩と創作・思索のひろば
趣味でウェブの認証 API を地力で設計しようとしていたときに、認証フローの仕様を頑張ってこしらえたとして、その正しさをどうやって保証するんだろう？ と疑問に思い、調べていたところ、「形式手法」というのに行き当たった。 形式手法というのはシステムの正しさを上流工程から検証するための方法で、数理論理やロジックに基づいている。その中でも厳密な仕様定義を求める方向と自動検証を求める方向とあるらしいが、Alloy はその後者に位置づけられ、軽量形式手法と呼ばれるもののひとつだということらしい。Alloy はモデリングのための言語および実行環境で、以下のホームページから入手できる。 http://alloy.mit.edu/alloy/ インターネット上にチュートリアルやマニュアルもあるが、作者による教科書の邦訳が出ていて、これで勉強してみた。 抽象によるソフトウェア設計−Alloyではじめる形式手
AWS Summit Tokyo 2016 で形式手法について話してきました - チェシャ猫の消滅定理
先日行われた AWS Summit Tokyo 2016 で、形式手法のインフラ設計への応用について発表してきました。 形式手法で捗る！インフラ構成の設計と検証 from y_taka_23 www.slideshare.net モデル検査器 Alloy を利用して AWS の設定を検査する、という内容の LT で、昨年 12 月の NGK2015B でも同じテーマについて話しています。よければ以下の記事も合わせてお読みください。 ccvanishing.hateblo.jp NGK2015B の発表ではサンプルコードの紹介に比較的時間を割いているのに対して、今回の発表では「動機」の部分によりウェイトを置いた構成になっています。 なぜ形式手法なのか？ 今回のテーマを一言でまとめると以下のようになります。 インフラ構成が「秘伝のタレ」と化すのをどう防ぐべきか？ ある程度の規模のインフラを長期
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
