Wireless sensor network featuring a self-healing mechanism and a dedicated formal verification mechanism to verify its behavior
| 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 |
|
|---|
| Project Period (FY) |
2015-04-01 – 2018-03-31
|
| Project Status |
Completed (Fiscal Year 2017)
|
| Budget Amount *help |
¥4,680,000 (Direct Cost: ¥3,600,000、Indirect Cost: ¥1,080,000)
Fiscal Year 2017: ¥780,000 (Direct Cost: ¥600,000、Indirect Cost: ¥180,000)
Fiscal Year 2016: ¥1,950,000 (Direct Cost: ¥1,500,000、Indirect Cost: ¥450,000)
Fiscal Year 2015: ¥1,950,000 (Direct Cost: ¥1,500,000、Indirect Cost: ¥450,000)
|
|---|
| 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.
|
Report
(4 results)
Research Products
(7 results)
