組込みシステムの外部環境に 着目した動作仕様検証 九州工業大学　鵜林研究室 金川 太俊　瀬戸 敏喜　谷口 奨　吉田 純　鵜林　尚靖 (株)東芝 ソフトウェア技術センター 鷲見 毅　　　平山 雅之

目次 研究の背景 形式手法を用いた外部環境分析の妥当性確認 適用事例 まとめと今後の課題 外部環境分析手法 外部環境分析における問題点 テスト実行 システムと外部環境の振舞い検証 適用事例 まとめと今後の課題

組込みシステムにおける 外部環境分析とその問題点 研究の背景 組込みシステムにおける 外部環境分析とその問題点

本研究は組込みシステム開発における信頼性向上を目的とする 研究の背景 不具合発覚！ システム開発プロセス 分析 設計 実装 テスト 最初から見直し コスト大 上流工程 下流工程 ドキュメント 分析 設計 実装 テスト 信頼性の高い出力であれば手戻りは軽減できる 本研究は組込みシステム開発における信頼性向上を目的とする

：システム外の環境から影響を受け、不具合を出すケースが多い 組込みシステム開発の特徴 ：システム外の環境から影響を受け、不具合を出すケースが多い →外部環境を分析する手法を提案 外部環境を分析することで組込みシステム開発における信頼性を向上させる 上流工程 下流工程 不具合発覚！ 外部環境分析 分析 設計 実装 テスト ドキュメント 外部環境を考慮したモノ 外部環境に起因するものは 存在しない →信頼性向上 不具合

外部環境の範囲：システムに要求された安全性、信頼性、機能性 を満たすために必要な範囲 外部環境分析手法 1.組込みシステムと外部環境とのインタラクションを行うハードウェアを抽出する 2.抽出したハードウェアが注目する要素(Context)と、その値に影響をする要素 　(Context)を抽出する 3.組込みシステムと外部環境の構造を、UMLプロファイルを用いて静的/動的の 　両側面から記述する 《Actuator》 《Sensor》 駆動モータ 光センサ 外乱 【コメント】 外部環境分析手法(つまり、このスライドで説明している範囲)は、既に提案してきている事を口頭で説明できる様にしておいて下さい。 車体の速度 ラインの 反射光 例：ライントレーサロボット 環境光 コースの勾配 外部環境の範囲：システムに要求された安全性、信頼性、機能性 　　 を満たすために必要な範囲

成果物：外部環境クラス図 →外部環境の静的記述 システム クラスごとに ステレオタイプ付加 関連ごとに ステレオタイプ付加 外部環境 【コメント】 外部環境用のステレオタイプ(《Hardware》、《Observe》等々)について、上手く説明できる様にしておいて下さい。 スライドとして追加する必要は無いと思いますが、その分、口頭で上手く説明する必要がありますので。 外部環境

成果物：各クラスの状態遷移 →外部環境の動的記述 遷移イベント： 他クラスの状態遷移 光センサ 直下部の反射光 環境光 直下部の色 高い 低い 光センサ 直下部の反射光：強い 直下部の反射光：弱い 遷移イベント： 他クラスの状態遷移 直下部の反射光 強い 弱い 環境光 時間の経過 直下部の色：黒 強い 弱い 直下部の色：白 直下部の色、ラインとの位置関係は不要かもしれません 【コメント】 このスライドも、前のスライドと同様に、ポイントを上手く説明できる様にしておいて下さい。 私が考える範囲では、 “外部環境に登場する、他の《Context》の状態変化が遷移条件になっている” 事がポイントだと思いますが、 その他にも、形式モデルを作成する際にポイントとなる事があれば、それを説明できると良いです。 黒 白 直下部の色 ラインとの位置関係：ライン外 ラインとの位置関係：ライン上 ライン上 ライン外 ラインとの位置関係 車体の走行

外部環境分析における問題点 本研究の目的 外部環境分析の範囲を決定する指針が無い システム要件を満たす範囲で外部環境分析を行いたい 現状、範囲の決定は分析者がAd-hocに行っている 本研究の目的 論理的な根拠に基づく外部環境分析範囲の妥当性確認を行う そのためのアプローチとして形式手法（Formal Method）を用いる 外部環境 Ad-hoc 以下の文章から、本研究の問題意識を明確に示す方が良い。 “外部環境の範囲：システムに要求された安全性、信頼性、機能性を満たすために必要な範囲”としているが、 　⇒しかし、この範囲を決定する指針が無い 　　分析者が、Ad-hocに決定している 　　↑ 　これが、本研究の問題意識のはず その上で、本研究の目的を示す。 　⇒そこで、形式手法を導入する事で、上記の範囲の決定に、ある程度の論理的な根拠を示せる様にする 　これが、本研究の目的になるはず システム 論理的根拠 分析範囲

：形式手法を用いた外部環境分析の妥当性確認 アプローチ ：形式手法を用いた外部環境分析の妥当性確認 形式手法 数学を用いた厳密な仕様記述 仕様の検証 現在の外部環境分析でシステム要件を満たすか否かを数学的に検証する 不具合が発見されなければ現在の分析は妥当なもの 同時に、分析範囲外の外部環境については考慮していないことを明示することにもなる ここで示されているアプローチは、VDMを用いた仕様の探索に関してのみ SPINを用いる根拠となる、システムと外部環境を合せた振舞いを網羅的に検証する部分の説明が無い 【コメント】 このスライドで、 　“形式検証を行って、不具合が発見されなければ、外部環境の範囲として妥当と考えて良い” という事を主張しておく必要がある。 つまり、 ・既存：「これくらい考えておけば、多分大丈夫だろう」という、経験ベースの(悪く言えば、Ad-hocな)根拠 ・提案：「形式検証による検査をパスしたので、大丈夫」という、テスト結果に基づいた根拠 　　　　また、「形式検証を行った範囲外については、保証さていない」事を明示しているとも、メリットとして主張できる 　　　　⇒結果、検証された範囲(＝仕様として検討した範囲)の妥当性を議論するベースを作れた事になる。 という事を説明しておく必要があります。 外部環境分析で得られた結果を形式手法に置き換え、検証する

形式手法を用いた 外部環境分析の妥当性確認

形式手法の使用目的 外部環境分析結果 システム要件を満たすか？ １．テスト実行 現在の外部環境範囲において、 潜在する不具合はないか？ ２．網羅的振舞い検証 現在の外部環境分析は 妥当なものである

外部環境を考慮に入れたテストを上流工程で行う 現在の外部環境分析のもと、システム要件を満たすかをテストにより確認する 形式手法の使用目的（1） ：上流工程でのテスト実行 外部環境を考慮に入れたテストを上流工程で行う 現在の外部環境分析のもと、システム要件を満たすかをテストにより確認する どこまでを外部環境仕様の範囲とすべきか数値をもって探索する 形式手法に変換 type ・・・ operations 外部環境の仕様 テスト実行 仕様の変更 ツール補助により上流工程でのテスト実行が可能な、 VDM （Vienna Development Method）を用いる

システムと外部環境の状態の組み合わせを網羅する 不具合が潜在する組み合わせがないか検査する 形式手法の使用目的（2） ：システムと外部環境との振舞いを網羅的に検証 システムと外部環境の状態の組み合わせを網羅する 不具合が潜在する組み合わせがないか検査する システム 外部環境 【コメント】 網羅的な検証を行う意義について、以下の様な説明をすると良いと思います。 　VDMによるテスト実行は、どちらかというと機能を断片的に検証していると言える。 　従って、外部環境の状態によっては、検証漏れとなっているケースが無いとは言えない。 　⇒SPINによる網羅的な検証によって、その点(網羅性)を補う。 振舞いを検証 自動で網羅的検査を行うことができる、 SPINを用いる

形式手法の導入方法 ・外部環境分析手法 UMLプロファイルを作成 ・プロファイルは形式手法への導入を意識して作成している 外部環境分析手法 ＵＭＬプロファイル 外部環境分析手法 クラス図 状態遷移図 ・クラスの種類 ・クラス間の関連 ・各クラスの状態遷移 形式手法 VDM SPIN active proctype ・・・(){ do ::　・・・ 　od } type ・・・ operations

適用事例 テスト実行 振舞い検証 適用事例の説明は、 “説明を聞けば、どうやって検証を行うのかイメージできる” 事を目標として説明内容を精査して下さい。 今のままだと、「何となく分かった様な、分からない様な…」と言う感想になると思います。

VDMを用いて外部環境を考慮した仕様の探索を行う 適用事例（１） ：テスト実行 VDMを用いて外部環境を考慮した仕様の探索を行う 分析時に想定している外部環境の属性値をパラメータとして変化させ、テストケースを作る テストケースに従いテスト実行 現在の仕様でシステム要件を満たすか確認する 範囲によって満たさない場合があるならば、その範囲を数値的に明示する このスライド以降で、VDMで記述されたモデルを用いて、どうやって仕様探索を行うかを説明する ・まずは、テスト実行を用いて仕様の確認を行う事を説明する 【コメント】 元々は、「ツール補助によるテスト実行」の次、 「VDM：テスト実行による探索（ライントレース機能）」の前に置かれていたスライドをここに持ってきました。 VDMのテスト実行によって仕様探索を行う事について、概略を説明するスライドだと思うので、事例による具体的な説明の前に置いた方が良さそうです。 (この辺は、プレゼンの仕方に対する個人的な好みもありますので、判断はお任せします。)

VDM適用例 外部環境分析結果からの入力 →外部環境クラス図 外部環境クラス図からクラスごとに情報を抜き出す ステレオタイプ クラス名 クラスの種類 クラス間の関連 外部環境クラス図からクラスごとに情報を抜き出す ステレオタイプ クラス名 クラスの属性

VDM-SL（ VDM-Specification Language ）による記述 例：環境光 ステレオタイプ：Context クラス名：環境光 属性：光量：real ステレオタイプ VDM-SLで記述 Contextの記述形式に基づく記述（本研究で定義） types LightVolume = real state EnvironmentLight of environment_light　:　LightVolume init el == el = mk_EnvironmentLight(0) end クラスの属性 必要であれば、関連についても用意します クラス名 ＊VDM-SL：VDMの記述言語の一つ

：今回はCSKシステムズが公開している 「VDMTools」を使用 ツール補助によるテスト実行 ：今回はCSKシステムズが公開している 「VDMTools」を使用 このスライド以降で、VDMで記述されたモデルを用いて、どうやって仕様探索を行うかを説明する ・まずは、テスト実行を用いて仕様の確認を行う事を説明する

VDM：テスト実行による探索（ライントレース機能） 光センサが扱うセンサ値は0～100 100 白を示す値（誤認識） 環境光 下限値 上限値 期待値 10 40 60 90 25 75 白 センサ値：75 環境光 環境光の大きさがセンサに対し30の影響を与えるとき 環境光の大きさがセンサに対し15の影響を与えるとき 環境光の大きさがセンサに対し60の影響を与えるとき どちらともとれない中間値 環境光 センサ値：55 環境光 ・各パラメータの値によって想定外の動作が生じるケースが存在する ・テストケースを作成しそれらのケースを探索する このスライドで説明されている、パラメータを調整している点について ・何故、センサ値や反射光の値を調整しているのかを説明する 　恐らく、センサ値や反射光の値が、分析時に想定している(＝分析者の想定に依存している)為、調整の対象になっていると思われる 　⇒その点を説明する ・分析時に想定している部分は、モデル上のどこに現れるかについても説明する 　⇒調整する際、モデル上のどこをいじれば良いかの指針を示した方が、手法のメリットを納得してもらい易い 環境光 センサ値：40 反射光の値：25 黒 ※黒：反射光（10～40） 実験等により既に明確

VDM：テスト実行による探索（ライントレース機能） 各種パラメータを変化させテスト実行する 変化させるパラメータ＝分析時に想定するパラメータ ・環境光の値 ・反射光の値 ＊色の閾値と期待値：システム側で規定する部分のため対象外 例：環境光のパラメータを変化させる types LightVolume = real state EnvironmentLight of environment_light　:　LightVolume init el == el = mk_EnvironmentLight(30) end types LightVolume = real state EnvironmentLight of environment_light　:　LightVolume init el == el = mk_EnvironmentLight(0) end types LightVolume = real state EnvironmentLight of environment_light　:　LightVolume init el == el = mk_EnvironmentLight(15) end パラメータ変化

VDM：テスト実行による探索 この問題について、 下限値10、上限値40 　　　　反射光の値 環境光の値 10 25 40 OK 15 中間値 30 誤認識 45 60 この問題について、 「環境光が30以上の状況では動作を保証しない」という仕様にするか、HWの追加等行い問題を解決するかは設計判断であり、 本手法の範囲外のものと考えている 中間値は読み飛ばせばよい 問題は黒を白と誤認識してしまうこと このテストにより、環境光の値が30以上となったとき、動作の保証が不可能であることが分かった

