情報処理学会 第80回全国大会講演要旨

無線センサネットワークは、温度や湿度といった環境の監視に適しており、また環境の変化に合わせてその動作を変更することも可能である。しかし、それぞれのセンサノードは並列に動作しており、互いに影響を及ぼし合うため、センサネットワーク振る舞いの正しさを、シミュレーションなどを用いて事前に動作保証することは困難である。本稿は、C言語で記述した無線センサノードの動作仕様を、形式検証手法を用いて検証する手法を提案する。また、提案手法の適用結果を、具体的なセンサネットワーク動作例を用いて示す。