Output details

Towards verifying correctness of wireless sensor network applications using insense and spin

<02>This paper applies cutting-edge linear time temporal logic and model checking to the programming of wireless sensor networks. Such systems increasingly provide autonomous decision-making based on sensed data, where data and communications errors give rise directly to faulty decisions: the significance of this work is that formal analysis allows the properties of the sensor network to be verified to eliminate race conditions and so forth from the complex communications structures typically needed to handle partial failures in the network. Experimental results demonstrate importance by detecting a fault that would, in a production system, have given rise to significant errors.