Demo: Towards bug-free implementation for wireless sensor networks
Manchun Zheng, Jun Sun, David Sanán, Yang Liu, Jin Song Dong, Yu Jason Gu · 2011
In this demonstration, a systematically domain-specific model checker, NesC@PAT, is presented. The tool takes NesC programs as input, and automatically verifies WSNs against properties specified in the form of deadlock freeness, state reachability or linear temporal logic formulas. We will show that NesC@PAT is able to find errors caused by rarely unexpected scenarios, which are difficult to be detected by general simulating or debugging.