Skip to main content
SpringerLink
Log in

Analyzing Interrupt Handlers via Interprocedural Summaries

  • Chapter
  • First Online:
Symposium on Real-Time and Hybrid Systems

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 11180))

  • 451 Accesses

Abstract

Interrupts are a commonly used facility to guarantee real-time response in embedded systems, and thus are frequently encountered in embedded software. Modeling interrupt preemption as function calls, is a natural choice for analyzing or verifying programs involving interrupts. Therefore, interprocedural analysis of interrupt handlers is highly desired when analyzing programs with interrupts. In this paper, we present two interprocedural analysis approaches specifically for analyzing interrupt handlers. One is based on tabulation of procedure summaries, while the other is based on procedure summaries that are built by partitioning inputs. These two approaches fit for interrupt handlers with different features. Finally, we show preliminary experimental results obtained by our prototype implementation.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. https://en.wikipedia.org/wiki/MIL-STD-1553

  2. https://en.wikipedia.org/wiki/CAN_bus

  3. Bourdoncle, F.: Interprocedural abstract interpretation of block structured languages with nested procedures, aliasing and recursivity. In: Deransart, P., Maluszyński, J. (eds.) PLILP 1990. LNCS, vol. 456, pp. 307–323. Springer, Heidelberg (1990). https://doi.org/10.1007/BFb0024192

    Chapter  Google Scholar 

  4. Brylow, D., Damgaard, N., Palsberg, J.: Static checking of interrupt-driven software. In: ICSE 2001, pp. 47–56. IEEE (2001)

    Google Scholar 

  5. Chen, J., Cousot, P.: A binary decision tree abstract domain functor. In: Blazy, S., Jensen, T. (eds.) SAS 2015. LNCS, vol. 9291, pp. 36–53. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-48288-9_3

    Chapter  Google Scholar 

  6. Cousot, P., Cousot, R.: Static determination of dynamic properties of recursive procedures. In: IFIP Conference on Formal Description of Programming Concepts, pp. 237–277. North-Holland (1977)

    Google Scholar 

  7. Jeannet, B.: The ConcurInterproc Analyzer. http://pop-art.inrialpes.fr/interproc/concurinterprocweb.cgi

  8. Jeannet, B.: Relational interprocedural verification of concurrent programs. Softw. Syst. Model. 12(2), 285–306 (2013)

    Article  Google Scholar 

  9. Jeannet, B.: The fixpoint solver. http://pop-art.inrialpes.fr/~bjeannet/bjeannet-forge/fixpoint/

  10. Jeannet, B., Miné, A.: Apron: a library of numerical abstract domains for static analysis. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 661–667. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02658-4_52

    Chapter  Google Scholar 

  11. Kidd, N., Jagannathan, S., Vitek, J.: One stack to run them all - reducing concurrent analysis to sequential analysis under priority scheduling. In: van de Pol, J., Weber, M. (eds.) SPIN 2010. LNCS, vol. 6349, pp. 245–261. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-16164-3_18

    Chapter  Google Scholar 

  12. Lal, A., Touili, T., Kidd, N., Reps, T.W.: Interprocedural analysis of concurrent programs under a context bound. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 282–298. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_20

  13. Liang, L., Melham, T., Kroening, D., Schrammel, P., Tautschnig, M.: Effective verification for low-level software with competing interrupts. ACM Trans. Embed. Comput. Syst. 17(2), 36:1–36:26 (2017)

    Google Scholar 

  14. Liu, H., Jiang, Y., Zhang, H., Gu, M., Sun, J.: Taming interrupts for verifying industrial multifunction vehicle bus controllers. In: Fitzgerald, J., Heitmeyer, C., Gnesi, S., Philippou, A. (eds.) FM 2016. LNCS, vol. 9995, pp. 764–771. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-48989-6_48

    Chapter  Google Scholar 

  15. Mangal, R., Naik, M., Yang, H.: A Correspondence between two approaches to interprocedural analysis in the presence of join. In: Shao, Z. (ed.) ESOP 2014. LNCS, vol. 8410, pp. 513–533. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54833-8_27

    Chapter  Google Scholar 

  16. Monniaux, D.: Verification of device drivers and intelligent controllers: a case study. In: EMSOFT 2007, pp. 30–36. ACM (2007)

    Google Scholar 

  17. Necula, G.C., McPeak, S., Rahul, S.P., Weimer, W.: CIL: intermediate language and tools for analysis and transformation of C programs. In: Horspool, R.N. (ed.) CC 2002. LNCS, vol. 2304, pp. 213–228. Springer, Heidelberg (2002). https://doi.org/10.1007/3-540-45937-5_16

    Chapter  Google Scholar 

  18. Ouadjaout, A., Miné, A., Lasla, N., Badache, N.: Static analysis by abstract interpretation of functional properties of device drivers in TinyOS. J. Syst. Softw. 120, 114–132 (2016)

    Article  Google Scholar 

  19. Qadeer, S., Rajamani, S.K., Rehof, J.: Summarizing procedures in concurrent programs. In: POPL 2004, pp. 245–255. ACM (2004)

    Google Scholar 

  20. Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 93–107. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-31980-1_7

    Chapter  MATH  Google Scholar 

  21. Ramalingam, G.: Context-sensitive synchronization-sensitive analysis is undecidable. ACM Trans. Program. Lang. Syst. 22(2), 416–430 (2000)

    Article  Google Scholar 

  22. Reps, T.W., Horwitz, S., Sagiv, S.: Precise interprocedural dataflow analysis via graph reachability. In: POPL 1995, pp. 49–61. ACM Press (1995)

    Google Scholar 

  23. Schwarz, M.D., Seidl, H., Vojdani, V., Lammich, P., Müller-Olm, M.: Static analysis of interrupt-driven programs synchronized via the priority ceiling protocol. In: POPL 2011, pp. 93–104. ACM (2011)

    Google Scholar 

  24. Sharir, M., Pnueli, A.: Two approaches to interprocedural data flow analysis. In: Program Flow Analysis: Theory and Applications, Chapter 7, pp. 189–233. Prentice-Hall (1981)

    Google Scholar 

  25. Sung, C., Kusano, M., Wang, C.: Modular verification of interrupt-driven software. In: ASE 2017, pp. 206–216. IEEE Computer Society (2017)

    Google Scholar 

  26. Vörtler, T., Höckner, B., Hofstedt, P., Klotz, T.: Formal verification of software for the Contiki operating system considering interrupts. In: DDECS 2015, pp. 295–298. IEEE Computer Society (2015)

    Google Scholar 

  27. Wang, Y., Shi, J., Wang, L., Zhao, J., Li, X.: Detecting data races in interrupt-driven programs based on static analysis and dynamic simulation. In: Internetware 2015, pp. 199–202. ACM (2015)

    Google Scholar 

  28. Wang, Y, Wang, L., Yu, T., Zhao, J., Li, X.: Automatic detection and validation of race conditions in interrupt-driven embedded software. In: ISSTA 2017, pp. 113–124. ACM (2017)

    Google Scholar 

  29. Wu, X., Chen, L., Miné, A., Dong, W., Wang, J.: Numerical static analysis of interrupt-driven programs via sequentialization. In: EMSOFT 2015, pp. 55–64. IEEE Press (2015)

    Google Scholar 

  30. Wu, X., Chen, L., Miné, A., Dong, W., Wang, J.: Static analysis of runtime errors in interrupt-driven programs via sequentialization. ACM Trans. Embed. Comput. Syst. 15(4), 70 (2016)

    Google Scholar 

  31. Wu, X., Wen, Y., Chen, L., Dong, W., Wang, J.: Data race detection for interrupt-driven programs via bounded model checking. In: SERE 2013 (Companion), pp. 204–210. IEEE (2013)

    Google Scholar 

