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

2016 年度 実施状況報告書

形式的動作検証機能と自己修復機能を備えた無線センサネットワークの研究

研究課題

研究課題/領域番号 15K00133
研究機関会津大学

研究代表者

宮崎 敏明  会津大学, コンピュータ理工学部, 教授 (70404895)

研究期間 (年度) 2015-04-01 – 2018-03-31
キーワード形式的検証 / 自己修復
研究実績の概要

本研究の目的は、外部より無線を用いて各センサノードにプログラムをリモートダウンロードすることにより、その振る舞いを再定義可能な無線センサネットワーク: Reconfigurable Sensor Network(RSN)を実現することである。センサノード動作を記述する専用言語Funclet+を設け、その記述から、形式検証ツールへの入力記述と、C言語記述を生成するトランスレータを開発した。また、いくつかの典型的なセンサノードの動作をFunclet+言語で記述し、その記述にミスがないことを形式検証ツールで検証できることを確認した。さらに、上述のトランスレータから生成されたC言語記述をコンパイルして得られたオブジェクトコードを、実機センサノードにダウンロードし、定義した仕様通りに正しく動作することも確認した。
ノードの動作を正確に規定するには、(A)自ノード・隣接ノードの状態把握及びその状態に依存するアクション,(B)センサ制御(on/off, sampling rateなど),(C)データ処理(Signal processing, data aggregation, packet transferなど)の3項目が定義出来なければならない。Funclet+言語の設計に際しては、上記を考慮した。また、Funclet+は、プロセス代数の一つであるCSP(Communicating Sequence Processes)に基づいており、上述のトランスレータは、Funclet+記述からCSP記述を生成する。生成されたCSP記述は、CSPの形式検証ツールであるPATを用いて検証される。一方、トランスレータから生成されたC言語記述は、クロスコンパイラによりコンパイルされ、オブジェクトコードを得る。得られたオブジェクトコードは、我々が過去に開発した実機センサノードと、それ用の開発環境を用いて、当該センサノードへダウンロードされる。

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

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

理由

ノードの動作を正確に規定するには、(A)自ノード・隣接ノードの状態把握及びその状態に依存するアクション,(B)センサ制御(on/off, sampling rateなど),(C)データ処理(Signal processing, data aggregation, packet transferなど)の3項目が定義出来なければならない。それらが定義できるノードの動作記述言語Funclet+を設計し、それによって記述した動作をCSP(Communicating Sequence Processes)記述に変換するトランスレータを試作した。また、生成したCSP記述が既存の形式検証ツールPATで形式検証可能であることを確認した。さらに、上記トランスレータは、Funclet+記述からC言語記述も生成でき、それをコンパイルして得たオブジェクトコードが実機センサノードで正しく動作することも確認した。ほぼ予定通りの進捗である。

今後の研究の推進方策

昨年度までにセンサノードあるいはセンサネットワークの動作定義に矛盾がないかを、形式検証を用いて確認し、実機センサノードで誤りなく動作するプログラムを生成するといった当初の目的を達成するシステムを完成させた。しかしながら、現状、形式検証ツールで検証できる動作仕様は限定的で、大規模な動作を検証することはできない。それを解決するために、階層的な動作仕様が定義できるようにシステムを拡張し、詳細部分は、既に検証済みとして、最上位階層の動作仕様のみ検証すれば、全体の動作が保証できるようにする。次に、本研究のもう一つの課題であるノードの自己修復動作の実現を目指し、各ノードは、ダメージを受けた近隣ノードの機能を肩代わりする機構の実装に取り組む。

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

当初試作したトランスレータの改変を外部に委託する予定であったが、当該委託を延期し、仕様の見直し等に集中したため。

次年度使用額の使用計画

仕様の変更および新規開発項目を整理した後、平成29年度にトランスレータの改変を、外部委託する。予算の多くは、本外部委託に使用する予定である。

  • 研究成果

    (4件)

すべて 2017 2016

すべて 雑誌論文 (1件) (うち査読あり 1件) 学会発表 (3件) (うち国際学会 1件)

  • [雑誌論文] Demand-Addressable Sensor Network: Toward Large-Scale Active Information Acquisition2016

    • 著者名/発表者名
      T. Miyazaki, N. Suematsu, D. Baba, P. Li, S. Guo, J. Kitamichi, T. Hayashi, and T. Tsukahara
    • 雑誌名

      IEEE Sensors Journal

      巻: 16 ページ: 7421-7432

    • DOI

      10.1109/JSEN.2016.2575846

    • 査読あり
  • [学会発表] 無線センサネットワークにおけるデッドロック検出のための形式手法2017

    • 著者名/発表者名
      池田愛大,秋山直輝,宮崎敏明
    • 学会等名
      情報処理学会第79回全国大会
    • 発表場所
      名古屋
    • 年月日
      2017-03-16 – 2017-03-18
  • [学会発表] Deadlock-free Behavior Definition for Wireless Sensor Nodes Using Formal Verification2016

    • 著者名/発表者名
      N. Akiyama, A. Ikeda and T. Miyazaki
    • 学会等名
      IEEE student session in 2016 Tohoku-Section Joint Convention of Institutes of Electrical and Information Engineers, Japan
    • 発表場所
      仙台
    • 年月日
      2016-08-30 – 2016-08-31
  • [学会発表] Formal Approach to Produce Verified Programs for Wireless Sensor Nodes2016

    • 著者名/発表者名
      T.Miyazaki and N. Akiyama
    • 学会等名
      IEEE 10th International Symposium on Communication Systems, Networks and Digital Signal Processing (CSNDSP2016)
    • 発表場所
      Prague
    • 年月日
      2016-07-20 – 2016-07-22
    • 国際学会

URL: 

公開日: 2018-01-16  

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

Powered by NII kakenhi