ディペンダブル組込みシステムのためのコンテキスト分析手法九州工業大学瀬戸敏喜組込みシステムの特徴 • 組込みシステムは外部環境から影響を受け、異常動作をとることが多く見られる • これは，システムが不具合を起こしやすいことを示しており，信頼性の面で問題があると考えられる《Sensor》光センサ外乱例：ライントレーサロボットラインの反射光環境光外部環境分析の必要性 • 要求分析終了時にシステムと外部環境との関係を分析する工程を置く上流工程下流工程へ外部環境を考慮した出力を送ることができる →外部環境に起因する不具合を減らすことによって信頼性向上を図る要求分析外部環境分析設計出力下流工程外部環境を分析するための手法として実装 CAMEmb（A Context Analysis Method for Embedded Systems）を提案テスト本手法の要点 • システムにとって本質的には不要な要素による影響の分析 – システムによるコンテキストの観測経路，制御経路のモデル化による影響要素の発見 • システムが扱いたい情報とハードウェアによって実際に扱えるもののギャップを表現 – 影響要素によってシステムの動作がどう変わるかを形式手法によって検査モデリングコンテキスト要件定義ハードウェア分析表モデル記述 UML（UMLプロファイル，OCL）システムモデル形式手法による検証構造検証 Alloy Analyzer 動作仕様検証テスト実行： VDM Tools + Alloy Analyzer 網羅検証： SPIN システム要件コンテキスト要件コンテキストモデル本手法で扱うディペンダブルに関する関心事 • システムの持つ性質による分類 – – – – – – – 可用性(Availability) 信頼性(Reliability) 安全性(Safety) 完全性(Integrity) 保守性(Maintainability) セキュリティその他(？？？) • システムを作る手段による分類 – – – – – – 欠陥防止(Fault Prevention) 耐故障性(Fault Tolerance) 欠陥除去(Fault Removal) 欠陥予測(Fault Forecasting) 反撃(Counter Attack) その他(？？？) • システムへの脅威による分類 – – – – – 失敗(Failure) 過誤(Error) 欠陥(Fault) 攻撃(Attack) その他(？？？) • 赤字および太字が対象となる関心事関心事に対する解決策 • • • • ディペンダブルの関心事のモデル化性質の保証ディペンダブルの関心事と他の要素との関連モデルの活用例題仕様：障害物分岐対応ライントレーサ ■ライントレーサ：ドライブモータにより速度制御ステアモータにより進行方向制御 ■ライントレーサの走行経路：ラインに沿って走行実線障害物 ■障害物検知によるルート選択：障害物のないルートを選択分岐，合流コンテキストのモデル化 • 静的モデルの特徴 – 通常は属性として記述されるような項目をクラスとして記述する • システムの動作に影響する情報の関連がわかりやすくなる – UMLプロファイルを用いてクラス間の関連をいくつかの種類に分類している • 動的モデルの特徴 – 静的モデルから特定の要素を選択し，その状態遷移を記述するコンテキストの静的モデル図システムのコンテキスト観測経路 ■青矢印：システムの本来の観測経路 ■青枠：システムの本来の観測対象システムの観測に対する影響経路 ■赤矢印：システム本来の観測を阻害する影響経路 ■赤枠：システム本来の観測を阻害する影響要素コンテキストの情報源 ■黄矢印：観測対象から情報源への経路 ■黄枠：観測対象の情報源コンテキストの静的モデル図コンテキストの動的モデルモデルの活用：形式手法を用いた検査 • コンテキストモデルの妥当性検査 – コンテキストには満たすべき性質が存在 • モデルが性質を満たしているか構造面から検査 – Alloy Analyzer • システムの動作仕様検査 – コンテキストに対応したシステム仕様を探索する必要 • コンテキスト上でのシステム仕様テストによる試行を繰り返す – VDM-Tools + Alloy Analyzer – 作成した仕様の動作を網羅的に検査 • コンテキスト上でのシステム動作の網羅検証 – SPIN モデルの活用：形式手法を用いた検査 • コンテキストモデルの妥当性検査 – コンテキストには満たすべき性質が存在 • モデルが性質を満たしているか構造面から検査 – Alloy Analyzer • システムの動作仕様検査 – コンテキストに対応したシステム仕様を探索する必要 • コンテキスト上でのシステム仕様テストによる試行を繰り返す – VDM-Tools + Alloy Analyzer – 作成した仕様の動作を網羅的に検査 • コンテキスト上でのシステム動作の網羅検証 – SPIN システムモデル網羅検証 • システムと外部環境の状態の組み合わせを網羅する • 不具合が潜在する組み合わせがないか検査するシステム外部環境振舞いを検証自動で網羅的検査を行うことができる、 SPINを用いるシステムモデル+外部環境モデルシステムモデル各状態遷移図をPromeraで記述する外部環境動的モデル ※システムモデル、外部環境モデル共にCAMEmbモデリング工程にて作成済み状態遷移図を全てPromeraで記述し、SPINで振舞検証を行うシステムモデル+外部環境モデル状態モデルをPromeraで記述 active proctype System(){ do:: If ::PS_state == On -> SM_state = SM_Right; ::PS_state == PS_OutSide -> SM_state = SM_Left; ::OB_state == OB_Near -> SM_state = SM_Left; fi; od } SPIN 振舞いをSPINで検証する active proctype Position(){ do ::PS_state = PS_On; ::PS_state = PS_OutSide; od } LTLによる時相論理に基づく検証 • システムが動作する上で守られなくてはならない制約をLTLで記述する • ライントレーサ動作上の制約 – 障害物が存在する場合、システムは左にステアリングを切る – これをLTLで記述すると以下のようになる • []((障害物：有) -> <>ステアモータ：左) – 障害物：有ならば、いつかはステアモータ：左となることが常に守られる – 制約が常に守られるか確認（信頼性，安全性検査） SPIN検証結果ライン検出→右ステア障害物検出→左ステアシステムが上記の二つの挙動をとりうるとき、「ライン検出→右ステア」が常に優先された場合、左ステアが実行されることは無いシステムモデルにはエラーが潜在していた！ SPIN検証結果 ■ライントレーサ ■ライントレーサの走行経路 ■本来進むべき経路 ■誤動作により障害物に衝突 →信頼性，安全性に問題あり障害物 ■障害物検知によるルート選択：ライン追跡動作が優先され右ルートへ向かう実線分岐，合流システムモデルの修正 • 対策例 – ライン追跡動作よりも障害物回避を優先する設定の追加 – 具体的には：ガード条件の付加 • 「ライン検出→右ステア」の際、[障害物：無]というガード条件を付加する • これにより「障害物検出→左ステア」の実行を保証することができるまとめ • モデリング工程により，システムへの脅威である失敗（Failure）の原因となる要素を発見し，モデル化する • 形式手法による検査工程により，前述の失敗（Failure）により起こりうる欠陥を予測（Fault Forecasting）し，対策を講じることでそれを防止（Fault Prevention）する • CAMEmbでは，上記の方法でシステムの信頼性（Reliability）や安全性（Safety）の向上を図る