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

2017 Fiscal Year Final Research Report

• Project/Area Number: 15K00133
• Research Category: Grant-in-Aid for Scientific Research (C)
• Allocation Type: Multi-year Fund
• Section: 一般
• Research Field: Information network
• Research Institution: The University of Aizu
• Principal Investigator: Miyazaki Toshiaki 会津大学, コンピュータ理工学部, 教授 (70404895)
• Project Period (FY): 2015-04-01 – 2018-03-31
• Keywords: センサネットワーク / 形式検証 / 自己修復 / プログラマブル / CSP / OTAP

Outline of Final Research Achievements

We realized a wireless sensor network named Reconfigurable Sensor Network (RSN), in which behavior can be redefined by downloading a new program to sensor nodes remotely using wireless communication. To define RSN behavior, dedicated behavior description language Funclet+ was designed. A language translator was also developed. It generates an input description to a formal verification tool, and C description. Both generated descriptions represent the behavior described using Funclet+. Thus, by validating the generated input description using the formal verification tool, we can ensure that the generated C description properly represents the behavior described using Funclet+. We described some typical sensor node behaviors using Funclet+, and confirmed that the generated C descriptions can run on real sensor nodes properly after verifying the behaviors using the formal verification tool.

Free Research Field

情報通信