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

無線センサネットワークは、環境モニタリングに有効である。しかし、各センサノードの振る舞い、または互いに影響を及ぼし合うセンサネットワークとしての振る舞いを検証し、デッドロックを事前に見つけることは難しい。我々は、Communicating Sequential Processes（CSP）に基づく形式検証ツールと、無線センサノードで実際に動作するコードを同時に生成するシステムを実現した。本稿では、周期呼び出しのある実用的な例に対し、我々のシステムを適用した結果を示す。