![Alloyによるモデル化
操作定義と権限チェックの実施
//オペレーション定義
abstract sig Operation {}
sig Create extends Operation { target : Path } //新規作成
sig Copy extends Operation { disj src, dst : Path } //コピー
sig Delete extends Operation { target : Path } //削除
sig Chmod extends Operation { target : Path, perm : Permission } //権限変更
//抜粋
else #(Chmod & x.command) > 0 => {
let c = (x.command <: Chmod), s = x.state {
exists[s, c.target]
getElem[s, c.target].chmodable //変更権限があるか？
}
}](https://image.slidesharecdn.com/alloyanalyzer-141001064927-phpapp01/85/Alloy-analyzer-32-320.jpg)
![検証したい性質の記述
権限変更フラグが立っていないファイルをどう操作しても、
pred PermissionConsistency {
some x : StateTrans | some y : x.^next | some p : sameFiles[x.state, y.state] |
let xe = getElem[x.state, p], ye = getElem[y.state, p] |
xe.contents = ye.contents and
xe.permission.perm = none and // 権限変更できないはずなのに
ye.permission.perm = P // できたりしないよね？
}
権限変更フラグを立てた状態にはできない。
（フラグを立てた状態に至るパスを見つけろ）](https://image.slidesharecdn.com/alloyanalyzer-141001064927-phpapp01/85/Alloy-analyzer-33-320.jpg)
Alloy analyzer
- 1. Alloy Analyzerで 簡単設計チェック 2011年8月8日 有限会社ITプランニング 小笠原啓
- 2. ? Alloy Analyzerのご紹介 ? Alloyって何ができるの？ ? データモデリング ? ビジネスの仕組みの記述 ? 手続きの検証 ? まとめ アジェンダ
- 4. Alloy Analyzerとは ? Alloy AnalyzerはMITで開発されたオープンソース （MITライセンス）のJava製GUI付き仕様記述?検 証ツール。 ? B, Z, VDMのようなツールは仲間。 ? 2006年頃から公開されており、Version 4で解析速 度向上、文法のブラッシュアップ。 ? 2011年8月現在Version 4.1.10が最新(4.2 RCあり)。 開発者のDaniel Jackson@MIT
- 5. Alloy Analyzerの検証は全自動 ? 簡素な言語で仕様を記述すると、その仕様を満た す状態を検索して図示してくれる（モデルファイ ンダー）。 ? 検証したい性質を記述すると、その性質が満たさ れるかどうか全自動でチェックしてくれる。
- 6. 小スコープ仮説 ? 全自動チェックにはスコープ（チェックする範 囲）があり有限。それでも多くの設計がチェック できる。（小スコープ仮説） 探索空間とAlloyのスコープ（イメージ）
- 9. V字モデル 要求分析 システム設計 詳細設計 モジュール実装 高効率?高信頼なソフトウェア開発のための関数プログラミングと形 式手法10 受け入れテスト システムテスト 結合テスト 単体テスト このフェーズで嬉しい
- 10. 例えば、データモデリング ? データ構造を表現して、その制約条件などを記述 する。贰搁図を作成する工程。
- 12. １対ｎの関係
- 13. Alloyではこう書けます sig Company, Person {} // 企業と従業員 one sig Employ { employee : Company -> set Person // 雇用関係 }
- 16. サンプル図を続けて見ている と??? 副業規定 违反！？
- 17. モデルの修正 sig Company, Person {} // 企業と従業員 one sig Employ { employee : Company lone -> set Person// 雇用関係 } 一人の人が複数の企業に雇われないように。従業員は０人以上。
- 18. １対ｎの関係のバリエーション sig Company, Person {} // 企業と従業員 one sig Employ { // 雇用関係 employee : Company lone -> set Person } lone(０か１） one（１のみ） set（０以上） some（１以上）
- 19. サンプル図でチェック！ ? 一口に１対ｎの関係といっても、厳密にはいくつ かの種類が考えられる。ｎ対ｎはもっと種類が多 い。 ? 複雑なデータを扱うときは、しっかりとモデリン グしておかないと、後工程での手戻りが高コスト となる。 ? Alloyを使ってモデルを記述すると、意図したモデ リングができているかどうか、サンプル図を見な がらチェックできる。 ? 完成したAlloyコードとサンプル図を設計書に張っ ておくと効果的。
- 20. 正確性向上！ レビュー時間短縮！
- 22. ケーススタディ 陶器のカタログ販売 ? 陶器の窯元さんは自社で陶器を制作している。 ? ただ、個別に売っていては効率が良くないので、 窯元さんが何社も集まって、一つの陶器カタログ を作る。 ? そのカタログをホテルや外食産業に配布して、カ タログを見て注文してもらう。受注は、カタログ に参加している窯元さんがそれぞれ受ける。 ? 窯元さんは受注を受けた時に、自社製品以外の注 文は、カタログ参加窯元に仕入発注を出して対応 する。
- 23. 陶器のカタログ販売 カタログ 注文 注文
- 24. 础濒濒辞测で书くとこうなります
- 25. サンプル図
- 26. 仕様を記述する過程で 疑問に思った事 ? 窯元さんの製品は必ず一社オリジナル？同じ製品 を二社以上が作っていることは無い？ sig Maker { products: disj set Product // 自社製品 } ? カタログに載せる製品は参加窯元さんの全ての製 品？それとも一部だけ？ // 商品はカタログ参加企業の商品 products in member.products
- 27. 仕様記述で 仕様の穴を早期に見つける ? シンプルな仕様だと思っていても、書き下してみ ると意外と曖昧さが残っている。 ? Alloyで仕様を記述する事で、簡単に曖昧性が浮き 彫りになる。 ? プログラムを書くわけではないので、実装の詳細 には縛られずに、仕様だけを表現できる。
- 28. 仕様バグとはもう言わせない！
- 29. 手続きの検証例 ファイルシステムの権限 ? 読み込み権限があるファイルのみ読み込み可能、 書き込み権限があるファイルのみ書き込み可能と する簡易ファイルシステムを考えてみる。 ? 権限を勝手に変えられると元も子もないので、権 限変更フラグも用意する。権限変更フラグがある ファイルの権限のみ、読み込み?書き込み権限を 含めて、変更できる。
- 30. 簡易ファイルシステム 権限のイメージ foo/ 256 12:23:22 rwp bar 421 12:20:01 r-- aaa 482 12:39:39 rw- ?全権限 ?読み込みのみ ?読み書き
- 31. Alloyによるモデル化 ? 木構造のファイルシステムと４つの操作（新規作 成、コピー、削除、権限変更）をモデル化。 ? 各操作を実行する前に権限をチェック。 abstract sig Elem { // 全てのファイルシステムエレメントには権限が設定されている。 permission : Permission } sig File extends Elem { contents : Contents // ファイルには内容がある。 } sig Dir extends Elem {} // ディレクトリ。子要素は別途定義する。
- 32. Alloyによるモデル化 操作定義と権限チェックの実施 //オペレーション定義 abstract sig Operation {} sig Create extends Operation { target : Path } //新規作成 sig Copy extends Operation { disj src, dst : Path } //コピー sig Delete extends Operation { target : Path } //削除 sig Chmod extends Operation { target : Path, perm : Permission } //権限変更 //抜粋 else #(Chmod & x.command) > 0 => { let c = (x.command <: Chmod), s = x.state { exists[s, c.target] getElem[s, c.target].chmodable //変更権限があるか？ } }
- 33. 検証したい性質の記述 権限変更フラグが立っていないファイルをどう操作しても、 pred PermissionConsistency { some x : StateTrans | some y : x.^next | some p : sameFiles[x.state, y.state] | let xe = getElem[x.state, p], ye = getElem[y.state, p] | xe.contents = ye.contents and xe.permission.perm = none and // 権限変更できないはずなのに ye.permission.perm = P // できたりしないよね？ } 権限変更フラグを立てた状態にはできない。 （フラグを立てた状態に至るパスを見つけろ）
- 34. デモ：性质の検証
- 35. 手続きの検証 ? 少し複雑な組合せ問題になると、人間はすぐに見 落としをしてしまう。 ? Alloyは網羅的にチェックしてくれるので、人間が 見落としがちなケースもカバーしてくれる。 ? 記述に慣れてくれば、比較的短時間にモデルを構 築できる。 ? アルゴリズムが少し変更になったとき、Alloyのモ デルがあれば簡単に回帰チェックができる。
- 37. 手続きのモデル化と検証 その他の例 ? ホテルの客室施錠問題。 ? DNSのモデル化と検証。 ? バージョン管理システムのモデル化と検証。 ? メモリキャッシュ戦略のモデル化と検証。 ? コミットプロトコルのモデル化と検証。 ? タスクのスケジューリング問題。 ? 数独、連立方程式、正直うそつきパズル。
- 38. まとめ ? Alloy AnalyzerはMITで作られたオープンソースの仕 様記述?検証ツール。 ? 決められたスコープ内での網羅的全自動チェック が可能。 ? 正確なデータモデリングの支援、仕様記述による 曖昧さの早期発見、複雑な手続きの検証など、使 い方次第で様々な利点が得られる。 ? 日本語の情報源も登場！応用を始めるには良い時 期。
- 42. 情報源（４）：書籍 抽象によるソフトウェア設計－Alloyではじめる形式手 法 Daniel Jackson (著), 中島震(監訳), 今井健男(翻訳), 酒井政裕(翻訳), 遠藤侑介(翻訳), 片岡欣夫(翻訳) オーム社
- 44. 设计に自动チェックの力を！
- 45. ご清聴ありがとうございました。