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

Coleri S., Ergen M.

6th World Multi-Conference on Systemics, Cybernetics and Informatics (SCI 2002)/8th International Conference on Information Systems Analysis and Synthesis (ISAS 2002), Florida, United States Of America, 14 - 18 July 2002, pp.553-558 identifier

  • Publication Type: Conference Paper / Full Text
  • Volume:
  • City: Florida
  • Country: United States Of America
  • Page Numbers: pp.553-558
  • Istanbul Technical University Affiliated: Yes


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.