2013 年年度度ソフトウェア 工学分野の先導的研究 支援事業 抽象化に基づいた UML 設計の検証 支援ツールの開発 公 立立 大学法 人岡 山県 立立 大学情報 工学部情報システム 工学科 横川智教
背景 - 組込みソフトウェア開発の課題 組込みソフトウェアの開発プロセス 要求分析 設計 実装 テスト 手戻り 下流流 工程での不不具合の検出 上流流 工程への 手戻りの発 生 手戻りによる開発コスト増 大 設計検証の必要性の 高まり 2014/07/29 ETWest2014 IPAブースプレゼン 2
背景 - 組込みソフトウェアの設計検証 設計ドキュメント 要求仕様 どの状態にもいつか必ず到達する 危険な状態には決して到達しない UML( 状態マシン図 ) ある変数が定められた値に必ず到達する 作成された設計ドキュメントが要求仕様を満たしているか? 2014/07/29 ETWest2014 IPA ブースプレゼン 3
背景 - 設計検証の困難さ 従来の枠組み ( テスト レビュー ) で組込みソフトウェアの設計検証を 行行うのは 非常に困難である 理理由 1. 組込みソフトウェアの不不具合が社会に及ぼす影響が甚 大であり, 信頼性への要求のハードルが 非常に 高い 2. ソフトウェアの 大規模 複雑化により, システムの取り得る状態数が 人 手でテストを 行行う限界を遙かに越えている 網羅羅的かつ 自動検証が可能なモデル検査技術の利利 用 2014/07/29 ETWest2014 IPA ブースプレゼン 4
モデル検査 モデル検査とは 状態遷移系でモデル化されたシステムの全数探索索により求める特性を満たすか否かを 自動検証する技術 モデル検査の適 用 1. モデル化 言語により検査対象システム ( 仕様書 設計書 回路路図 etc.) を記述 2. 論論理理式として検査項 目 ( 要求仕様 試験仕様 基本性質 客先要望 etc.) を記述 3. モデル検査ツールによる 自動探索索の実施 4. モデルが検査項 目を満たすという証明か, 満たさない場合は反例例を出 力力 2014/07/29 ETWest2014 IPA ブースプレゼン 5
研究課題 モデル検査を設計検証に導 入する上での問題点 問題 1. モデル作成の困難さ 対象システムを検証ツール固有のモデル化 言語で記述 モデル作成には専 門的な知識識やノウハウが必要 問題 2. 状態爆発の危険性 モデル化された対象システムの状態空間を網羅羅的探索索 モデル規模によっては検証に莫 大な時間を要する モデル作成を 支援するためのツールを開発し問題を解決 2014/07/29 ETWest2014 IPAブースプレゼン 6
検証 支援ツール 前提 1. 対象とする設計記法として, 組込みソフトウェア開発に広く利利 用されている形式仕様記法 UML を想定する 2. モデル検査ツールとして, モデル記述 言語の表現 力力および検証速度度に優れた NuSMV を利利 用する ツールの機能 1. SMV 言語への 自動変換を 目的とした UML 図の抽象化 2. モデルサイズ削減を 目的とした UML 図の抽出 分割および抽象化 3. UML 図から SMV 言語への 自動変換 2014/07/29 ETWest2014 IPA ブースプレゼン 7
検証 支援ツールの概要 要求仕様 (*.ctl) UML 図 (*.asta) 入 力力インタフ ス ー 仕様 テンプレート 要求仕様 記述制約 UML 図 抽象化 変換モジ ル ー 検証モデル (*.smv) 検証結果 (*.out) 出 力力インタフ ス ー 検証結果 ( 整形済 ) (*.result) 違反箇所 情報 (*.ce) UML モデリングツール astah* モデル検査ツール NuSMV 検証 支援ツール 外部ツール l UML 図の記述には astah* を, 検証には NuSMV を 用いる l UML 図が満たすべき記述制約と, 要求仕様を記述するための仕様テンプレートが定められている 2014/07/29 ETWest2014 IPA ブースプレゼン 8
SMV 言語による検証モデル 生成の流流れ 状態マシン図 シーケンス図 UML 図ファイル (*.asta) safe(xxx = 1) live(message_1) reachable(s) モデル 生成 CTL 式 生成 MODULE main VAR XXX : {aaa, bbb, ccc}; YYY : {ddd, eee, fff}; fg1 : boolean; ASSIGN init(xxx) := aaa; next(xxx) := case fg = TRUE : bbb; TRUE : XXX; esac; init(yyy) := ddd; next(yyy) := case fg = FALSE : fff TRUE : YYY; esac; init(fg) := FALSE; next(fg) := case fg = FALSE : {TRUE, FALSE}; TRUE : fg; esac; SPEC AG!(XXX = ccc) SPEC EF(ZZZ = iii) SPEC AF(YYY = fff) モデル CTL 式 要求仕様ファイル (*.ctl) 検証モデルファイル (*.smv) 2014/07/29 ETWest2014 IPAブースプレゼン 9
事例例適 用による評価 l 経緯 某ソフトウェア開発企業に事例例提供を打診 開発に 用いた状態遷移表から UML 図 ( 状態マシン図 ) を作成 対象システムは店舗従業員向けの 商品供給指 示システム 売場の端末と商品管理理室のモニターの間で, 商品供給のための通信を 行行う l 検査項 目 検査 1: 仕様テンプレートを 用いた基本特性の検査 検査 2: 事例例提供元より要望のあった特性の検査 2014/07/29 ETWest2014 IPA ブースプレゼン 10
検査対象となる UML 図 2 台の売場端末とモニター表 示の動作の状態マシン図 ( 状態遷移表を元に作成 ) 端末 A 端末 B モニター UML 図ファイル R_CDS.asta 2014/07/29 ETWest2014 IPA ブースプレゼン 11
検査 1 仕様テンプレートを 用いて 4 つの基本特性を記述 検査項 目 テンプレート ツールへの 入 力力 状態の到達可能性 通信モードの到達可能性 通信モードの安全性 モニターの到達可能性 reachable(s) reachable(x,a) safe(x,a) reachable(s) reachable(terminal_a = send) reachable(terminal_a = receive) reachable(terminal_a = com) reachable(terminal_b = send) reachable(terminal_b = receive) reachable(terminal_b = com) reachable(md_a, 1) reachable(md_a, 2) reachable(md_b, 1) reachable(md_b, 2) safe(md_a, 3) safe(md_a, - 1) safe(md_b, 3) safe(md_b, - 1) reachable(ctl_monitor = surplus) reachable(ctl_monitor = sufficient) reachable(ctl_monitor = opdmal) reachable(ctl_monitor = few) reachable(ctl_monitor = short) 要求仕様ファイル BASIC.ctl 2014/07/29 ETWest2014 IPA ブースプレゼン 12
本ツールの適 用結果 ( 検査 1) R_CDS.asta BASIC.ctl R_CDS_BASIC.smv R_CDS_BASIC.out R_CDS_BASIC.result 本ツールを 用いて SMV ファイルを 生成 モデル検査器 NuSMV で検査 検査結果の整形 (001) EF Terminal_A = send is true (002) EF Terminal_A = receive is true (003) EF Terminal_A = com is true (004) EF Terminal_B = send is true (005) EF Terminal_B = receive is true (006) EF Terminal_B = com is true (007) EF MD_A = 1 is true (008) EF MD_A = 2 is true (009) EF MD_B = 1 is true (010) EF MD_B = 2 is true (011) AG!(MD_A = 3) is true (012) AG!(MD_A = - 1) is true (013) AG!(MD_B = 3) is true (014) AG!(MD_B = - 1) is true (015) EF Ctl_Monitor = surplus is true (016) EF Ctl_Monitor = sufficient is true (017) EF Ctl_Monitor = opdmal is true (018) EF Ctl_Monitor = few is true (019) EF Ctl_Monitor = short is true R_CDS_BASIC.result 全ての結果がTRUE 誤りは存在しない 2014/07/29 ETWest2014 IPAブースプレゼン 13
検査 2 事例例提供元より要望のあった特性を直接検査式として記述 1. 端末が待機状態であり, かつ通信モードが通話無しでない状態への到達可能性 2. 端末が着信中状態であり, かつ通信モードが 2 回線通話である状態への到達可能性 3. 端末が通話中であり, かつ通信モードが通話無しである状態への到達可能性 1A: SPEC!EF(Terminal_A = wait &!(MD_A = 0)) 2A: SPEC!EF(Terminal_A = receive & MD_A = 2) 2A: SPEC!EF(Terminal_A = com & MD_A = 0) 1B: SPEC!EF(Terminal_B = wait &!(MD_B = 0)) 2B: SPEC!EF(Terminal_B = receive & MD_B = 2) 3B: SPEC!EF(Terminal_B = com & MD_B = 0) 要求仕様ファイル R_CDS_REQ.ctl 2014/07/29 ETWest2014 IPA ブースプレゼン 14
本ツールの適 用結果 ( 検査 2) R_CDS.asta R_CDS_REQ.ctl R_CDS_REQ.smv R_CDS_REQ.out R_CDS_REQ.result R_CDS_REQ.ce (001)!(EF (Terminal_A = wait &!(MD_A = 0))) is true (002)!(EF (Terminal_A = receive & MD_A = 2)) is true (003)!(EF (Terminal_A = com & MD_A = 0)) is false R_CDS_REQ.result( 一部 ) 結果が FALSE 誤りを検出し, 反例例を出 力力 (003)!(EF (Terminal_A = com & MD_A = 0)) is false - > State: 1.1 <- Terminal_A = inidal MD_A = 0 Power = start Event_A = emp R_CDS_REQ.ce( 一部 ) 2014/07/29 ETWest2014 IPA ブースプレゼン 15
本ツールの適 用結果 ( 検査 2) 特性 3A に対する反例例の解析 1 2 3 4 5 Event_A emp emp report response emp MD_A 0 0 0 0 0 Terminal_A inidal inidal wait send com 端末が通信中 (Terminal_A=com) であるにもかかわらず, 通信モードが通話無し (MD_A=0) となる状態に到達している 原因 : 状態遷移表のアクションの 1 つが UML 図に正しく転記されていなかった UML 図による設計の誤りを正しく検出できた 反例例を元に誤り箇所を特定することができた 2014/07/29 ETWest2014 IPA ブースプレゼン 16
まとめ 2014/07/29 ETWest2014 IPA ブースプレゼン 17 ツールデモ 本ツールのデモを岡 山県 立立 大学のブース (U- 06) 内にて実施しています. お気軽にお越しください. 成果 モデル検査による UML 設計の検証 支援ツールの開発 開発現場における事例例への適 用に基づく評価 自動検証による 人的 時間的コストを削減 ソフトウェア信頼性の担保
謝辞 本発表は, 独 立立 行行政法 人情報処理理推進機構 技術本部ソフトウェア 高信頼化センター (IPA/SEC) が実施した, 2013 年年度度ソフトウェア 工学分野の先導的研究 支援事業 (RISE) の 支援を受けて, 公 立立 大学法 人岡 山県 立立 大学 ( 研究責任者 有本和 民 ) が 行行った研究成果の 一部を取りまとめたものです. 2014/07/29 ETWest2014 IPA ブースプレゼン 18