Download references

Acknowledgments

We thank Antoine Miné for his helpful discussions on this work. This work is supported by the National Key R&D Program of China (No. 2017YFB1001802), and the NSFC Program (Nos. 61872445, 61532007).

Author information

Authors and Affiliations

  1. State Key Laboratory of High Performance Computing, Changsha, China

    Ji Wang

  2. School of Computer, National University of Defense Technology, Changsha, China

    Xueguang Wu, Liqian Chen & Ji Wang

Authors
  1. Xueguang Wu
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Liqian Chen
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Ji Wang
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Liqian Chen .

Editor information

Editors and Affiliations

  1. Newcastle University, Newcastle, UK

    Cliff Jones

  2. National University of Defense Technology, Changsha, China

    Ji Wang

  3. Institute of Software, CAS, Beijing, China

    Naijun Zhan

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Wu, X., Chen, L., Wang, J. (2018). Analyzing Interrupt Handlers via Interprocedural Summaries. In: Jones, C., Wang, J., Zhan, N. (eds) Symposium on Real-Time and Hybrid Systems. Lecture Notes in Computer Science(), vol 11180. Springer, Cham. https://doi.org/10.1007/978-3-030-01461-2_13

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-01461-2_13

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-01460-5

  • Online ISBN: 978-3-030-01461-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation