Formal Verification for Wireless Sensor Network in Consideration of Communication Errors

Wireless sensor networks (WSNs) consist of many wireless sensor nodes and their behavior is often programmable. However, it is hard to check the correctness of new program for wireless sensor nodes because each node works autonomously. In this paper, we propose a formal verification framework that can detect not only algorithmic errors but also communication ones, which cannot be handled by previous formal verification approaches for WSNs. Using our environment, the program describing sensor node behavior can be verified before installing it in the sensor node. After describing communication model and system structure, we show how it works using an example.