• 研究課題をさがす
  • 研究者をさがす
  • KAKENの使い方
  1. 課題ページに戻る

2015 年度 実施状況報告書

動的システムに対する組込み制御プログラムの信頼性検証に関する研究

研究課題

研究課題/領域番号 26330092
研究機関日本大学

研究代表者

関澤 俊弦  日本大学, 工学部, 准教授 (10549314)

研究分担者 岡野 浩三  信州大学, 工学部, 准教授 (70252632)
研究期間 (年度) 2014-04-01 – 2017-03-31
キーワードモデル検査 / 確率的振舞い / 自律移動ロボット
研究実績の概要

平成27年度は,確率的な振舞いをもつ系のモデル化および検証を目的としていた.この目的に対して,平成26年度のモデル検査器SPIN上でのシミュレーションから,抽象化手法等の適用により状態数爆発を回避する必要があることが判明していた.この結果を受け,平成27年度には,本質的に連続量となる確率系に対して区間分割などの手法を適用しすることにより,状態数を抑制しつつマルコフ決定過程(Markov Decision Process)でモデル化が可能であることを示した.また,自律移動ロボットの実装例を具体的な対象として,確率的な振舞いが確率モデル検査で検証可能であることを示した.
上記の検証は,外乱を考慮した自律ロボットの誤差補正を対象としていた.しかし,自律移動ロボットの振舞いを考えたとき,自己位置推定などの要素技術が存在する.これらの要素技術に関してもモデル化および検証に着手し,確率的な振舞いを除いた系でモデル検査の適用可能性を示した.
提案手法の適用領域を拡張するためには確率的な性質のみならず,時間的な性質も考慮に入れる必要がある.そのため,時間的な性質のモデル検査における抽象化と反例解析手法の研究を行なった.

現在までの達成度 (区分)
現在までの達成度 (区分)

2: おおむね順調に進展している

理由

平成27年度に取り組む課題とされていた確率系の研究要素は,区間分割等の手法を適用することより,本質的に連続となる確率分布を離散的な状態に落とし込みモデル化が可能となった.また,外乱を含んだモデル化も実現している.これらのモデルには一定の制約があるものの,自律移動ロボットを対象としたモデル検査を用いた検証が可能であることを示した.また,対象系の組込みシステムを離散系と連続系が混在するハイブリッドシステムと捉えたときの検証に対しては,まず時間的な要素の扱いに取り組んだ.モデル検査の際に問題となる状態爆発問題を回避するために,時間的要素を扱う反例解析手法に取り組み,状態数削減に効果があるこを示した.研究対象領域の拡張に必要となるこれらの確率的および時間的要素の取り組みと,現実的な自律移動ロボットで考慮が必要となる外乱の扱いに対して,モデル検査を用いた検証手法を提案したことにより,おおむね予定通り進展していると判断した.

今後の研究の推進方策

確率系の検証において,現在,モデル化は人手で行なっている.しかし,この方法は人為的な誤りが混入するだけでなく,体系化されていない点に問題がある.これまでの取り組みから半自動的なモデル化を実現するための変換ルールを策定することにより,特定の性質を満たす自律移動ロボットのモデル検査手法の体系化に取り組みたい.また,具体的な自律移動ロボットを考えたとき,外乱や位置の確率的分布などは観測データに基づく必要がある.平成27年度に,LEGO EV3を用いて自律移動ロボットを実装したことにより,誤差の確率分布などが測定可能となっている.平成28年度は,これらの観測データを活用することにより,より現実的な振舞いに対して提案手法が適用可能であることを示す予定である.また,時間的な性質を含めた連続量をモデルに取り込むことにより,提案手法の拡張を試みる.この試みでは,モデル検査だけでなくシミュレーション等の協調が必要と考えられる.

次年度使用額が生じた理由

使用額に差異が生じた理由の1つとして,成果を論文誌に投稿するにあたり別刷り代などを保留したことと,平成27年度に研究分担者が異動したため,設備や旅費等の見込み額が変わったためです.また,平成26年度は,研究の進捗と照らし合わせMatlab/Simulinkの購入を見送ったことも一因です.

次年度使用額の使用計画

研究代表者および分担者の異動により旅費が申請時より増加する見込みであることと,研究計画で予定されている学会発表等に使用予定です.確率系などの信頼性保証においては,検証のみではなく,設計やシミュレーションの数値演算との組み合わせもアプローチの1つです.自律ロボットの実装により得られたこれまでの進捗を考えると,設計および解析用に平成27年度に購入を見送ったMatlab/Simulinkを購入する予定です.

  • 研究成果

    (6件)

すべて 2016 2015

すべて 雑誌論文 (1件) (うち査読あり 1件、 謝辞記載あり 1件) 学会発表 (5件) (うち国際学会 2件)

  • [雑誌論文] Parallel Multiple Counter-Examples Guided Abstraction Loop - Applying to Timed Automaton -2016

    • 著者名/発表者名
      Kozo Okano, Takeshi Nagaoka, Toshiaki Tanaka, Toshifusa Sekizawa, and Shinji Kusumoto
    • 雑誌名

      International Journal of Informatics Society

      巻: Vol. 8, No. 2 ページ: 103-116

    • 査読あり / 謝辞記載あり
  • [学会発表] 一次元系における自己位置推定の振舞い検証に向けて2016

    • 著者名/発表者名
      関澤俊弦,岡野浩三
    • 学会等名
      IEICE/SIGSS ソフトウェアサイエンス研究会
    • 発表場所
      沖縄県立宮古青少年の家 (沖縄県宮古島市)
    • 年月日
      2016-03-11 – 2016-03-11
  • [学会発表] 自然語要求仕様記述の形式検証に向けて - 話題沸騰ポットのモデル検査に向けて -2016

    • 著者名/発表者名
      遠藤健,小形真平,岡野浩三,関澤俊弦
    • 学会等名
      IPSJ/SIGSE ウィンターワークショップ 2016・イン・逗子
    • 発表場所
      湘南国際村センター (神奈川県三浦郡)
    • 年月日
      2016-02-04 – 2016-02-04
  • [学会発表] 時間的性質を考慮に入れた自律移動ロボットの誤差検出と振舞い検証に向けて2015

    • 著者名/発表者名
      小林佳正,岡野浩三,関澤俊弦
    • 学会等名
      JSSST 第22回 ソフトウェア工学の基礎ワークショップ
    • 発表場所
      ほほえみの宿 滝の湯 (山形県天童市)
    • 年月日
      2015-11-27 – 2015-11-27
  • [学会発表] Parallel Multiple Counter-Examples Guided Abstraction Loop to Timed Automaton2015

    • 著者名/発表者名
      Kozo Okano, Takeshi Nagaoka, Toshiaki Tanaka, Toshifusa Sekizawa, and Shinji Kusumoto
    • 学会等名
      International Workshop on Informatics 2015
    • 発表場所
      Amsterdam, Netherlands
    • 年月日
      2015-09-06 – 2015-09-09
    • 国際学会
  • [学会発表] Behavior Verification of Autonomous Robot Vehicle in Consideration of Errors and Disturbances2015

    • 著者名/発表者名
      Toshifusa Sekizawa, Fumiya Otsuki, Kazuki Ito, and Kozo Okano
    • 学会等名
      The 1st IEEE International Workshop on Dependable Software and Applications
    • 発表場所
      Taichung, Taiwan
    • 年月日
      2015-07-05 – 2015-07-05
    • 国際学会

URL: 

公開日: 2017-01-06  

サービス概要 検索マニュアル よくある質問 お知らせ 利用規程 科研費による研究の帰属

Powered by NII kakenhi