Abstract
We present a new compositional approach for analysing the resource usage of reactive box-based systems, as exemplified by Hume. Our analysis deals with a key aspect of reactivity, namely determining the worst-case execution time between some external input event and the associated output event, taking into account repeated box iterations and the possible interactions between boxes in terms of input/output values. In order to achieve this, we capture the system behaviour by abstract interpretation, obtaining counter automata, finite state automata with additional counters that can be used to represent sizes/resource costs and control repetitions. These counter automata precisely capture cost information from the original box-based system, but in a way that is more abstract and therefore easier to analyse. The key contribution of this paper over previous work is that we are able to analyse box-based computations for cyclic systems whose costs may depend on some input parameters and in which the cost formulae are non-linear.
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
Albert, E., Arenas, P., Genaim, S., Puebla, G.: Closed-Form Upper Bounds in Static Cost Analysis. Journal of Automated Reasoning 46(2), 161–203 (2011)
Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)
Annichini, A., Asarin, E., Bouajjani, A.: Symbolic Techniques for Parametric Reasoning About Counter and Clock Systems. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 419–434. Springer, Heidelberg (2000)
Bernat, G., Burns, A.: An approach to symbolic worst-case execution time analysis. In: 25th Workshop on Real-Time Programming, Palma, Spain (May 2000)
Bozga, M., Iosif, R., Lakhnech, Y.: Flat Parametric Counter Automata. In: Bugliesi, M., Preneel, B., Sassone, V., Wegener, I. (eds.) ICALP 2006. LNCS, vol. 4052, pp. 577–588. Springer, Heidelberg (2006)
Bygde, S., Lisper, B.: Towards an automatic parametric WCET analysis. In: 8th Intl. Workshop on Worst-Case Execution Time (WCET) Analysis (2008); associated with ECRTS 2008
Chin, W.-N., Khoo, S.-C.: Calculating sized types. In: Partial Evaluation and Semantics-based Program Manipulation, pp. 62–72 (2000)
Coffman, J., Healy, C., Mueller, F., Whalley, D.: Generalizing parametric timing analysis. In: LCTES 2007, pp. 152–154 (2007)
Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proc. Principles of Programming Languages (POPL), pp. 238–252 (1977)
Graham, R.L., Knuth, D.E., Patashnik, O.: Concrete Mathematics. 2nd edition. Pearson Education (1994)
Hammond, K., Michaelson, G.J.: Hume: A Domain-Specific Language for Real-Time Embedded Systems. In: Pfenning, F., Macko, M. (eds.) GPCE 2003. LNCS, vol. 2830, pp. 37–56. Springer, Heidelberg (2003)
Hernández-Marin, S., Wallace, A.M., Gibson, G.J.: Bayesian analysis of LiDAR signals with multiple returns. IEEE Transactions on Pattern Analysis and Machine Intelligence 29(12), 2170–2180 (2007)
Herrmann, C.A., Bonenfant, A., Hammond, K., Jost, S., Loidl, H.-W., Pointon, R.: Automatic amortised worst-case execution time analysis. In: Rochange, C. (ed.) 7th Intl. Workshop on Worst-Case Execution Time (WCET) Analysis. Internationales Begegnungs- und Forschungszentrum für Informatik (IBFI), Schloss Dagstuhl, Germany (2007)
Hoffmann, J., Aehlig, K., Hofmann, M.: Multivariate Amortized Resource Analysis. In: 38th Symp. on Principles of Prog. Langs. (POPL 2011), pp. 357–370 (2011)
Hovland, D.: Regular Expressions with Numerical Constraints and Automata with Counters. In: Leucker, M., Morgan, C. (eds.) ICTAC 2009. LNCS, vol. 5684, pp. 231–245. Springer, Heidelberg (2009)
Jost, S., Hammond, K., Loidl, H.-W., Hofmann, M.: Static determination of quantitative resource usage for higher-order programs. In: Proc. Principles of Programming Languages, POPL (2010)
Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer (1999)
Penczek, F., Herhut, S., Grelck, C., Scholz, S.-B., Shafarenko, A., Barrière, R., Lenormand, E.: Parallel Signal Processing with S-Net. Procedia Computer Science 1(1), 2079–2088 (2010); ICCS 2010
Schüle, T., Schneider, K.: Exact runtime analysis using automata-based symbolic simulations. In: Proc 1st ACM/IEEE Int. Conf. Formal Methods and Models for Co-Design (MEMOCODE 2003). IEEE Computer Society (2003)
Sipser, M.: Introduction to the Theory of Computation. PWS Publishing Company (1997)
Sperberg-McQueen, M.: Notes on finite state automata with counters (May 2004), http://www.w3.org/XML/2004/05/msm-cfa.html
Valiant, L.G.: A bridging model for parallel computation. Communications of the ACM 33(8), 103–111 (1990)
Wegbreit, B.: Mechanical program analysis. Communication of the ACM 18(9), 528–539 (1975)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Herrmann, C.A., Hammond, K. (2012). Counter Automata for Parameterised Timing Analysis of Box-Based Systems. In: Peña, R., van Eekelen, M., Shkaravska, O. (eds) Foundational and Practical Aspects of Resource Analysis. FOPARA 2011. Lecture Notes in Computer Science, vol 7177. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-32495-6_8
Download citation
DOI: https://doi.org/10.1007/978-3-642-32495-6_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-32494-9
Online ISBN: 978-3-642-32495-6
eBook Packages: Computer ScienceComputer Science (R0)