Skip to main content
SpringerLink
Log in

On the Modular Integration of Abstract Semantics for WCET Analysis

  • Conference paper
  • First Online:
Foundational and Practical Aspects of Resource Analysis (FOPARA 2013)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 8552))

Abstract

We propose here a modular resource analysis which is constructed around a rewrite-based formal specification of an embedded system. Designing and analyzing embedded systems considers both hardware and software behavioral aspects which we capture using the modular notion of system configuration. Hence, we use a configuration-based design methodology and we instantiate parts of the configuration to accommodate data and control-flow abstractions. These instantiations require no modifications of the original formal specification. We implement in this manner a particular resource analysis, namely worst case execution time (WCET), and evaluate it with respect to a reusability metric.

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 34.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 44.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. AbsInt Angewandte Informatik: aiT Worst-Case Execution Time Analyzers

    Google Scholar 

  2. Asăvoae, M., Asăvoae, I.M., Lucanu, D.: On abstractions for timing analysis in the \(\mathbb{K}\) framework. In: Peña, R., van Eekelen, M., Shkaravska, O. (eds.) FOPARA 2011. LNCS, vol. 7177, pp. 90–107. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  3. Asavoae, M., Lucanu, D., Roşu, G.: Towards semantics-based WCET analysis. In: WCET (2011) (to appear)

    Google Scholar 

  4. Biere, A., Knoop, J., Kovács, L., Zwirchmayr, J.: The auspicious couple: Symbolic execution and WCET analysis. In: WCET, pp. 53–63 (2013)

    Google Scholar 

  5. Blazy, S., Maroneze, A., Pichardie, D.: Formal verification of loop bound estimation for WCET analysis. In: Cohen, E., Rybalchenko, A. (eds.) VSTTE 2013. LNCS, vol. 8164, pp. 281–303. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

  6. Burger, D., Austin, T.M.: The SimpleScalar tool set, version 2.0. SIGARCH Comput. Archit. News 25, 13–25 (1997)

    Article  Google Scholar 

  7. Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C. (eds.): All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007)

    MATH  Google Scholar 

  8. Cousot, P., Cousot, R.: Systematic design of program analysis frameworks. In: POPL, pp. 269–282 (1979)

    Google Scholar 

  9. Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL, pp. 238–252. ACM Press (1977)

    Google Scholar 

  10. Şerbănuţă, T.F., Roşu, G.: K-Maude: a rewriting based tool for semantics of programming languages. In: Ölveczky, P.C. (ed.) WRLA 2010. LNCS, vol. 6381, pp. 104–122. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  11. Cutumisu, M., Onuczko, C., Szafron, D., Schaeffer, J., McNaughton, M., Roy, T., Siegel, J., Carbonaro, M.: Evaluating pattern catalogs: the computer games experience. In: ICSE, pp. 132–141 (2006)

    Google Scholar 

  12. Dams, D.: Comparing abstraction refinement algorithms. ENTCS 89(3), 405–416 (2003)

    Google Scholar 

  13. Gustafsson, J., Betts, A., Ermedahl, A., Lisper, B.: The Mälardalen WCET benchmarks: Past, present and future. In: WCET, pp. 136–146 (2010)

    Google Scholar 

  14. Hammond, K., Ferdinand, C., Heckmann, R., Dyckhoff, R., Hofmann, M., Jost, S., Loidl, H.W., Michaelson, G., Pointon, R.F., Scaife, N., Sérot, J., Wallace, A.: Towards formally verifiable WCET analysis for a functional programming language. In: WCET (2006)

    Google Scholar 

  15. Healy, C.A., Whalley, D.B., Harmon, M.G.: Integrating the timing analysis of pipelining and instruction caching. In: RTSS, pp. 288–297 (1995)

    Google Scholar 

  16. Hills, M., Roşu, G.: Towards a module system for K. In: Corradini, A., Montanari, U. (eds.) WADT 2008. LNCS, vol. 5486, pp. 187–205. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  17. Leroy, X.: Formal verification of a realistic compiler. CACM 52(7), 107–115 (2009)

    Article  Google Scholar 

  18. Li, X., Mitra, T., Roychoudhury, A.: Accurate timing analysis by modeling caches, speculation and their interaction. In: DAC, pp. 466–471 (2003)

    Google Scholar 

  19. Li, Y.T.S., Malik, S.: Performance analysis of embedded software using implicit path enumeration. In: DAC, pp. 456–461 (1995)

    Google Scholar 

  20. Li, Y.T.S., Malik, S., Wolfe, A.: Efficient microarchitecture modeling and path analysis for real-time software. In: IEEE RTSS, pp. 298–307 (1995)

    Google Scholar 

  21. Meseguer, J.: Twenty years of rewriting logic. J. Log. Algebr. Program. 81(7–8), 721–781 (2012)

    Article  MathSciNet  MATH  Google Scholar 

  22. Moore, R.E., Kearfott, R.B., Cloud, M.J.: Introduction to Interval Analysis. SIAM, Philadelphia (2009)

    Book  MATH  Google Scholar 

  23. Reineke, J., Grund, D., Berg, C., Wilhelm, R.: Timing predictability of cache replacement policies. Real-Time Syst. 37(2), 99–122 (2007)

    Article  MATH  Google Scholar 

  24. Roşu, G., Şerbănuţă, T.F.: An overview of the K semantic framework. J. Logic Algebraic Program. 79(6), 397–434 (2010)

    Article  MATH  Google Scholar 

  25. Theiling, H., Ferdinand, C., Wilhelm, R.: Fast and precise WCET prediction by separated cache and path analyses. Real-Time Syst. 18(2/3), 157–179 (2000)

    Article  Google Scholar 

  26. Wilhelm, R.: Why AI + ILP is good for WCET, but MC is Not, Nor ILP alone. In: Steffen, B., Levi, G. (eds.) VMCAI 2004. LNCS, vol. 2937, pp. 309–322. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  27. Wilhelm, R., Engblom, J., Ermedahl, A., Holsti, N., Thesing, S., Whalley, D., Bernat, G., Ferdinand, C., Heckmann, R., Mitra, T., Mueller, F., Puaut, I., Puschner, P., Staschulat, J., Stenström, P.: The worst-case execution-time problem–overview of methods and survey of tools. TECS 7(3), 1–53 (2008)

    Article  Google Scholar 

  28. Wilhelm, R., Wachter, B.: Abstract interpretation with applications to timing validation. In: Gupta, A., Malik, S. (eds.) CAV 2008. LNCS, vol. 5123, pp. 22–36. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

Download references

Acknowledgments

We thank very much to the anonymous reviewers for their comments and suggestions which helped us to focus and improve our work in this paper.

Author information

Authors and Affiliations

  1. VERIMAG/UJF, Gières, France

    Mihail Asăvoae & Irina Măriuca Asăvoae

Authors
  1. Mihail Asăvoae
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Irina Măriuca Asăvoae
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Mihail Asăvoae .

Editor information

Editors and Affiliations

  1. Università di Bologna, Bologna, Italy

    Ugo Dal Lago

  2. Universidad Complutense de Madrid, Madrid, Spain

    Ricardo Peña

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer International Publishing Switzerland

About this paper

Cite this paper

Asăvoae, M., Asăvoae, I.M. (2014). On the Modular Integration of Abstract Semantics for WCET Analysis. In: Dal Lago, U., Peña, R. (eds) Foundational and Practical Aspects of Resource Analysis. FOPARA 2013. Lecture Notes in Computer Science(), vol 8552. Springer, Cham. https://doi.org/10.1007/978-3-319-12466-7_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-12466-7_2

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-12465-0

  • Online ISBN: 978-3-319-12466-7

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation