Lazy preemption to enable path-based analysis of interrupt-driven code

ABSTRACT

One of the important factors in ensuring the correct functionality of wireless sensor networks (WSNs) is the reliability of the software running on individual sensor nodes. Research has shown that path-sensitive static analysis is effective for bug detection and fault diagnosis; however, path-sensitive analysis is prohibitively expensive when applied to a WSN application due to the large state space caused by arbitrary interrupt preemptions. In this paper, we propose a new execution model called lazy preemption that reduces this state space by restricting interrupt handlers to a set of predetermined preemption points, if possible. This execution model allows us to represent the program with an inter-interrupt control flow graph (IICFG), which is easier to analyze than the original CFGs with arbitrary interrupt preemptions.

References

1. P. Ballarini and A. Miller. Model Checking Medium Access Control for Sensor Networks. In ISoLA '06, 2006.
2. D. Brylow, N. Damgaard, and J. Palsberg. Static Checking of Interrupt-Driven Software. In ICSE '01, 2001.
3. N. Cooprider, W. Archer, E. Eide, D. Gay, and J. Regehr. Efficient Memory Safety for TinyOS. In SenSys '07, 2007.
4. C. Killian, J. Anderson, R. Jhala, and A. Vahdat. Life, Death, and the Critical Transition: Finding Liveness Bugs in Systems Code. In NSDI '07, 2007.
5. Z. Lai, S. Cheung, and W. Chan. Inter-Context Control-Flow and Data-Flow Test Adequacy Criteria for nesC Applications. In FSE '08, 2008.
6. W. Le and M. L. Soffa. Marple: A Demand-Driven Path-Sensitive Buffer Overflow Detector. In FSE '08, 2008.
7. W. Le and M. L. Soffa. Path-Based Fault Correlation. In FSE '10, 2010.
8. P. Li and J. Regehr. T-Check: Bug Finding for Sensor Networks. In IPSN '10, 2010.
9. L. Mottola, T. Voigt, F. Osterlind, J. Eriksson, L. Baresi, and C. Ghezzi. Anquiro: Enabling Efficient Static Verification of Sensor Network Software. In SESENA '10, 2010.
10. J. Regehr. Random Testing of Interrupt-Driven Software. In EMSOFT '05, 2005.
11. J. Regehr, A. Reid, and K. Webb. Eliminating Stack Overflow by Abstract Interpretation. ACM Trans. Embed. Comput. Syst., 4(4), 2005.
12. B. Schlich. Model Checking of Software for Microcontrollers. ACM Trans. Embed. Comput. Syst., 9(4), 2010.
13. J. Yang, M. L. Soffa, L. Selavo, and K. Whitehouse. Clairvoyant: A Comprehensive Source-Level Debugger for Wireless Sensor Networks. In SenSys '07, 2007.

Index Terms

• General and reference

  • Cross-computing tools and techniques

    • Reliability

• Software and its engineering

  • Software organization and properties

    • Extra-functional properties

      • Software reliability