Interface contracts for TinyOS

ABSTRACT

TinyOS applications are built with software components that communicate through narrow interfaces. Since components enable fine-grained code reuse, this approach has been successful in creating applications that make very efficient use of the limited code and data memory on sensor network nodes. However, the other important benefit of components---rapid application development through black-box reuse---remains largely unrealized because in many cases interfaces have implied usage constraints that can be the source of frustrating program errors. Developers are commonly forced to read the source code for components, partially defeating the purpose of using components in the first place. Our research helps solve these problems by allowing developers to explicitly specify and enforce component interface contracts. Due to the extensive reuse of the most common interfaces, implementing contracts for a small number of frequently reused interfaces permitted us to extensively check a number of applications. We uncovered some subtle and previously unknown bugs in applications that have been in common use for years.

REFERENCES

• 1: Cristian Cadar , Vijay Ganesh , Peter M. Pawlowski , David L. Dill , Dawson R. Engler, EXE: automatically generating inputs of death, Proceedings of the 13th ACM conference on Computer and communications security, October 30-November 03, 2006, Alexandria, Virginia, USA [doi>10.1145/1180405.1180445]
• 2: Arindam Chakrabarti , Luca de Alfaro , Thomas A. Henzinger , Marcin Jurdzinski , Freddy Y. C. Mang, Interface Compatibility Checking for Software Modules, Proceedings of the 14th International Conference on Computer Aided Verification, p.428-441, July 27-31, 2002
• 3: Nathan Cooprider , John Regehr, Pluggable abstract domains for analyzing embedded software, Proceedings of the 2006 ACM SIGPLAN/SIGBED conference on Language, compilers, and tool support for embedded systems, June 14-16, 2006, Ottawa, Ontario, Canada
• 4: David Gay , Philip Levis , Robert von Behren , Matt Welsh , Eric Brewer , David Culler, The nesC language: A holistic approach to networked embedded systems, Proceedings of the ACM SIGPLAN 2003 conference on Programming language design and implementation, June 09-11, 2003, San Diego, California, USA
• 5: Dimitra Giannakopoulou , Corina S. Pasareanu , Jamieson M. Cobleigh, Assume-Guarantee Verification of Source Code with Design-Level Assumptions, Proceedings of the 26th International Conference on Software Engineering, p.211-220, May 23-28, 2004
• 6: Lin Gu , John A. Stankovic, t-kernel: providing reliable OS support to wireless sensor networks, Proceedings of the 4th international conference on Embedded networked sensor systems, October 31-November 03, 2006, Boulder, Colorado, USA [doi>10.1145/1182807.1182809]
• 7: Jason Hill , Robert Szewczyk , Alec Woo , Seth Hollar , David Culler , Kristofer Pister, System architecture directions for networked sensors, Proceedings of the ninth international conference on Architectural support for programming languages and operating systems, p.93-104, November 2000, Cambridge, Massachusetts, United States
• 8: Philip Levis. Amqueue implementation, 2006. http://tinyos.cvs.sourceforge.net/*checkout*/tinyos/tinyos-2.x/tos/system/AMQueueImplP.nc.
• 9: Philip Levis. TinyOS Extension Proposal (TEP) 107: TinyOS 2.x Boot Sequence, 2006. http://tinyos.cvs.sourceforge.net/*checkout*/tinyos/tinyos-2.x/doc/html/tep107.html.
• 10: Philip Levis. TinyOS Extension Proposal (TEP) 116: Packet Protocols, 2006. http://tinyos.cvs.sourceforge.net/*checkout*/tinyos/tinyos-2.x/doc/html/tep116.html.
• 11: Bertrand Meyer, Applying "Design by Contract", Computer, v.25 n.10, p.40-51, October 1992 [doi>10.1109/2.161279]
• 12: George C. Necula , Scott McPeak , Shree Prakash Rahul , Westley Weimer, CIL: Intermediate Language and Tools for Analysis and Transformation of C Programs, Proceedings of the 11th International Conference on Compiler Construction, p.213-228, April 08-12, 2002
• 13: Nithya Ramanathan , Kevin Chang , Rahul Kapur , Lewis Girod , Eddie Kohler , Deborah Estrin, Sympathy for the sensor network debugger, Proceedings of the 3rd international conference on Embedded networked sensor systems, November 02-04, 2005, San Diego, California, USA [doi>10.1145/1098918.1098946]
• 14: John Regehr , Nathan Cooprider , Will Archer , Eric Eide, Efficient type and memory safety for tiny embedded systems, Proceedings of the 3rd workshop on Programming languages and operating systems: linguistic support for modern operating systems, p.6-es, October 22-22, 2006, San Jose, California [doi>10.1145/1215995.1216001]
• 15: Ram Kumar Rengaswamy, Eddie Kohler, and Mani Srivastava. Software-based memory protection in sensor nodes. In Proc. of the 3rd Workshop on Embedded Networked Sensors (EmNets), Cambridge, MA, May 2006.
• 16: Ben L. Titzer, Virgil: objects on the head of a pin, Proceedings of the 21st annual ACM SIGPLAN conference on Object-oriented programming systems, languages, and applications, October 22-26, 2006, Portland, Oregon, USA
• 17: Ben L. Titzer , Daniel K. Lee , Jens Palsberg, Avrora: scalable sensor network simulation with precise timing, Proceedings of the 4th international symposium on Information processing in sensor networks, April 24-27, 2005, Los Angeles, California
• 18: P. Völgyesi , M. Maróti , S. Dóra , E. Osses , Á. Lédeczi, Software composition and verification for sensor networks, Science of Computer Programming, v.56 n.1-2, p.191-210, April 2005 [doi>10.1016/j.scico.2004.11.012]

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Programming by contract

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.5 Testing and Debugging
          Subjects: Testing tools (e.g., data generators, coverage testing)

General Terms:
Design, Reliability, Verification

Keywords:
TinyOS, automated testing, design by contract, sensor networks, validation