ディペンダブル組込みシステムのためのコンテキスト分析手法 瀬 戸 敏 喜 † ， 金 川 太 俊 †， 谷 口 奨††， 吉 田 純††， 鵜 林 尚 靖†† 本稿では，コンテキストを考慮した要求分析手法 CAMEmb (Context Analysis Method for Embedded systems) を提案する．CAMEmb は UML ベースのモデリング手法と形式検証支援から構成され，これを用いる ことにより，コンテキストを考慮した厳密な仕様を獲得することが可能となる． A Context Analysis Method for Dependable Embedded Systems TOSHIKI SETO†, HIROTOSHI KANAGAWA†, SUSUMU TANIGUCHI††, JUN YOSHIDA††, NAOYASU UBAYASHI†† This position paper proposes a context-dependent requirements analysis method called CAMEmb (Context Analysis Method for Embedded systems) consisting of UML-based modeling and formal verification support. Adopting CAMEmb, we can obtain rigorous specifications that take into account the contexts. 1. はじめに 本稿では，組込みシステムに特化したディペンダブ ル ソ フトウェアの要 求 分 析 手 法 CAMEmb (Context Analysis Method for Embedded systems) について述 べる．本稿でいう組込みシステムは，システム外部の環 境（コンテキスト）を観測するセンサ，コンテキストを変化 させるためのアクチュエータなどのハードウェアと，それ らを制御するソフトウェアで構成される．コンテキストは， 組込みシステムのアクチュエータによる制御のほかにも さまざまな要因で変化するため，その組み合わせによ っては，ソフトウェアによるアクチュエータの制御が期待 したものにならず，システムが異常動作を起こす可能 性がある．CAMEmb では，このような不具合の防止に よりシステムの安全性向上を図る． † 九州工業大学大学院 情報工学研究科 情報科学専攻 †† 九州工業大学 情報工学部 知能情報工学科 コンテキスト要件定義 コンテキスト要件定義 ハードウェア分析表 ハードウェア分析表 モデル記述 モデル記述 UML（ （UMLプロファイル プロファイル， ） プロファイル， OCL） システムモデル 形式手法による検証 CAMEmb では，コンテキストに起因した不具合をシ ステム開発の早期に発見することができる．不具合の 例をライントレース機能と障害物回避機能を持つライン トレーサで考える．このライントレーサは，コンテキストの 状態によっては，ライントレース機能による右ステアリン グと，障害物回避機能による左ステアリングの実行が 同時に起こり，実際のステアリング方向が不定となる可 能性がある．これでは，車体がそのまま障害物に向か モデリング 2. CAMEmb の概要 ってしまう可能性があり，システムの安全性に問題があ ると考えられる．このような不具合は，開発早期での発 見と対策の検討が有効と考える． CAMEmb によってシステムの不具合を発見する手 順は，システムの動作に関係するコンテキストのモデル 化と，記述したモデル上でのシステムの動作検証の二 工程からなる．図 1に CAMEmb の全体像を示す．以 下で各工程を簡単に説明する． 2.1. モデリング モデリングの工程では，システムと関係するコンテキ ストを明確にし，検証で考慮する範囲を定める．モデル の記述は，コンテキストの要件を定義した上で行う．コ ンテキストの要件とは，コンテキストに対する制約の記 述であり，例えばライントレーサの場合，「障害物は分 岐後のどちらか一方のライン上にのみ配置される可能 システム要件 システム要件 コンテキスト要件 コンテキスト要件 コンテキストモデル 構造検証 Alloy Analyzer 動作仕様検証 テスト実行 実行： テスト実行： VDM Tools + Alloy Analyzer 網羅検証： 網羅検証： SPIN 図 1 : CAMEmb の全体像 図 2 : ライントレーサのコンテキストモデル（一部） 性がある」などの制約を記述する．また，検証時に用い る簡単なシステムモデルも記述する． コンテキストモデルはシステムの動作に影響する自 然界の状態をコンテキストとしてモデル化したものであ る．図 2に，ライントレーサのコンテキストモデルの一部 を示す．ステレオタイプ<<Context>>のクラスがコンテキ ストの構成要素であり，<<Sensor>>はシステムの持つ センサを表す．図から，光センサは「ラインの有無」を 「地面からの反射光」として間接的（<<Transfer>>）に検 出（<<Observe>>）し，それを阻害する（<<Noise>>）要 因として「環境光」が存在すること，さらに「地面からの 反射光」にも影響を与える（<<Affect>>）要素であること がわかる．また，「ラインの有無」は「コース」に依存して いる．CAMEmb では，これらを UML 標準の拡張メカニ ズムである UML プロファイルによって定義している[1]． システムモデルは，センサによる入力とアクチュエー タによる出力の関係をモデル化したもので，ソフトウェア の動作とその入出力を簡略化して表現する． 2.2. 形式手法による検証 形式手法による検証では，モデル化したコンテキス トの範囲において，システムが意図通りに動作すること を確認する．これには，まずコンテキストモデルの構造 を検証し，その後，システムの動作仕様の検証を行え ば良い．これにより，システムの不具合を防止できる． (1) 構造検証 構造検証では，モデリング工程で記述したコンテキ ストモデルが要件を満たしているかを確認する．これは， 動作仕様検証において，存在しないコンテキストによる 異常の検出を防止する．例えば，「障害物は分岐先の どちらか一方のライン上にのみ配置される可能性があ る」というライントレーサのコンテキスト要件について検 査すると，分岐先の両方のラインに障害物があり，迂回 ルートが存在しないコースがコンテキストとなりうるモデ ルの場合，そのようなインスタンスが示される．このよう な場合はモデルの修正が必要なことがわかり，そのま ま動作仕様検証に進むことによる，存在しないコンテキ ストによる異常の検出を防止できる． 検証には Alloy Analyzer を用い，コンテキストの構 造に対して，述語論理による条件を与え検証を行う． 例えば，図 2のようなコンテキストを Alloy モデルに変 換し検証することで，前述のような問題のあるコースが コンテキストとなりうるモデルでないかを確認できる． (2) 動作仕様検証 検証により妥当であることが示されたコンテキストモ デルを用い，システムの動作をテスト実行と網羅検証 の二つの工程で検証する．テスト実行ではシステムモ デルの機能が意図どおりであることを確認し，網羅検 証ではそのモデルがコンテキストモデルと組み合わさ れて全体として動作したときに不正な状態にならないこ とを確認する． 本項では特に，網羅検証について説明する．この 工程では，モデル化した範囲のコンテキストにおいて， システムが意図通りに動作することを確認する．ここで 異常が見つかった場合，それはシステムの不具合であ る．前述したライントレーサのステアリング操作の競合 の問題はこの工程で発見できる． 検証には SPIN を用い，コンテキスト及びシステムを 有限状態マシン，ハードウェアによる観測と制御を通信 とした協調動作のプロセスに対して，時相論理による条 件の検証を行う． 3. 今後の課題 本稿では，CAMEmb による不具合発見による，組 込みシステムの安全性向上について述べた．今後の 課題として，誤認識や競合の検証に現在のツールで 十分か，信頼性等に影響を与える他の要因がないか の検討などが考えられる． 本研究にあたり，多大なご協力をいただいた(株)東 芝の平山雅之氏，鷲見毅氏に感謝いたします． 参考文献 [1] 瀬戸敏喜, 金川太俊, 鵜林尚靖, 鷲見毅, 平山 雅之: 組込みシステムの外部環境分析のための UML プロファイル, 情報処理学会 組込技術とネ ットワークに関するワークショップ ETNET2007, 研究報告 2007-EMB-4, pp.65-70, 2007.
© Copyright 2024 ExpyDoc
