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

2015 年度 実施状況報告書

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

研究課題

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

研究代表者

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

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

本研究の目的は、外部より無線を用いて各センサノード(以下、単にノード)にプログラムをリモートダウンロードすることにより、その振る舞いを再定義可能な無線センサネットワーク: Reconfigurable Sensor Network(RSN)を実現することである。研究の初年次として、ノード動作を正確に定義するのに十分な記述能力を持ち、かつ、記述したノード動作の無矛盾性をダウンロード前に、形式的検証手法によりチェック出来る枠組みを持つプログラム記述言語の設計を中心に行った。

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

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

理由

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

今後の研究の推進方策

構築した動作仕様の形式検証環境をユーザビリティの観点から見直し、ユーザにとってより使い易い環境に改変すると共に、検証済みの動作が実機センサノードで、実際に動作することを確認する。次に、本研究のもう一つの課題であるノードの自己修復動作の実現を目指し、各ノードは、ダメージを受けた近隣ノードの機能を肩代わりするように、自律的に、サーバからプログラムをダウンロードし、RSNの機能を継続しようとする機構の実現に取り組む。

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

当初予定していた言語処理系(Funclet+トランスレータ)の初期開発機能が見積よりも安く済んだため。

次年度使用額の使用計画

次年度へ繰り越す予算は、採択された国際会議(2016.7)および次年度投稿を予定している国内会議の参加費に使用する予定。
また、次年度の予算は、すべて言語処理系の改変に使用する予定。

  • 研究成果

    (1件)

すべて 2016

すべて 学会発表 (1件) (うち国際学会 1件)

  • [学会発表] Formal Approach to Produce Verified Programs for Wireless Sensor Node2016

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

URL: 

公開日: 2017-01-06  

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

Powered by NII kakenhi