Abstract. We provide the first tool for verifying the logic of contextaware applications written for the mainstream sensor network operating system TinyOS; we focus on detecting pr...
We investigate the application of the software bounded model checking tool CBMC to the domain of wireless sensor networks (WSNs). We automatically generate a software behavior mode...