紹介担当： 石尾 隆（大阪大学） Q11.  Feature Model によって定義される「プロダクトの集合」 （プロダクトライン）の振舞いを検証する手法の拡張 ◦ 通常の振舞い検証： たとえば Promela を使って，１プロダクトの 振舞いを表現したオートマトンの取りうる状態遷移を調べる ◦

Presentation on theme: "紹介担当： 石尾 隆（大阪大学） Q11.  Feature Model によって定義される「プロダクトの集合」 （プロダクトライン）の振舞いを検証する手法の拡張 ◦ 通常の振舞い検証： たとえば Promela を使って，１プロダクトの 振舞いを表現したオートマトンの取りうる状態遷移を調べる ◦"— Presentation transcript:

1 紹介担当： 石尾 隆（大阪大学） Q11

2  Feature Model によって定義される「プロダクトの集合」 （プロダクトライン）の振舞いを検証する手法の拡張 ◦ 通常の振舞い検証： たとえば Promela を使って，１プロダクトの 振舞いを表現したオートマトンの取りうる状態遷移を調べる ◦ 著者らの既存研究： 「特定の feature 条件を満たすプロダクトだ けに許される状態遷移」を使って，プロダクトの集合の振舞いモ デルを１オートマトンで表現可能とした [7][8][9]  例： ネットワーク接続 Feature を持つ製品のみ接続待ち状態に遷移可能  個別製品ごとに構築 → 検証を繰り返すよりも効率的 ◦ この論文： 扱える Feature Model 自体を拡張し，それに合わせ て振舞いモデルの検証環境も拡張した Q12

3  Multi-feature に対応 ◦ 従来の Feature Model では， feature は「ある」か「ない」かの二択 ◦ Multi-feature は， 1 つの feature の複数のインスタンスを許す  例： 宇宙船との通信機能において，異なる通信能力を持つ宇宙船ごとに個別の 「受信バッファ」などを持てる  feature の複数のインスタンスを， f1[0].f2[1] のように配列として取り扱う  各 feature に boolean, int の属性を持つことを許す ◦ Feature インスタンスごとの情報を表現できる  例： バッファサイズなど  これら導入の必要性は，過去の調査 [15] による ◦ Multi-feature に対応しているのはこれまで heavyweight な手法のみだっ た ◦ 既存研究では semantics に曖昧なところがあったので，性質をきちんと定 義 Q13

4  feature の特定のインスタンスに対してプロセスを 関連付けて実行できるように， fPromela を拡張 ◦ 整数の属性の制約に関しては SMT Solver で対応 ◦ 計算を簡略化するため， 数値の大小関係を boolean 変数 に変換して SAT のレベルで解く方式も実装している  例： x 4) に置き換え， (x > 4) に 1 つの boolean 変数を対応させる．（任意の制約が扱えるわけではな い）  Model Checker で Multi-feature に対応したのは初めて Q14

5  論理展開が丁寧で読みやすい ◦ プロダクトライン， Feature Model の基礎知識だけで読め る ◦ Multi-feature をしっかり定義．形式的に書かれている性 質の多くは，直観的なもの  Feature Model については例を含めて詳しい  Feature の階層については，論文では (f1, 0)(f2, 1) と表現した り， Feature c の子要素として (c, m, i) と表現したりするので， 読むときは表現を確認しながら読むと良い  振舞い検証そのものの具体例はない ◦ 検証の性能的な評価のみ Q15

6 紹介担当：神田 哲也（大阪大学） Q21

7  Product Line の検証アプローチが提唱されている ◦ Product-based  全プロダクトを総当りで検証 ◦ Sample-based  いくつかの機能の組み合わせに限るなどして効率化 ◦ Family-Based  プロダクトライン全体をワンパスで処理  product-based と sample-based ・ family- based の比較は行われている ◦ sample-based と family-based の比較はまだ  アプローチの長短を同じ土俵で評価しよう ◦ SPL VERIFIER モデル検査 ツールチェインを作成 Q22

8  Product-based ◦ 全プロダクトを総当りで検証  Sample-based ◦ 検証するプロダクトを限定して効率化を図る ◦ pair-wise: 全機能から 2 つの機能を抜き出した組 {f1,f2}{f1,f3}... に対し、その機能を持つプロダクトを選択して検証 ◦ single-wise （ひとつ）, triple-wise （みっつ）  Family-Based ◦ プロダクトライン全体をワンパスで処理 (Fig.4 も参照 ) ◦ 挙動が異なる部分だけ分岐して検証 ◦ Late splitting & Early joining  共通度が高いほど、分岐して検証する部分を減らせる Q23

9  くらべかた ◦ Detection rate  検出された欠陥プロダクト数 / 全体の欠陥プロダクト数 ◦ Time fraction  検証時間 /product-based( 総あたり ) での検証時間 ◦ Detection efficiency  detection rate / time fraction  結果 ◦ Sample-based がうまくいくかは欠陥とサンプル量にかかってい る  時間は劇的に早くなるけど、見逃しも増える ◦ Family-based がうまくいくかはプロダクト間の類似度にかかっ ている  late-splitting と early-joining が有効に働くか ◦ pair-wise より triple-wise ◦ sample-based より family-based Q24

10  それぞれのアプローチの説明が簡潔でわかりやす かった  sample-based と family-based の比較、という モチベーションだがそれぞれの特徴についても丁 寧に評価していた  ツールや検査対象は既存研究でも使われているも の ◦ 関連研究へのポインタとしても丁度よいと思います Q25