Abstract
Hard real-time systems need methods to determine upper bounds for their execution times, usually called worst-case execution times. This talk gives an introduction into state-of-art Timing-Analysis methods. These use Abstract Interpretation to predict the system’s behavior on the underlying processor’s components and Integer Linear Programming to determine a worst-case path through the program. The abstract interpretation is based on an abstract processor model that is conservative with respect to the timing behavior of the concrete processor. Ongoing work is reported to analyze abstract processor models for properties that have a strong influence on the expected precision of timing prediction and also on the architecture of the timing-analysis tool. Some of the properties we are interested in can be model checked.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Ferdinand, C., Heckmann, R., Langenbach, M., Martin, F., Schmidt, M., Theiling, H., Thesing, S., Wilhelm, R.: WCET Determination for a Real-Life Processor. In: Henzinger, T.A., Kirsch, C. (eds.) EMSOFT 2001. LNCS, vol. 2211, pp. 469–485. Springer, Heidelberg (2001)
Harmon, M.G., Baker, T.P., Whalley, D.B.: A Retargetable Technique for Predicting Execution Time of Code Segments. Real-Time Systems 7, 159–182 (1994)
Heckmann, R., Langenbach, M., Thesing, S., Wilhelm, R.: The influence of processor architecture an the design and the results of WCET tools. IEEE Proceedings on Real-Time Systems 91(7), 1038–1054 (2003)
Li, Y.-T.S., Malik, S., Wolfe, A.: Performance estimation of embedded software with instruction cache modeling. Design Automation of Electronic Systems 4(3), 257–279 (1999)
Lundqvist, T., Stenström, P.: Timing anomalies in dynamically scheduled microprocessors. In: Proceedings of the 20th IEEE Real-Time Systems Symposium (RTSS 1999), December 1999, pp. 12–21 (1999)
Langenbach, M., Thesing, S., Heckmann, R.: Pipeline Modelling for Timing Analysis. In: Static Analysis Symposium. LNCS, vol. 2274, pp. 294–309. Springer, Heidelberg (2002)
Lundqvist, T.: A WCET Analysis Method for Pipelined Microprocessors with Cache Memories. PhD thesis, Chalmers University of Technology, Göteborg, Sweden (2002)
Schneider, J.: Combined Schedulability and WCET Analysis for Real-Time Operating Systems. PhD thesis, Saarland University (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Wilhelm, R. (2004). Formal Analysis of Processor Timing Models. In: Graf, S., Mounier, L. (eds) Model Checking Software. SPIN 2004. Lecture Notes in Computer Science, vol 2989. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24732-6_1
Download citation
DOI: https://doi.org/10.1007/978-3-540-24732-6_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-21314-7
Online ISBN: 978-3-540-24732-6
eBook Packages: Springer Book Archive