Skip to main content
SpringerLink
Log in

Analyzing Real-Time Event-Driven Programs

  • Conference paper
Formal Modeling and Analysis of Timed Systems (FORMATS 2009)

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

Abstract

Embedded real-time systems are typically programmed in low-level languages which provide support for event-driven task processing and real-time interrupts. We show that the model checking problem for real-time event-driven Boolean programs for safety properties is undecidable. In contrast, the model checking problem is decidable for languages such as Giotto which statically limit the creation of tasks. This gives a technical reason (static analyzability) to prefer higher-level programming models for real-time programming, in addition to the usual readability and maintainability arguments.

This research was sponsored by the NSF grants CCF-0546170, CCF-0702743, and CNS-0720881.

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 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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Aho, A., Sethi, R., Ullman, J.: Compilers: Principles, Techniques, and Tools. Addison-Wesley, Reading (1986)

    MATH  Google Scholar 

  2. Atig, M.F., Bouajjani, A., Touili, T.: Analyzing asynchronous programs with preemption. In: FSTTCS 2008: Proc. 28th Int. Conf. on Fondation of Software Technology and Theoretical Computer Science (2008)

    Google Scholar 

  3. Ganty, P., Majumdar, R., Rybalchenko, A.: Verifying liveness for asynchronous programs. In: POPL 2009: Proc. 36th ACM SIGACT-SIGPLAN Symp. on Principles of Programming Languages, pp. 102–113. ACM Press, New York (2009)

    Google Scholar 

  4. Ghosal, A., Henzinger, T.A., Kirsch, C.M., Sanvido, M.A.A.: Event-driven programming with logical execution times. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 357–371. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  5. Henzinger, T.A., Horowitz, B., Kirsch, C.M.: Giotto: A time-triggered language for embedded programming. In: Henzinger, T.A., Kirsch, C.M. (eds.) EMSOFT 2001. LNCS, vol. 2211, pp. 166–184. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  6. Henzinger, T.A., Kirsch, C.M.: The embedded machine: predictable, portable real-time code. In: PLDI 2002: Proc. 23rd Conf. on Programming Language Design and Implementation, pp. 315–326. ACM Press, New York (2002)

    Google Scholar 

  7. Henzinger, T.A., Kirsch, C.M., Majumdar, R., Matic, S.: Time safety checking for embedded programs. In: Sangiovanni-Vincentelli, A.L., Sifakis, J. (eds.) EMSOFT 2002. LNCS, vol. 2491, pp. 76–92. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  8. Jhala, R., Majumdar, R.: Interprocedural analysis of asynchronous programs. In: POPL 2007: Proc. 34th ACM SIGACT-SIGPLAN Symp. on Principles of Programming Languages, pp. 339–350. ACM Press, New York (2007)

    Google Scholar 

  9. Libevent, http://www.monkey.org/~provos/libevent/

  10. Minsky, M.: Finite and Infinite Machines. Prentice-Hall, Englewood Cliffs (1967)

    MATH  Google Scholar 

  11. Mitchell, J.: Foundations for Programming Languages. MIT Press, Cambridge (1996)

    Google Scholar 

  12. Sen, K., Viswanathan, M.: Model checking multithreaded programs with asynchronous atomic methods. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 300–314. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  13. Titzer, B.L.: Virgil: objects on the head of a pin. In: OOPSLA 2006: Proc. 21st ACM-SIGPLAN conference on Object-oriented programming systems, languages, and applications, pp. 191–208. ACM Press, New York (2006)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. CS Department, University of California, Los Angeles, CA, USA

    Pierre Ganty

  2. IMDEA Software, Spain

    Pierre Ganty & Rupak Majumdar

Authors
  1. Pierre Ganty
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Rupak Majumdar
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Computing Laboratory, Oxford University, Wolfson Building, Parks Road, OX1 3QD, Oxford, UK

    Joël Ouaknine

  2. Institute for Computing and Information Sciences , Radboud University Nijmegen , P.O. Box 9010, 6500, Nijmegen, GL, The Netherlands

    Frits W. Vaandrager

Rights and permissions

Reprints and permissions

Copyright information

© 2009 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Ganty, P., Majumdar, R. (2009). Analyzing Real-Time Event-Driven Programs. In: Ouaknine, J., Vaandrager, F.W. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2009. Lecture Notes in Computer Science, vol 5813. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-04368-0_14

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-04368-0_14

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-04367-3

  • Online ISBN: 978-3-642-04368-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation