research-article

T-check: bug finding for sensor networks

Authors:

John RegehrAuthors Info & Claims

IPSN '10: Proceedings of the 9th ACM/IEEE International Conference on Information Processing in Sensor Networks

Pages 174 - 185

https://doi.org/10.1145/1791212.1791234

Published: 12 April 2010 Publication History

Abstract

Sensor nodes are resource poor and failure-prone. Sensor networks are composed of many such nodes that are often hard to physically reach and that are connected by unreliable wireless links. Together, these factors make sensor network debugging into a challenging activity, and in fact it is not uncommon for a deployed sensornet to encounter sporadic faults that are effectively impossible to locate, reproduce, and fix.

We developed T-Check, a tool that uses random walks and explicit state model checking to find safety and liveness errors in sensor network applications running on TinyOS. By building upon TOSSIM---an event-driven simulator that abstracts away interrupt-driven concurrency and other low-level hardware interaction---T-Check loses the ability to detect certain low-level errors, but gains enough scalability to detect distributed errors such as a collection tree protocol's failure to properly repair when a node dies. We have used T-Check to find previously unknown bugs in TinyOS.

References

[1]

Will Archer, Philip Levis, and John Regehr. Interface contracts for TinyOS. In Proc. of the Intl. Conf. on Information Processing in Sensor Networks (IPSN'07), SPOTS Track, Cambridge, MA, April 2007.

Digital Library

[2]

Thomas Ball and Sriram K. Rajamani. The SLAM project: Debugging system software via static analysis. In Proc. of the 29th ACM Symp. on Principles of Programming Languages (POPL), Portland, OR, USA, January 2002.

Digital Library

[3]

Dirk Beyer, Thomas A. Henzinger, Ranjit Jhala, and Rupak Majumdar. The software model checker Blast: Applications to software engineering. Intl. Journal on Software Tools for Technology Transfer, 9(5--6), October 2007.

Digital Library

[4]

Qing Cao, Tarek Abdelzaher, John Stankovic, Kamin Whitehouse, and Liqian Luo. Declarative tracepoints: A programmable and application independent debugging system for wireless sensor networks. In Proc. of the 6th ACM Conf. on Embedded Networked Sensor Systems (SenSys), Raleigh, NC, USA, November 2008.

Digital Library

[5]

E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems (TOPLAS), 8:244--263, April 1986.

Digital Library

[6]

Jeremy Condit, Matthew Harren, Zachary Anderson, David Gay, and George C. Necula. Dependent types for low-level programming. In Proc. of the 16th European Symp. on Programming (ESOP), Braga, Portugal, March--April 2007.

Digital Library

[7]

Nathan Cooprider, William Archer, Eric Eide, David Gay, and John Regehr. Efficient memory safety for TinyOS. In Proc. of the 5th ACM Conf. on Embedded Networked Sensor Systems (SenSys), pages 205--218, Sydney, Australia, November 2007.

Digital Library

[8]

David Gay, Phil Levis, Robert von Behren, Matt Welsh, Eric Brewer, and David Culler. The nesC language: A holistic approach to networked embedded systems. In Proc. of the ACM SIGPLAN 2003 Conf. on Programming Language Design and Implementation (PLDI), pages 1--11, San Diego, CA, June 2003.

Digital Library

[9]

Omprakash Gnawali, Rodrigo Fonseca, Kyle Jamieson, David Moss, and Philip Levis. Collection tree protocol. In Proc. of the 7th ACM Conference on Embedded Networked Sensor Systems (SenSys), Berkeley, CA, USA, November 2009.

Digital Library

[10]

Patrice Godefroid. Model checking for programming languages using Verisoft. In Proc. of the Symp. on Principles of Programming Languages, pages 174--186, Nice, France, January 1997.

Digital Library

[11]

Ben Greenstein and Philip Levis. TinyOS Extension Proposal (TEP) 113: Serial Communication, 2006. http://www.tinyos.net/tinyos-2.x/doc/html/tep113.html.

[12]

Alex Groce and Rajeev Joshi. Random testing and model checking: Building a common framework for nondeterministic exploration. In Proc. of the 6th Intl. Workshop on Dynamic Analysis (WODA), Seattle, WA, USA, July 2008.

Digital Library

[13]

Lin Gu and John A. Stankovic. t-kernel: Providing reliable OS support to wireless sensor networks. In Proc. of the 4th ACM Conf. on Embedded Networked Sensor Systems (SenSys), Boulder, CO, November 2006.

Digital Library

[14]

Klaus Havelund and Thomas Pressburger. Model checking Java programs using Java PathFinder. Intl. Journal on Software Tools for Technology Transfer, 2(4), March 2000.

[15]

Jason Hill, Robert Szewczyk, Alec Woo, Seth Hollar, David Culler, and Kristofer Pister. System architecture directions for networked sensors. In Proc. of the 9th Intl. Conf. on Architectural Support for Programming Languages and Operating Systems (ASPLOS), pages 93--104, Cambridge, MA, November 2000.

Digital Library

[16]

Mohammad Maifi Khan, Tarek Abdelzaher, and Kamal Kant Gupta. Towards diagnostic simulation in sensor networks. In Proc. of the Intl. Conf. on Distributed Computing in Sensor Systems (DCOSS), Santorini Island, Greece, June 2008.

Digital Library

[17]

Mohammad Maifi Khan, Hieu Khac Le, Hossein Ahmadi, Tarek F. Abdelzaher, and Jiawei Han. Dustminer: Troubleshooting interactive complexity bugs in sensor networks. In Proc. of the 6th ACM Conf. on Embedded Networked Sensor Systems (SenSys), Raleigh, NC, USA, November 2008.

Digital Library

[18]

Charles Killian, James W. Anderson, Ranjit Jhala, and Amin Vahdat. Life, death, and the critical transition: Detecting liveness bugs in systems code. In Proc. of the 4th Symp. on Networked Systems Design and Implementation (NSDI), Cambridge, MA, April 2007.

Digital Library

[19]

Nupur Kothari, Todd Millstein, and Ramesh Govindan. Deriving state machines from TinyOS programs using symbolic execution. In Proc. of the 7th Intl. Conf. on Information Processing in Sensor Networks (IPSN 2008), St. Louis, MO, 2008.

Digital Library

[20]

Veljko Krunic, Eric Trumpler, and Richard Han. NodeMD: Diagnosing node-level faults in remote wireless sensor systems. In Proc. of the 5th International Conference on Mobile Systems, Applications, and Services (Mobisys), San Juan, Puerto Rico, June 2007.

Digital Library

[21]

Ram Kumar, Eddie Kohler, and Mani Srivastava. Harbor: software-based memory protection for sensor nodes. In Proc. of the 6th Intl. Conf. on Information Processing in Sensor Networks (IPSN07), Cambridge, MA, USA, 2007.

Digital Library

[22]

Philip Levis, Nelson Lee, Matt Welsh, and David Culler. TOSSIM: Accurate and scalable simulation of entire TinyOS applications. In Proc. of the 1st ACM Conf. on Embedded Networked Sensor Systems (SenSys), pages 126--137, Los Angeles, CA, November 2003.

Digital Library

[23]

Kaisen Lin and Philip Levis. Data discovery and dissemination with DIP. In Proc. of the 7th Intl. Conf. on Information Processing in Sensor Networks (IPSN08), pages 433--444, St. Louis, MO, USA, April 2008.

Digital Library

[24]

Liqian Luo, Tian He, Gang Zhou, Lin Gu, Tarek F. Abdelzaher, and John A. Stankovic. Achieving repeatability of asynchronous events in wireless sensor networks with EnviroLog. In Proc. of the 25th Conf. on Computer Communications (INFOCOM), Barcelona, Spain, April 2006.

[25]

Moteiv. Telos rev. B datasheet, 2005. http://www.moteiv.com.

[26]

Nguyet T. M. Nguyen and Mary Lou Soffa. Program representations for testing wireless sensor network applications. In Proc. of the Workshop on Domain Specific Approaches to Software Test Automation (DoSTA'07), Dubrovnik, Croatia, 2007.

Digital Library

[27]

Raimondas Sasnauskas, Olaf Landsiedel, Muhammad Hamad Alizai, Carsten Weise, Stefan Kowalewski, and Klaus Wehrle. KleeNet: Discovering insidious interaction bugs in wireless sensor networks before deployment. In Proc. of the 9th ACM/IEEE International Conference on Information Processing in Sensor Networks (IPSN), Stockholm, Sweden, April 2010.

Digital Library

[28]

Bastian Schlich. Model Checking of Software for Microcontrollers. Dissertation, RWTH Aachen University, Aachen, Germany, June 2008.

[29]

Geoff Werner-Allen, Konrad Lorincz, Jeff Johnson, Jonathan Lees, and Matt Welsh. Fidelity and yield in a volcano monitoring sensor network. In Proc. of the 7th USENIX Symp. on Operating Systems Design and Implementation (OSDI), Berkeley, CA, USA, November 2006.

Digital Library

[30]

Andreas Zeller and Ralf Hildebrandt. Simplifying and isolating failure-inducing input. IEEE Transactions on Software Engineering, 28(2):183--200, February 2002.

Digital Library

Cited By

Al-Bataineh OMoonen LVidziunas L(2024)Extending the range of bugs that automated program repair can handleJournal of Systems and Software10.1016/j.jss.2023.111918209(111918)Online publication date: Mar-2024
https://doi.org/10.1016/j.jss.2023.111918
Vu MXu LElbaum SSun WQiao K(2022)Efficient Protocol Testing Under Temporal Uncertain Event Using Discrete-event Network SimulationsACM Transactions on Modeling and Computer Simulation10.1145/349002832:2(1-30)Online publication date: 4-Mar-2022
https://dl.acm.org/doi/10.1145/3490028
Al-Bataineh OMoonen L(2022)Towards Extending the Range of Bugs That Automated Program Repair Can Handle2022 IEEE 22nd International Conference on Software Quality, Reliability and Security (QRS)10.1109/QRS57517.2022.00031(209-220)Online publication date: Dec-2022
https://doi.org/10.1109/QRS57517.2022.00031
Show More Cited By

Index Terms

T-check: bug finding for sensor networks

Recommendations

Software verification for TinyOS
IPSN '10: Proceedings of the 9th ACM/IEEE International Conference on Information Processing in Sensor Networks

We describe the first software tool for the verification of TinyOS 2, MSP430 applications at compile-time. Given assertions upon the state of the sensor node, the tool boundedly explores all program executions and returns to the programmer an error ...
Lifetime analysis of a sensor network with hybrid automata modelling
WSNA '02: Proceedings of the 1st ACM international workshop on Wireless sensor networks and applications

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. ...
TinyPK: securing sensor networks with public key technology
SASN '04: Proceedings of the 2nd ACM workshop on Security of ad hoc and sensor networks

Wireless networks of miniaturized, low-power sensor/actuator devices are poised to become widely used in commercial and military environments. The communication security problems for these networks are exacerbated by the limited power and energy of the ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

IPSN '10: Proceedings of the 9th ACM/IEEE International Conference on Information Processing in Sensor Networks

April 2010

460 pages

ISBN:9781605589886

DOI:10.1145/1791212

Conference Chairs:
Tarek Abdelzaher
UIUC
,
Thiemo Voigt
SICS
,
Adam Wolisz
TU Berlin

Copyright © 2010 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

IEEE-SPS: Signal Processing Society
SIGBED: ACM Special Interest Group on Embedded Systems

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 12 April 2010

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

National Science Foundation

Conference

IPSN '10

Sponsor:

IEEE-SPS
SIGBED

IPSN '10: The 9th International Conference on Information Processing in Sensor Networks

April 12 - 16, 2010

Stockholm, Sweden

Acceptance Rates

Overall Acceptance Rate 143 of 593 submissions, 24%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

73
Total Citations
View Citations
425
Total Downloads

Downloads (Last 12 months)7
Downloads (Last 6 weeks)0

Reflects downloads up to 19 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Al-Bataineh OMoonen LVidziunas L(2024)Extending the range of bugs that automated program repair can handleJournal of Systems and Software10.1016/j.jss.2023.111918209(111918)Online publication date: Mar-2024
https://doi.org/10.1016/j.jss.2023.111918
Vu MXu LElbaum SSun WQiao K(2022)Efficient Protocol Testing Under Temporal Uncertain Event Using Discrete-event Network SimulationsACM Transactions on Modeling and Computer Simulation10.1145/349002832:2(1-30)Online publication date: 4-Mar-2022
https://dl.acm.org/doi/10.1145/3490028
Al-Bataineh OMoonen L(2022)Towards Extending the Range of Bugs That Automated Program Repair Can Handle2022 IEEE 22nd International Conference on Software Quality, Reliability and Security (QRS)10.1109/QRS57517.2022.00031(209-220)Online publication date: Dec-2022
https://doi.org/10.1109/QRS57517.2022.00031
Germiniani SDanese APravadelli G(2020)Automatic generation of assertions for detection of firmware vulnerabilities through alignment of symbolic sequencesIEEE Transactions on Emerging Topics in Computing10.1109/TETC.2020.3035187(1-1)Online publication date: 2020
https://doi.org/10.1109/TETC.2020.3035187
Vu MXu LElbaum SSun WQia K(2019)Efficient systematic testing of network protocols with temporal uncertain eventsIEEE INFOCOM 2019 - IEEE Conference on Computer Communications10.1109/INFOCOM.2019.8737390(604-612)Online publication date: Apr-2019
https://doi.org/10.1109/INFOCOM.2019.8737390
Mehmood AAlrajeh NMukherjee MAbdullah SSong H(2018)A Survey on Proactive, Active and Passive Fault Diagnosis Protocols for WSNs: Network Operation PerspectiveSensors10.3390/s1806178718:6(1787)Online publication date: 1-Jun-2018
https://doi.org/10.3390/s18061787
Danese ABertacco VPravadelli G(2018)Symbolic assertion mining for security validation2018 Design, Automation & Test in Europe Conference & Exhibition (DATE)10.23919/DATE.2018.8342262(1550-1555)Online publication date: Mar-2018
https://doi.org/10.23919/DATE.2018.8342262
Afanasov MMottola LGhezzi C(2018)Software Adaptation in Wireless Sensor NetworksACM Transactions on Autonomous and Adaptive Systems10.1145/314545312:4(1-29)Online publication date: 23-Jan-2018
https://dl.acm.org/doi/10.1145/3145453
Iwanicki K(2018)A Distributed Systems Perspective on Industrial IoT2018 IEEE 38th International Conference on Distributed Computing Systems (ICDCS)10.1109/ICDCS.2018.00116(1164-1170)Online publication date: Jul-2018
https://doi.org/10.1109/ICDCS.2018.00116
Grichi HMosbahi OKhalgui MLi Z(2017)RWiN: New Methodology for the Development of Reconfigurable WSNIEEE Transactions on Automation Science and Engineering10.1109/TASE.2016.260891814:1(109-125)Online publication date: Jan-2017
https://doi.org/10.1109/TASE.2016.2608918
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents