平成19年度トップエスイー修了制作ゴール指向要求分析を用いたモデル検査技術の適用プロセス株式会社日立製作所 [email protected] 小川秀人開発における問題点手法・ツールの適用による解決ソフトウェア品質向上策の１つとして，設計検証へのモデル検査技術適用が期待されているが，製品開発への実適用において，技術の難しさに起因する，以下が問題となっている． (1) 専用言語によるモデルや検証式の記述 (2) 検証項目の策定､検証項目の充分性 (3) 特定の人材への依存設計用モデルからの検証用モデルの自動生成を前提とし，ゴール指向要求分析技法KAOSを検証項目の策定に用いたプロセスを確立． (1) 検証プロセスの自動化 (2) 要求とのトレーサビリティを持つ検証項目をシステマティックに導出 (3) 特別なスキルに依存しない検証プロセスゴール指向要求分析による検査項目の導出プロセス要求分析者設計者 KAOS ｺﾞｰﾙﾂﾘｰ UML設計ツール Jude 要求分析ツール ktool 基本語彙辞書記号 dvd1 dvd2 dvd3 dvd5 基本語彙電源が入るコピー指示を受ける HDレコーダに再生を指示する受信した番組を録画する要求ｺﾞｰﾙ一覧要求ゴール電源が入るとコピー指示を受けるコピー指示を受けると再生を指示する再生を認識すると録画する再生が終了するまで録画を継続する機械 DVD DVD DVD DVD 種別状態ｲﾍﾞﾝﾄｲﾍﾞﾝﾄ変数検証支援ツール（試作）自動生成自動実行モデル検査ツール SPIN 検証カバレジの可視化サブゴールからの帰結によりvalid 検証によりinvalid 検証によりvalid 値 waiting start_copy req_play_HD 1 検証式 [] (dvd1 -> <> dvd2) [] (dvd2 -> <> dvd3) [] (dvd4 -> <> dvd5) [] (dvd5 -> (dvd5 U dvd9)) ※架空製品を想定検査仕様 Promela 属性受信送信 copying 状態遷移モデル状態遷移対応表検査項目一覧ゴールパターン Achieve □（Ａ→◇Ｂ）入力補助検証結果: Valid or Invalid 提案プロセスの評価従来検証用記述専用言語検証視点設計視点検証項目導出アドホック検証充分性不明検証体制個人依存本プロセス設計情報利用し自動化要求視点システマティック要求に対するカバレジロール間の共同作業架空製品を想定した事例での適用評価：要求数 43 件中、検証項目化した数 28件 valid 25件(検証:19、帰結:6)、invalid 3件トップエスイー ∼サイエンスによる知的ものづくり教育プログラム∼ 国立情報学研究所トップエスイー：サイエンスによる知的ものづくり教育プログラム National Institute of Informatics 文部科学省振興調整費産学融合先端ソフトウェア技術者養成拠点の形成文部科学省科学技術振興調整費産学融合先端ソフトウェア技術者養成拠点の形成