Verification and power analysis of an event-based system (TinyOS) and sensor network with hybrid automata

The advances In digital circuitry and sensor technology has enabled reliable monitoring of environments through wireless microsensor systems. Event-driven operating system has been shown to meet the requirements of such platforms. In this paper, we focus on TinyOS, an event-based operating system for Smart Dust networked sensors. We show how to model TinyOS as a hybrid automata with the tool HyTech and verify the correct operation of the system by using safety verification feature of HyTech. Since lifetime is a important metric for sensor nodes that are planned to be deployed once and unattended for long periods of time without maintenance, we perform power analysis of a sensor node by using trace generation feature of HyTech. Furthermore, we simulate a tree sensor network of TinyOS motes by using the programming language SHIFT to determine the lifetime of the network as a function of the distance from the central data collector.