ディペンダブル組込みシステムのためのコンテキスト分析手法 九州工業大学 瀬戸敏喜

組込みシステムの特徴 組込みシステムは外部環境から影響を受け、異常動作をとることが多く見られる これは，システムが不具合を起こしやすいことを示しており，信頼性の面で問題があると考えられる 《Sensor》 光センサ 外乱 ラインの 反射光 環境光 例：ライントレーサロボット

外部環境分析の必要性 要求分析終了時にシステムと外部環境との関係を分析する工程を置く 下流工程へ外部環境を考慮した出力を送ることができる 上流工程 要求分析 下流工程へ外部環境を考慮した出力を送ることができる →外部環境に起因する不具合を減らすことによって信頼性向上を図る 外部環境分析 設計 出力 下流工程 外部環境を分析するための手法として CAMEmb（A Context Analysis Method for Embedded Systems）を提案 実装 テスト

本手法の要点 システムにとって本質的には不要な要素による影響の分析 システムによるコンテキストの観測経路，制御経路のモデル化による影響要素の発見 システムが扱いたい情報とハードウェアによって実際に扱えるもののギャップを表現 影響要素によってシステムの動作がどう変わるかを形式手法によって検査

本手法で扱う ディペンダブルに関する関心事 システムの持つ性質による分類 可用性(Availability) 信頼性(Reliability) 安全性(Safety) 完全性(Integrity) 保守性(Maintainability) セキュリティ その他(？？？) システムへの脅威による分類 失敗(Failure) 過誤(Error) 欠陥(Fault) 攻撃(Attack) システムを作る手段による分類 欠陥防止(Fault Prevention) 耐故障性(Fault Tolerance) 欠陥除去(Fault Removal) 欠陥予測(Fault Forecasting) 反撃(Counter Attack) その他(？？？) 赤字および太字が対象となる関心事

関心事に対する解決策 ディペンダブルの関心事のモデル化 性質の保証 ディペンダブルの関心事と他の要素との関連 モデルの活用

例題仕様： 障害物分岐対応ライントレーサ ■ライントレーサ： ドライブモータにより速度制御 ステアモータにより進行方向制御 ■ライントレーサの走行経路： ラインに沿って走行 実線 障害物 分岐，合流 ■障害物検知によるルート選択： 障害物のないルートを選択

コンテキストのモデル化 静的モデルの特徴 動的モデルの特徴 通常は属性として記述されるような項目をクラスとして記述する システムの動作に影響する情報の関連がわかりやすくなる UMLプロファイルを用いてクラス間の関連をいくつかの種類に分類している 動的モデルの特徴 静的モデルから特定の要素を選択し，その状態遷移を記述する

コンテキストの静的モデル図

システムのコンテキスト観測経路 ■青矢印：システムの本来の観測経路 ■青枠：システムの本来の観測対象

システムの観測に対する影響経路 ■赤矢印：システム本来の観測を阻害する影響経路 ■赤枠：システム本来の観測を阻害する影響要素

コンテキストの情報源 ■黄矢印：観測対象から情報源への経路 ■黄枠：観測対象の情報源

コンテキストの静的モデル図

コンテキストの動的モデル

モデルの活用： 形式手法を用いた検査 コンテキストモデルの妥当性検査 システムの動作仕様検査 コンテキストには満たすべき性質が存在 モデルが性質を満たしているか構造面から検査 Alloy Analyzer システムの動作仕様検査 コンテキストに対応したシステム仕様を探索する必要 コンテキスト上でのシステム仕様テストによる試行を繰り返す VDM-Tools + Alloy Analyzer 作成した仕様の動作を網羅的に検査 コンテキスト上でのシステム動作の網羅検証 SPIN

モデルの活用： 形式手法を用いた検査 コンテキストモデルの妥当性検査 システムの動作仕様検査 コンテキストには満たすべき性質が存在 モデルが性質を満たしているか構造面から検査 Alloy Analyzer システムの動作仕様検査 コンテキストに対応したシステム仕様を探索する必要 コンテキスト上でのシステム仕様テストによる試行を繰り返す VDM-Tools + Alloy Analyzer 作成した仕様の動作を網羅的に検査 コンテキスト上でのシステム動作の網羅検証 SPIN

システムモデル

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

システムモデル+外部環境モデル 各状態遷移図をPromeraで記述する システムモデル 外部環境動的モデル ※システムモデル、外部環境モデル共にCAMEmbモデリング工程にて作成済み

状態遷移図を全てPromeraで記述し、SPINで振舞検証を行う システムモデル+外部環境モデル 状態モデルをPromeraで記述 SPIN 振舞いをSPINで検証する

LTLによる時相論理に基づく検証 システムが動作する上で守られなくてはならない制約をLTLで記述する ライントレーサ動作上の制約 障害物が存在する場合、システムは左にステアリングを切る これをLTLで記述すると以下のようになる []((障害物：有) -> <>ステアモータ：左) 障害物：有ならば、いつかはステアモータ：左となることが常に守られる 制約が常に守られるか確認（信頼性，安全性検査）

SPIN検証結果 ライン検出→右ステア 障害物検出→左ステア システムが上記の二つの挙動をとりうるとき、 「ライン検出→右ステア」 が常に優先された場合、左ステアが実行されることは無い システムモデルにはエラーが潜在していた！

SPIN検証結果 ■ライントレーサ ■ライントレーサの走行経路 ■本来進むべき経路 ■誤動作により障害物に衝突 →信頼性，安全性に問題あり 　→信頼性，安全性に問題あり 実線 障害物 ■障害物検知によるルート選択： ライン追跡動作が優先され右ルートへ向かう 分岐，合流

システムモデルの修正 対策例 ライン追跡動作よりも障害物回避を優先する設定の追加 具体的には：ガード条件の付加 「ライン検出→右ステア」の際、[障害物：無]というガード条件を付加する これにより「障害物検出→左ステア」の実行を保証することができる

まとめ モデリング工程により，システムへの脅威である失敗（Failure）の原因となる要素を発見し，モデル化する 形式手法による検査工程により，前述の失敗（Failure）により起こりうる欠陥を予測（Fault Forecasting）し，対策を講じることでそれを防止（Fault Prevention）する CAMEmbでは，上記の方法でシステムの信頼性（Reliability）や安全性（Safety）の向上を図る