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

無線センサネットワークは環境モニタリングに有用である。また、所望の動作をするようにプログラムを変更することができる。しかし、センサネットワークではそれぞれのセンサノードが並行に動作し、互いに影響を及ぼし合っているのでその振る舞いは複雑でありその正しさを確認するのは難しい。本稿では、形式手法を用いて無線センサノードのプログラムを検証する手法を提案する。また、従来の形式手法では時間概念の欠如により困難だった通信エラー処理も検証可能とした。