Lifetime analysis of a sensor network with hybrid automata modelling
- 28 September 2002
- conference paper
- Published by Association for Computing Machinery (ACM)
Abstract
In this paper, we focus on TinyOS, an event-based operating system for networked sensor motes. We show how to model TinyOS as a hybrid automata with HyTech and verify the correct operation of the system by using safety verification feature of HyTech. Since lifetime is an 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.Keywords
This publication has 4 references indexed in Scilit:
- System architecture directions for networked sensorsPublished by Association for Computing Machinery (ACM) ,2000
- Next century challengesPublished by Association for Computing Machinery (ACM) ,1999
- HYTECH: a model checker for hybrid systemsInternational Journal on Software Tools for Technology Transfer, 1997
- Automatic symbolic verification of embedded systemsIEEE Transactions on Software Engineering, 1996