Allan I. McInnes
Abstract
Wireless sensor networks are an increasingly popular application area for embedded systems. Individual sensor nodes within a network are typically resource-constrained, event-driven, and require a high degree of concurrency. This combination of requirements motivated the development of the widely used TinyOS sensor node operating system. The TinyOS concurrency model is a lightweight nonpreemptive system designed to suit the needs of typical sensor network applications. Although the TinyOS concurrency model is easier to reason about than preemptive threads, it can still give rise to undesirable behavior due to unexpected interleavings of related tasks, or unanticipated preemption by interrupt handlers. To aid TinyOS developers in understanding the behavior of their programs we have developed a technique for using the process algebra Communicating Sequential Processes (CSP) to model the interactions between TinyOS components, and between an application and the TinyOS scheduling and preemption mechanisms. Analysis of the resulting models can help TinyOS developers to discover and diagnose concurrency-related errors in their designs that might otherwise go undetected until after the application has been widely deployed. Such analysis is particularly valuable for the TinyOS components that are used as building blocks for a large number of other applications, since a subtle or sporadic error in a widely deployed building block component could be extremely costly to repair.
- Archer, W., Levis, P., and Regehr, J. 2007. Interface contracts for TinyOS. In Proceedings of the 6th International Conference on Information Processing in Sensor Networks (IPSN’07). ACM, 158--165. Google Scholar
Digital Library
- Bucur, D. and Kwiatkowska, M. 2009. Towards software verification for TinyOS applications. In Proceedings of the Workshop on Formal Approaches to Ubiquitous Systems (FAUSt’09).Google Scholar
- Clarke, E. M. and Wing, J. M. 1996. Formal methods: State of the art and future directions. ACM Comput. Surv. 28, 4, 626--643. Google ScholarDigital Library
- Culler, D. E. 2006. TinyOS: Operating system design for wireless sensor networks. Sensors 23, 5.Google Scholar
- Gardiner, P. et al. 2005. Failures-Divergences Refinement: FDR2 User Manual. Formal Systems (Europe) Ltd.Google Scholar
- Gay, D., Levis, P., von Behren, R., Welsh, M., Brewer, E., and Culler, D. 2003. The nesC language: A holistic approach to networked embedded systems. ACM SIGPLAN Not. 38, 5, 1--11. Google ScholarDigital Library
- Gay, D., Levis, P., Culler, D., and Brewer, E. 2005. nesC 1.2 language reference manual. http://nescc.cvs.sourceforge.net/viewvc/*checkout*/nescc/nesc/doc/ref.pdf?revision=1.18.Google Scholar
- Kleine, M. and Helke, S. 2009. Low-level code verification based on CSP models. In Proceedings of the Brazilian Symposium on Formal Methods (SBMF’09). Springer, 266--281. Google ScholarDigital Library
- Kothari, N., Millstein, T., and Govindan, R. 2008. Deriving state machines from TinyOS programs using symbolic execution. In Proceedings of the 7th International Conference on Information Processing in Sensor Networks (IPSN’08). IEEE Computer Society, 271--282. Google ScholarDigital Library
- Levis, P. 2006. TinyOS programming. http://csl.stanford.edu/ pal/pubs/tinyos-programming.pdf.Google Scholar
- Levis, P. 2007. TinyOS 2.x boot sequence. TinyOS Extension Proposal TEP-107, TinyOS Core Working Group.Google Scholar
- Levis, P., Lee, N., Welsh, M., and Culler, D. 2003. TOSSIM: Accurate and scalable simulation of entire TinyOS applications. In Proceedings of the 1st International Conference on Embedded Networked Sensor Systems (SenSys’03). ACM, 126--137. Google ScholarDigital Library
- Levis, P., Madden, N., et al. 2005. TinyOS: An operating system for sensor networks. In Ambient Intelligence, W. Weber, J. Rabaey, and E. Aarts, Eds. Springer, 115--148.Google Scholar
- McInnes, A. I. 2009. Using CSP to model and analyze TinyOS applications. In Proceedings of the 16th Annual IEEE International Conference and Workshop on the Engineering of Computer Based Systems (ECBS’09). IEEE Computer Society, 79--88. Google ScholarDigital Library
- Rosa, N. S. and Cunha, P. R. F. 2007. Using LOTOS for formalising wireless sensor network applications. Sensors 7, 8, 1447--1461.Google ScholarCross Ref
- Roscoe, A. W. 1998. The Theory and Practice of Concurrency. Prentice Hall, Englewood Cliffs, NJ. Google ScholarDigital Library
- Sharp, C. 2008. AlarmToTimerC.nc. TinyOS 2.x Source. http://code.google.com/p/tinyos-main/source/browse/trunk/tos/lib/timer/AlarmToTimerC.nc?r=5108.Google Scholar
- Völgyesi, P., Maróti, M., Dóra, S., Osses, E., and Lédeczi, Á. 2005. Software composition and verification for sensor networks. Sci. Comput. Prog. 56, 1--2, 191--210. Google ScholarDigital Library
- Woehrle, M., Plessl, C., Beutel, J., and Thiele, L. 2007.Increasing the reliability of wireless sensor networks with a distributed testing framework. In Proceedings of the 4th Workshop on Embedded Networked Sensors (EmNets’07). ACM, 93--97. Google ScholarDigital Library
- Xie, F., Yang, G., and Song, X. 2006. Compositional reasoning for hardware/software co-verification. In Proceedings of the 4th International Symposium on Automated Technology for Verification and Analysis. Springer, 154--169. Google ScholarDigital Library
Index Terms
- Modeling and Analysis of TinyOS Sensor Node Firmware: A CSP Approach
Recommendations
Design of Wireless Sensor Networks Node in Coalmine
ICICTA '09: Proceedings of the 2009 Second International Conference on Intelligent Computation Technology and Automation - Volume 04Combined with the temperature and gas monitoring demand, a new technology which is called wireless sensor network is used to solve the problems exiting in most cable transmission systems. Base on designing of wireless sensor networks low-power hardware ...
Node Placement Strategy in Wireless Sensor Network
The performance and quality of services in wireless sensor networks WSNs depend on coverage and connectivity. Node placement is a fundamental issue closely related to the coverage and connectivity in sensor networks. Node placement influences the target ...
Viptos: a graphical development and simulation environment for TinyOS-based wireless sensor networks
SenSys '05: Proceedings of the 3rd international conference on Embedded networked sensor systemsWe are announcing the first release of Viptos (Visual Ptolemy and TinyOS), an integrated graphical development and simulation environment for TinyOS-based wireless sensor networks. Viptos allows developers to create block and arrow diagrams to construct ...
Reviews
S. Ramesh
This paper, as the name suggests, formalizes certain elements of TinyOS, an operating system that has become popular in the domain of sensor networks. The well-known formalism of communicating sequential processes (CSP) is used for modeling TinyOS, as there is a good match between the elements of CSP and TinyOS, such as concurrency and event-driven computation. The formalization involves translating programs written in nesC, the application language used in TinyOS, into CSP. This translation captures the interactions between multiple TinyOS applications. Besides this, CSP models of the scheduling, preemption, and priority mechanisms of TinyOS are also developed. The formalization is illustrated with a simple example of a TinyOS application. The motivation for the work is that a formal model of an application can be subjected to rigorous analysis, which can reveal subtle concurrency-related errors that are common in such applications. This well-written paper is easy to read and understand. That being said, I would have liked more illustrations and examples from real applications that bring out the need for formalization. The paper would be useful to beginners who are interested in formalizing concurrent systems, and for application developers wanting a better understanding of the TinyOS model. Online Computing Reviews Service
Access critical reviews of Computing literature here
Become a reviewer for Computing Reviews.
Comments