SPINを用いてシステム全体と外部環境の振舞いを検証する 適用事例（２） ：網羅的探索による振舞い検証 SPINを用いてシステム全体と外部環境の振舞いを検証する VDMでは機能ごとに検証を行ったが、SPINではシステム全体の動作を検証する 外部環境分析範囲は一種の閉空間である その閉空間の中において不具合を引き起こすケースがないか網羅的に探索する 事例で用意されている成果物(外部環境クラス図と状態遷移図)と、ここで検証する内容(ライントレース機能と障害物回避機能の競合)が繋がりません。 少なくとも、これまでの事例で使っていた成果物では、ライントレース機能と障害物回避機能の検証はできないはずです。 ⇒適用事例は、これまでの事例でSPINにかけて、問題が無い(デッドロックもライブロックも起きない)事を確認した、でも良いと思います。 　この時、VDMで仕様探索を行った後の外部環境モデルを使ってSPINの検証ができれば、本研究で提案する検証の全体像を掴んでもらえると思います。 【コメント】 元々は、「SPIN適用例（ライントレーサ：光センサの観測）」の次に置かれていたスライドを、ここに持ってきました。 (理由は、VDMの適用事例のスライドと同じです。好みによるという点も同じ。) SPINによる網羅的な検証の意義について、以下の様な説明を入れてはどうですか。 　VDMによるテスト実行は、どちらかというと機能を断片的に(離散的に)検証していると言える。 　一方で、SPINによるモデル検査は、問題領域(システム＋外部環境)を、網羅的に検証している。 　つまり、VDMによる検証の“隙間”を埋める意味合いがある。 　⇒「本当に(どんな場合でも)、この仕様で大丈夫な事を、モデル検査で網羅的に検証しましょう」という意味合い

SPIN適用例 外部環境分析結果からの入力 →各クラスの状態遷移図 各状態遷移図から情報を抜き出す 状態 遷移イベント 各クラスの状態遷移 各クラスの並行性 各状態遷移図から情報を抜き出す 強い 弱い 環境光 時間の経過 状態 遷移イベント

Promeraによる記述 Promeraで記述 独立に動作 active proctype EnvironmentLight(){ do 強い 弱い 環境光 時間の経過 例：環境光 並行性：独立に動作 イベント：時間の経過（非決定的） 状態：強い、弱い Promeraで記述 独立に動作 active proctype EnvironmentLight(){ do ::EL_state = EL_Weak; ::EL_state = EL_Strong; od } 状態 非決定的

状態遷移図を全てPromeraで記述する 振舞いをSPINで検証する

SPINによる振舞い検証 新規の不具合なし この結果から…. エラー表示 車体はライン上 システムはライン外と認識している 環境光は強い状態 ラインとの位置関係 環境光 強い ライン上 システム 新規の不具合なし ライン外と認識

適用事例まとめ 外部環境分析結果 システム要件を満たすか？ 環境光による 不具合発覚 １．テスト実行 現在の外部環境範囲において、 潜在する不具合はないか？ 新規の不具合 なし ２．網羅的振舞い検証 現在の外部環境分析は 妥当なものである

まとめ・今後の課題

・形式手法を用いることで外部環境分析の妥当性確認が行える ・分析範囲内で発見した不具合への対応は製品企画の側面からの判断が必要 まとめ ・形式手法を用いることで外部環境分析の妥当性確認が行える ・分析範囲内で発見した不具合への対応は製品企画の側面からの判断が必要 ・但し、どんな場合に問題となるかが明確になるので、製品企画上の判断を助ける情報を提供できる 今後の課題 ・形式モデルの作成手順を整理して、より容易に実行できる様にする ・組込みシステムに限らず、コンテキスト分析が必要な開発全てに適用可能な手法に発展させる まとめについて ・2点目の“ケースバイケース”という表現は問題あり 　⇒仕様探索によって問題がある事が分かった場合の対応は、製品企画の側面からの判断が必要 　　但し、どんな場合に問題となるかが明確になるので、製品企画上の判断を助ける情報を提供できる 　くらいの表現の方が良い。 今後の課題について ・“形式手法へのマッピングを明確にする”と書いてしまうと、今回はどうやって形式モデルを作ったのか、と言われる 　⇒形式モデルの作成手順を整理して、より容易に実行できる様にする 　くらいの表現に抑えておく ・“MDAなどに…”は、無くても良い

終

補足用

ライントレース機能と障害物回避機能の競合 SPIN：網羅的探索による振舞い検証 ライントレース機能と障害物回避機能の競合 ライントレース機能： 光センサを用いてラインを検知し、進行方向をライン上なら左へ、ライン外なら右へとる 障害物回避機能： 超音波センサを用いて、障害物の存在しない分岐方向へ進む、この状況では進行方向を左へとることで回避する 障害物 障害物を検知したので左へ ①ライントレース走行中 ライン外へ出たので右へ これを適用事例として出すならば、障害物回避機能を含めたライントレーサの形式モデルが必要 ⇒恐らく、用意している時間は無いので、今回の発表では出さない方が無難では？ ※モデルを用意できるなら、発表した方が良いのは間違いないが… 【コメント】 スライド15、スライド25に対するコメントを考えると、障害物の話は無くても良いかも… SPINによるモデル検査が、VDMのテスト実行による検証の“何を”を補うかは、センサ間の競合が無くても説明できそうなので。 ②超音波センサが障害物を検知