• Search Research Projects
  • Search Researchers
  • How to Use
  1. Back to project page

2017 Fiscal Year Annual Research Report

Wireless sensor network featuring a self-healing mechanism and a dedicated formal verification mechanism to verify its behavior

Research Project

Project/Area Number 15K00133
Research InstitutionThe University of Aizu

Principal Investigator

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

Project Period (FY) 2015-04-01 – 2018-03-31
Keywordsセンサネットワーク / 形式検証 / 自己修復
Outline of Annual Research Achievements

本研究の目的は、外部より無線を用いて各センサノードにプログラムをリモートダウンロードすることにより、その振る舞いを再定義可能な無線センサネットワーク: 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を用いて検証される。最終年度として、センサノード間の通信における遅延やパケットロスを扱える様に動作モデルを拡張し、そられ現象を形式検証できるようにシステムを拡張した。本拡張は、現実的な無線センサネットワークの動作を検証する上で重要である。

  • Research Products

    (2 results)

All 2018

All Presentation (2 results) (of which Int'l Joint Research: 1 results)

  • [Presentation] Formal Verification for Wireless Sensor Network in Consideration of Communication Errors2018

    • Author(s)
      A. Ikeda, N. Akiyama, T. Miyazaki
    • Organizer
      IEEE ICOIN2018 (The 33rd International Conference on Information Networking)
    • Int'l Joint Research
  • [Presentation] C言語で記述した無線センサネットワーク動作の形式検証法の提案2018

    • Author(s)
      秋山直輝,池田愛大,宮崎敏明
    • Organizer
      情報処理学会第80回全国大会

URL: 

Published: 2018-12-17  

Information User Guide FAQ News Terms of Use Attribution of KAKENHI

Powered by NII kakenhi