F1 Aluminum: Principled Scenario Exploration through Minimality by Tim Nelson, Salman Saghafi, Daniel J. Dougherty, Kathi Fisler, Shriram Krishnamurthi @ ICSE 2013 酒井 政裕 2013-07-09 ICSE2013 勉強会 The background image is from http://images-of-elements.com/. The image is licensed under a Creative Commons Attribution 3.0 Unported License. 背景 F1 • 背景 – 高レベルの仕様記述に対して「シナリオ」(=具体例)を 探索・生成するAlloyなどのツール – シナリオの利点 • システム設計者が、その設計の帰結、見落としていた制約、 代替的なデザインなどを検討するのを助ける • 具体的なので分かりやすく、現実に対応させやすい。 • 論理学等に詳しくない、ドメインの専門家にも理解可能 • 課題 – 複数あるシナリオから、どんなシナリオをどんな順で 提示するべきか? – 小さいシナリオはしばしば病的で、微妙な問題を明ら かにすることが多い – ⇒ 小さいシナリオから提示するように出来ないか? Alloyの例 abstract sig Subject {} sig Student extends Subject {} sig Professor extends Subject {} sig Class { TAs: set Student, instructor: one Professor } sig Assignment { forClass: one Class, submittedBy: some Student } pred PolicyAllowsGrading(s: Subject, a: Assignment) { s in a.forClass.TAs or s in a.forClass.instructor } pred WhoCanGradeAssignments() { some s : Subject | some a: Assignment | PolicyAllowsGrading[s, a] } run WhoCanGradeAssignments for 3 F1 コードと図は Aluminum: Principled Scenario Exploration through Minimality (by Tim Nelson, Salman Saghafi, Daniel J. Dougherty, Kathi Fisler, Shriram Krishnamurthi) より抜粋 複数シナリオの列挙 F1 Next Next Next … 図は Aluminum: Principled Scenario Exploration through Minimality (by Tim Nelson, Salman Saghafi, Daniel J. Dougherty, Kathi Fisler, Shriram Krishnamurthi) より抜粋 Alloy を変更し Aluminum を実装 F1 機能 1. GenerateMin シナリオ探索の スタートポイント – 極小なシナリオの生成・列挙 (関係からタプルを一つでも取り 余計なものを含ま 除くと、制約を満たさなくなる) ない、シナリオの 2. Augment – シナリオを、関係にタプルを追 加することでユーザが拡張 3. ConsistentTuples – シナリオに対し、関係に追加可 能なタプルを計算 本質に注目! 対話的探索! 「制約を追加して 再探索」という コンテキストス イッチを減らす 列挙の比較 Alloy Next Next Aluminum Next Next 図は Aluminum: Principled Scenario Exploration through Minimality (by Tim Nelson, Salman Saghafi, Daniel J. Dougherty, Kathi Fisler, Shriram Krishnamurthi) より抜粋 F1 • アルゴリズムは素直 F1 – SATレベルでの制約の順次追加による極小化など – ただし、Symmetry-Breakingは極小化との相互作用の 問題から、Alloy(KodKod)と別のヒューリスティクス を採用 • 実験を通じた観察 – Alloyは特定の極小シナリオの上位のシナリオばかり を列挙し、それ以外を数百回以上も出さないことが 多い – それまでにユーザが探索をやめてしまい、重要・危 険なシナリオを見逃す危険性 – Aluminumはシナリオ空間の本質をユーザに早く見 せる • 性能への影響はあまりなし Counter Play-Out: Executing Unrealizable Scenario-Based Specifications Shahar Maoz School of Computer Science Tel Aviv University, Israel Yaniv Sa’ar Dept. of Computer Science Weizmann Institute of Science, Israel サーベイ担当: 遠藤侑介 背景: Play-out • シーケンス図からコントローラを合成する panel cashier panel の プログラム insertCoin() incCoins() 合成 cashier の プログラム 自動販売機のシーケンス図 • 問題点:デバッグがつらい – 合成器「充足不可能な制約があって合成できないよ」 – 設計者「えー。どこを直せと。合成器のバグじゃないの」 提案: Counter Play-out • 合成できない場合、代わりに「ユーザ」を合成する – 合成された「ユーザ」は意地悪: システムがどうしようと、 最終的に制約違反してしまうように振る舞う panel cashier 意地悪なユーザを シミュレートする プログラム insertCoin() incCoins() 合成 – 合成器「ならお前がシステムやれよ。俺がユーザやるから」 – 設計者「……なるほど実現できない。すみませんでした」 貢献の概要 • 「意地悪なユーザ」の合成方法 – アルゴリズム自体はコントローラの合成とほぼ同じ • BDD ベースの symbolic algorithm – 解く制約が反転している • 実際に実装し、試してみた – PlayGo: シナリオベース仕様の Eclipse IDE – 小規模~中規模な例を 15 個ほど作ってみた • 論文には自動販売機のみ(シーケンス図5つ) • 状態数や合成にかかる時間の簡単な評価はあり • ユーザスタディ(デバッグ時間とか)は言及なし F3. Unifying FSM-Inference Algorithms through Declarative Specification by Ivan Beschastnikh , Yuriy Brun , Jenny Abrahamson , Michael D. Ernst , and Arvind Krishnamurthy 担当:今井健男(T芝) 実行ログから状態遷移モデル(FSM) を推定したい ※ Fig. 2 実行ログから状態遷移モデル(FSM) を推定したい ※ Fig. 2 手続き的な推定アルゴリズム (大抵ハードコーディング) ※ Fig. 3 手続き的なアルゴリズムの弱点 わかりにくい 1. 出力FSMの特徴が読 み取れない いじりにくい 2. 「こんな遷移を出したい /消したい」 「2つのアルゴリズムを マージしたい」 比較すんのツラい 3. ※ Fig. 3 並べてもわからん FSMの性質を宣言的に書けば そのとおりのFSMが出てくるツールを こういうパターンを並べれば、お望 作りました みのFSMが出てくる わかりやすい 1. いじりやすい 2. ※ Fig. 13 追加・削除・マージ ≒ 宣言を足したり引いたり 比較しやすい 3. 4. 特徴がそのまま書いてある 並べて見比べればいい (おまけ) 性能もすんげく上がりま した F4. What Good Are Strong Specifications? by Nadia Polikarpova, Carlo A. Furia, Yu Pei, and Bertrand Meyer 担当:今井健男(T芝) 強い形式仕様 vs. お手軽形式仕様 (strong) ≒ complete みんないやがる 書くの大変 (lightweight) ≒ incomplete, partial みんなに人気 Design by Contract 実行可能な仕様だけ Test-Driven (DbC) Development (TDD) テストケース=形式仕様 強い仕様を書く価値はあるのか? をエンピリカルに分析・評価 (+「強い仕様/契約」の書き方の提案) 「線形リストの指定位置の後ろに、 別のリストを挿入」の事後条件 お手軽仕様(DbC) ※ Fig. 1 より抜粋 挿入後の要素数は 2リストの要素数の合計 指定位置は 挿入前後で同じ 強い仕様(Model-Based Contract, MBC) ※ Fig. 2 より抜粋 ただし sequence, front, tail, ‘+’ は別に与える 分析・評価してみた 21種のEiffelコードに対するDbCとMBCで比較 総テストケース8700万個、総テスト時間1680時間 (!)分のテスト生成、バグの見つかり方を比較 結果(の一部をざっくりと): MBCの方が、バグが2倍以上見つかった 記述量(仕様記述の行数/コード行数)もほぼ2倍程度 (103 vs. 48) (0.46 vs. 0.2) …労力に見合う効果はある
© Copyright 2024 ExpyDoc