Generating Obstacle Conditions for Requirements Completeness Dalal Alrajeh* Jeff Kramer* Axel van Lamsweerdey† Alessandra Russo* Sebastian Uchitel* *Department of Computing, Imperial College London, UK †ICTEAM institute, Universit´e catholique de Louvain, Belgium ICSE2012 勉強会 2012年8月30日 担当：早稲田大学 情報理工学研究科 鷲崎研究室 坂本 一憲
背景と貢献 要求の見落としは欠陥の主な原因の一つ ゴール指向分析では障害を考えてリスク分析 形式手法でゴールの否定形から障害を導ける 実現できないような理想的過ぎる要求を挙げがち リスク分析をすることで要求の見落としを防ぐ ゴール指向分析では障害を考えてリスク分析 障害：ゴールを満たせなくなるような事前条件 形式手法でゴールの否定形から障害を導ける リアルタイム線形時相論理の記述が困難 貢献内容 モデル検査と学習(ILP)による要求の完全化 既存研究よりも自動化した範囲が広い ツールによる障害生成の支援(ドメイン一貫/完全) 振る舞い モデルを対象 2019/10/15
Fluent Linear Temporal Logic (FLTL) Motivated Example Fluent Linear Temporal Logic (FLTL) 理想的過ぎる要求 (暗黙な要求が存在) ゴール：「停止信号が出たら電車が停まる」 StopSingal => ○TrainStopped ドメイン知識1：「電車が止まる直前は運転手が対応可能」 ○TrainStopped => DriverResponsive ドメイン知識2：「電車が止まる直前は信号機が見える」 ○TrainStopped => SingalVisible 障害1：「停止信号に運転手が対応できない」 ◇(StopSingal ∧ ○￢ DriverResponsive) 障害2：「停止信号が見えない」 ◇(StopSingal ∧ ○￢ SingalVisible) 障害の 洗い出し 障害の否定形が 見落とした要求 Generating Obstacle Conditions for Requirements Completeness, Dalal Alrajeh, Jeff Kramer, Axel van Lamsweerde, Alessandra Russo and Sebastian Uchitel: in Proceedings of 34th International Conference on Software Engineering (ICSE‘12) の 3ページ目から抜粋 2019/10/15
提案手法：障害生成の反復適用 2. ゴールを満た す／満たさない 反例を検出 1. ドメイン情報のモデル化 4. 障害から新しい要求 ・ドメイン情報を反映 3. 得られた反例 から障害を学習 Generating Obstacle Conditions for Requirements Completeness, Dalal Alrajeh, Jeff Kramer, Axel van Lamsweerde, Alessandra Russo and Sebastian Uchitel: in Proceedings of 34th International Conference on Software Engineering (ICSE‘12) の 4ページ目から抜粋 2019/10/15
評価：ケーススタディ London Ambulance Service (LAS)に適用 Bounded/Unbounded Achieve Goalの例 Achieve: If C then sooner-or-later T 以下でBounded Achieve Goalの例を抜粋 ゴール「直前が出動可能で救急車が動員すると，11分以内に治療開始」 2種類のドメイン知識と反例をILPで学習して障害生成 障害1「直前で出動可＆出動済み＆11分以内でサービス外」 障害2「直前で出動可＆出動済み＆11分以内で割当不可」 障害3「直前で出動可＆出動済み＆直後に出動済みでない」 手作業で形式的に得られた障害を全て検出(既存研究) 既存研究で検出できない障害も発見(実際の障害に近い) 2019/10/15