Skip to main content
SpringerLink
Log in
Book cover

Models, Algorithms, Logics and Tools pp 560–577Cite as

WUPPAAL: Computation of Worst-Case Execution-Time for Binary Programs with UPPAAL

  • Chapter
  • First Online:

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

Abstract

We address the problem of computing the worst-case execution-time (WCET) of binary programs using a real-time model-checker. In our previous work, we introduced a fully automated and modular methodology to build a model (network of timed automata) that combined a binary program and the hardware to run the program on. Computing the WCET amounts to finding the longest path time-wise in this model, which can be done using a real-time model checker like Uppaal.

In this work, we generalise the previous approach and we define a generic framework to support arbitrary binary language and hardware.

We have implemented our new approach in an extended version of Uppaal, called Wuppaal. Experimental results using some standard benchmarks suite for WCET computation (from Mälardalen University) show that our technique is practical and promising.

P.G. Jensen—Part of this work was done while this author visited Macquarie University.

This is a preview of subscription content, 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

Learn about institutional subscriptions

Notes

  1. 1.

    An exact test for this assumption does not exist as this problem is undecidable.

References

  1. AbsInt Angewandte Informatik: aiT Worst-Case Execution Time Analyzers. http://www.absint.com/ait/

  2. Alur, R., Dill, D.: A theory of timed automata. TCS 126(2), 183–235 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  3. Behrmann, G., David, A., Larsen, K.G., Håkansson, J., Pettersson, P., Yi, W., Hendriks, M.: Uppaal 4.0. In: QEST, pp. 125–126. IEEE Computer Society (2006)

    Google Scholar 

  4. Bellard, F.: QEMU, a fast and portable dynamic translator. In: Proceedings of the Annual Conference on USENIX Annual Technical Conference, ATEC 2005, p. 41. USENIX Association, Berkeley (2005). http://dl.acm.org/citation.cfm?id=1247360.1247401

  5. Bernat, G., Colin, A., Petters, S.M.: pWCET a toolset for automatic worst-case execution time analysis of real-time embedded programs. In: Proceedings of the 3rd International Workshop on WCET Analysis, Workshop of the Euromicro Conference on Real-Time Systems, Porto, Portugal (2003)

    Google Scholar 

  6. Cassez, F.: Timed games for computing worst-case execution-times. Research report, National ICT Australia, 31 p., June 2010. http://arxiv.org/abs/1006.1951

  7. Cassez, F.: Timed games for computing WCET for pipelined processors with caches. In: ACSD 2011, pp. 195–204. IEEE Computer Society, June 2011

    Google Scholar 

  8. Cassez, F., de Aledo Marugán, P.G.: Timed automata for modelling caches and pipelines. In: van Glabbeek, R.J., Groote, J.F., Höfner, P. (eds.) Proceedings Workshop on Models for Formal Analysis of Real Systems, MARS 2015, Suva, Fiji, 23 November 2015. EPTCS, vol. 196, pp. 37–45 (2015)

    Google Scholar 

  9. Cassez, F., Béchennec, J.: Timing analysis of binary programs with UPPAAL. In: 13th International Conference on Application of Concurrency to System Design, ACSD 2013, pp. 41–50. IEEE Computer Society, July 2013

    Google Scholar 

  10. Cassez, F., Hansen, R.R., Olesen, M.C.: What is a timing anomaly? In: 12th International Workshop on Worst-Case Execution Time Analysis, WCET 2012, 10 July 2012, Pisa, Italy. OASICS, vol. 23, pp. 1–12. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, July 2012

    Google Scholar 

  11. Dalsgaard, A.E., Olesen, M.C., Toft, M., Hansen, R.R., Larsen, K.G.: Metamoc: modular execution time analysis using model checking. In: Lisper, B. (ed.) WCET. OASICS, vol. 15, pp. 113–123. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, Germany (2010)

    Google Scholar 

  12. Dalsgaard, A.E., Olesen, M.C., Toft, M.: Modular execution time analysis using model checking. Master’s thesis, Department of Computer Science, Aalborg University, Denmark (2009)

    Google Scholar 

  13. Ferdinand, C., Heckmann, R., Wilhelm, R.: Analyzing the worst-case execution time by abstract interpretation of executable code. In: Broy, M., Krüger, I.H., Meisinger, M. (eds.) ASWSD 2004. LNCS, vol. 4147, pp. 1–14. Springer, Heidelberg (2006). doi:10.1007/11823063_1

    Chapter  Google Scholar 

  14. Heizmann, M., Hoenicke, J., Podelski, A.: Refinement of trace abstraction. In: Palsberg, J., Su, Z. (eds.) SAS 2009. LNCS, vol. 5673, pp. 69–85. Springer, Heidelberg (2009). doi:10.1007/978-3-642-03237-0_7

    Chapter  Google Scholar 

  15. Heizmann, M., Hoenicke, J., Podelski, A.: Software model checking for people who love automata. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 36–52. Springer, Heidelberg (2013). doi:10.1007/978-3-642-39799-8_2

    Chapter  Google Scholar 

  16. Larsen, K.G., Pettersson, P., Yi, W.: Uppaal in a nutshell. J. Softw. Tools Technol. Transf. (STTT) 1(1–2), 134–152 (1997)

    Article  MATH  Google Scholar 

  17. Mälardalen WCET Research Group: WCET Project - Benchmarks. http://www.mrtc.mdh.se/projects/wcet/benchmarks.html

  18. Rapita Systems Ltd. Rapita Systems for timing analysis of real-time embedded systems. http://www.rapitasystems.com/

  19. Rieder, B., Puschner, P., Wenzel, I.: Using model checking to derive loop bounds of general loops within ANSI-C applications for measurement based WCET analysis. In: 6th International Workshop on Intelligent Solutions in Embedded Systems (WISES 2008), Regensburg, Germany (2008)

    Google Scholar 

  20. Sloane, A.M.: Lightweight language processing in Kiama. In: Fernandes, J.M., Lämmel, R., Visser, J., Saraiva, J. (eds.) GTTSE 2009. LNCS, vol. 6491, pp. 408–425. Springer, Heidelberg (2011). doi:10.1007/978-3-642-18023-1_12

    Chapter  Google Scholar 

  21. Sloane, A., Cassez, F., Buckley, S.: The sbt-rats parser generator plugin for Scala (tool paper). In: Proceedings of the 2016 7th ACM SIGPLAN Symposium on Scala, SCALA 2016, pp. 110–113. ACM, New York (2016). http://doi.acm.org/10.1145/2998392.3001580

  22. Stallman, R., Pesch, R., Shebs, S., et al.: Debugging with GDB. Free Software Foundation 51, 02110–1301 (2002)

    Google Scholar 

  23. Wilhelm, R., Engblom, J., Ermedahl, A., Holsti, N., Thesing, S., Whalley, D.B., Bernat, G., Ferdinand, C., Heckmann, R., Mitra, T., Mueller, F., Puaut, I., Puschner, P.P., Staschulat, J., Stenström, P.: The worst-case execution-time problem - overview of methods and survey of tools. ACM Trans. Embed. Comput. Syst. 7(3) (2008). Article no. 36

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Macquarie University, Sydney, Australia

    Franck Cassez, Pablo Gonzalez de Aledo & Peter Gjøl Jensen

  2. Aalborg University, Aalborg, Denmark

    Peter Gjøl Jensen

  3. University of Cantabria, Santander, Spain

    Pablo Gonzalez de Aledo

Authors
  1. Franck Cassez
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Pablo Gonzalez de Aledo
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Peter Gjøl Jensen
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Franck Cassez .

Editor information

Editors and Affiliations

  1. Reykjavik University, Reykjavik, Iceland

    Luca Aceto

  2. Aalborg University, Aalborg, Denmark

    Giorgio Bacci

  3. Aalborg University, Aalborg, Denmark

    Giovanni Bacci

  4. Reykjavík University, Reykjavik, Iceland

    Anna Ingólfsdóttir

  5. Inria Campus Beaulieu, Rennes, France

    Axel Legay

  6. Aalborg University, Aalborg, Denmark

    Radu Mardare

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this chapter

Cite this chapter

Cassez, F., de Aledo, P.G., Jensen, P.G. (2017). WUPPAAL: Computation of Worst-Case Execution-Time for Binary Programs with UPPAAL. In: Aceto, L., Bacci, G., Bacci, G., Ingólfsdóttir, A., Legay, A., Mardare, R. (eds) Models, Algorithms, Logics and Tools. Lecture Notes in Computer Science(), vol 10460. Springer, Cham. https://doi.org/10.1007/978-3-319-63121-9_28

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-63121-9_28

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-63120-2

  • Online ISBN: 978-3-319-63121-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation