OAuth2 のフローを Alloy Analyzer でモデリングする - 詩と創作・思索のひろば
趣味でウェブの認証 API を地力で設計しようとしていたときに、認証フローの仕様を頑張ってこしらえたとして、その正しさをどうやって保証するんだろう？ と疑問に思い、調べていたところ、「形式手法」というのに行き当たった。 形式手法というのはシステムの正しさを上流工程から検証するための方法で、数理論理やロジックに基づいている。その中でも厳密な仕様定義を求める方向と自動検証を求める方向とあるらしいが、Alloy はその後者に位置づけられ、軽量形式手法と呼ばれるもののひとつだということらしい。Alloy はモデリングのための言語および実行環境で、以下のホームページから入手できる。 http://alloy.mit.edu/alloy/ インターネット上にチュートリアルやマニュアルもあるが、作者による教科書の邦訳が出ていて、これで勉強してみた。 抽象によるソフトウェア設計−Alloyではじめる形式手
みずほ情報総研 ： 高品質で効率的なシステム開発
ソフトウェアシステムは人々の生活を支える重大な役割を持つようになっている。万一不具合がおきた場合、人々の安全に重大な影響を及ぼすシステムの安全性の保証について気になる方もいるだろう。また、たとえば無人運転路線の運行システムにはどのような安全設計がなされているのか、という疑問を浮かべる人もいるかも知れない。 1998年に開業したパリメトロ14号線は、無人運転でパリ市内を北西から南東に横切る路線である。パリメトロで最も新しい路線であり、他の路線と比べてホーム・車内ともにきれいなこの路線の運行システムは、Bメソッドという「形式手法」を用いて開発されている。Bメソッドを用いて開発されたシステムは、開発の上流工程において誤りが混入しないことを数学的に証明でき、開発の下流工程であるテスト工程および実運用において不具合がゼロという高い品質をもつ安全なシステムの構築が可能となる。パリメトロ14号線の運行シ
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
AWS は形式手法の夢を見るか？ - モデル検査器 Alloy によるインフラ設計
