{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:40:12Z","timestamp":1750308012701,"version":"3.41.0"},"reference-count":50,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2006,10,1]],"date-time":"2006-10-01T00:00:00Z","timestamp":1159660800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["SIGBED Rev."],"published-print":{"date-parts":[[2006,10]]},"abstract":"<jats:p>This paper describes ongoing work aimed at the construction of formal cost models and analyses that are capable of producing verifiable guarantees of resource usage (space, time and ultimately power consumption) in the context of real-time embedded systems. Our work is conducted in terms of the domain-specific language Hume, a language that combines functional programming for computations with finite-state automata for specifying reactive systems. We describe an approach in which high-level information derived from source-code analysis can be combined with worst-case execution time information obtained from abstract interpretation of low-level binary code. This abstract interpretation on the machine-code level is capable of dealing with complex architectural effects including cache and pipeline properties in an accurate way.<\/jats:p>","DOI":"10.1145\/1183088.1183093","type":"journal-article","created":{"date-parts":[[2007,1,17]],"date-time":"2007-01-17T18:32:02Z","timestamp":1169058722000},"page":"27-36","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Towards formally verifiable resource bounds for real-time embedded systems"],"prefix":"10.1145","volume":"3","author":[{"given":"Kevin","family":"Hammond","sequence":"first","affiliation":[{"name":"School of Computer Science, University of St Andrews, North Haugh, St Andrews, Scotland"}]},{"given":"Christian","family":"Ferdinand","sequence":"additional","affiliation":[{"name":"AbsInt GmbH, Germany"}]},{"given":"Reinhold","family":"Heckmann","sequence":"additional","affiliation":[{"name":"AbsInt GmbH, Germany"}]}],"member":"320","published-online":{"date-parts":[[2006,10]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Concurrent Programming in Erlang","author":"Armstrong J.","year":"1993","unstructured":"{1} J. Armstrong , S. Virding , and M. Williams . Concurrent Programming in Erlang . Prentice-Hall , 1993 . {1} J. Armstrong, S. Virding, and M. Williams. Concurrent Programming in Erlang. Prentice-Hall, 1993."},{"key":"e_1_2_1_2_1","volume-title":"Trends in Functional Programming","volume":"4","author":"Aspinall D.","year":"2004","unstructured":"{2} D. Aspinall , L. Beringer , M. Hofmann , and H.-W. Loidl . A resource-aware program logic for a JVM-like language . In Trends in Functional Programming , Volume 4 . Intellect , 2004 . {2} D. Aspinall, L. Beringer, M. Hofmann, and H.-W. Loidl. A resource-aware program logic for a JVM-like language. In Trends in Functional Programming, Volume 4. Intellect, 2004."},{"doi-asserted-by":"publisher","key":"e_1_2_1_3_1","DOI":"10.5555\/1947412.1947426"},{"doi-asserted-by":"publisher","key":"e_1_2_1_4_1","DOI":"10.5555\/827272.829144"},{"key":"e_1_2_1_5_1","volume-title":"Proof, Language, and Interaction","author":"Berry G.","year":"2000","unstructured":"{5} G. Berry . The Foundations of Esterel . In Proof, Language, and Interaction . MIT Press , 2000 . {5} G. Berry. The Foundations of Esterel. In Proof, Language, and Interaction. MIT Press, 2000."},{"doi-asserted-by":"publisher","key":"e_1_2_1_6_1","DOI":"10.1145\/291251.289440"},{"key":"e_1_2_1_7_1","first-page":"1","article-title":"AXD-301: a New Generation ATM Switching System","author":"Blau S.","year":"1998","unstructured":"{7} S. Blau and J. Rooth . AXD-301: a New Generation ATM Switching System . Ericsson Review , 1 , 1998 . {7} S. Blau and J. Rooth. AXD-301: a New Generation ATM Switching System. Ericsson Review, 1, 1998.","journal-title":"Ericsson Review"},{"doi-asserted-by":"publisher","key":"e_1_2_1_8_1","DOI":"10.1109\/5.97299"},{"doi-asserted-by":"publisher","key":"e_1_2_1_9_1","DOI":"10.1007\/11964681_5"},{"doi-asserted-by":"publisher","key":"e_1_2_1_11_1","DOI":"10.1109\/ECRTS.2005.7"},{"doi-asserted-by":"publisher","key":"e_1_2_1_12_1","DOI":"10.1145\/512950.512973"},{"doi-asserted-by":"publisher","key":"e_1_2_1_13_1","DOI":"10.1145\/512429.512433"},{"key":"e_1_2_1_14_1","volume-title":"Evaluation of static time analysis for CC systems. Technical report","author":"Eriksson O.","year":"2005","unstructured":"{14} O. Eriksson . Evaluation of static time analysis for CC systems. Technical report , M\u00e4lardalen University , August 2005 . {14} O. Eriksson. Evaluation of static time analysis for CC systems. Technical report, M\u00e4lardalen University, August 2005."},{"doi-asserted-by":"publisher","key":"e_1_2_1_16_1","DOI":"10.5555\/646787.703893"},{"unstructured":"{17} T.G. Group. Perfecting the Art of Building Embedded Systems. http:\/\/www.ganssle.com May 2003.  {17} T.G. Group. Perfecting the Art of Building Embedded Systems. http:\/\/www.ganssle.com May 2003.","key":"e_1_2_1_17_1"},{"doi-asserted-by":"publisher","key":"e_1_2_1_18_1","DOI":"10.1109\/ICECS.2000.911567"},{"key":"e_1_2_1_19_1","volume-title":"Trends in Functional Programming","volume":"4","author":"Hammond K.","year":"2004","unstructured":"{19} K. Hammond . Is it Time for Real-Time Functional Programming ? In Trends in Functional Programming , volume 4 . Intellect , 2004 . {19} K. Hammond. Is it Time for Real-Time Functional Programming? In Trends in Functional Programming, volume 4. Intellect, 2004."},{"doi-asserted-by":"publisher","key":"e_1_2_1_20_1","DOI":"10.5555\/954186.954189"},{"key":"e_1_2_1_21_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proc. Implementation of Functional Languages (IFL'02)","author":"Hammond K.","year":"2003","unstructured":"{21} K. Hammond and G. Michaelson . Predictable Space Behaviour in FSM-Hume . In Proc. Implementation of Functional Languages (IFL'02) , Madrid, Spain , number 2670 in Lecture Notes in Computer Science . Springer-Verlag , 2003 . {21} K. Hammond and G. Michaelson. Predictable Space Behaviour in FSM-Hume. In Proc. Implementation of Functional Languages (IFL'02), Madrid, Spain, number 2670 in Lecture Notes in Computer Science. Springer-Verlag, 2003."},{"key":"e_1_2_1_22_1","volume-title":"Proc. EuroPar 2002","author":"Hawkins J.","year":"2002","unstructured":"{22} J. Hawkins and A. Abdallah . Behavioural Synthesis of a Parallel Hardware JPEG Decoder from a Functional Specification . In Proc. EuroPar 2002 , Aug. 2002 . {22} J. Hawkins and A. Abdallah. Behavioural Synthesis of a Parallel Hardware JPEG Decoder from a Functional Specification. In Proc. EuroPar 2002, Aug. 2002."},{"doi-asserted-by":"publisher","key":"e_1_2_1_23_1","DOI":"10.1109\/JPROC.2003.814618"},{"doi-asserted-by":"publisher","key":"e_1_2_1_24_1","DOI":"10.5555\/763845.763847"},{"doi-asserted-by":"publisher","key":"e_1_2_1_25_1","DOI":"10.1145\/503272.503297"},{"doi-asserted-by":"publisher","key":"e_1_2_1_26_1","DOI":"10.1145\/604131.604148"},{"doi-asserted-by":"publisher","key":"e_1_2_1_27_1","DOI":"10.1145\/130697.130699"},{"doi-asserted-by":"publisher","key":"e_1_2_1_28_1","DOI":"10.1093\/comjnl\/32.2.98"},{"doi-asserted-by":"publisher","key":"e_1_2_1_29_1","DOI":"10.1145\/317636.317785"},{"doi-asserted-by":"publisher","key":"e_1_2_1_30_1","DOI":"10.1145\/237721.240882"},{"doi-asserted-by":"publisher","key":"e_1_2_1_32_1","DOI":"10.5555\/647171.716098"},{"key":"e_1_2_1_33_1","volume-title":"TFP'03 -- Symposium on Trends in Functional Programming","author":"MacKenzie K.","year":"2003","unstructured":"{33} K. MacKenzie and N. Wolverson . Camelot and Grail: Compiling a resource-aware functional language for the Java virtual machine . In TFP'03 -- Symposium on Trends in Functional Programming , Sep 11-12, 2003 , Edinburgh, Scotland , 2004. {33} K. MacKenzie and N. Wolverson. Camelot and Grail: Compiling a resource-aware functional language for the Java virtual machine. In TFP'03 -- Symposium on Trends in Functional Programming, Sep 11-12, 2003, Edinburgh, Scotland, 2004."},{"doi-asserted-by":"publisher","key":"e_1_2_1_34_1","DOI":"10.5555\/857172.857237"},{"key":"e_1_2_1_35_1","volume-title":"Trends in Functional Programming","volume":"4","author":"Michaelson G.","year":"2004","unstructured":"{35} G. Michaelson , K. Hammond , and J. S\u00e9rot . The finite state-ness of finite state Hume . In Trends in Functional Programming , Volume 4 . Intellect , 2004 . {35} G. Michaelson, K. Hammond, and J. S\u00e9rot. The finite state-ness of finite state Hume. In Trends in Functional Programming, Volume 4. Intellect, 2004."},{"doi-asserted-by":"publisher","key":"e_1_2_1_36_1","DOI":"10.5555\/549659"},{"key":"e_1_2_1_37_1","volume-title":"Programming with time-constrained reactions. Unpublished report","author":"Nordlander J.","year":"2006","unstructured":"{37} J. Nordlander , M. Carlsson , and M. Jones . Programming with time-constrained reactions. Unpublished report , 2006 . {37} J. Nordlander, M. Carlsson, and M. Jones. Programming with time-constrained reactions. Unpublished report, 2006."},{"key":"e_1_2_1_38_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proc. Implementation of Functional Languages (IFL'02)","author":"Portillo A.R.","year":"2003","unstructured":"{38} A.R. Portillo , K. Hammond , H.-W. Loidl , and P. Vasconcelos . A Sized Time System for a Parallel Functional Language (Revised) . In Proc. Implementation of Functional Languages (IFL'02) , Madrid, Spain , number 2670 in Lecture Notes in Computer Science . Springer-Verlag , 2003 . {38} A.R. Portillo, K. Hammond, H.-W. Loidl, and P. Vasconcelos. A Sized Time System for a Parallel Functional Language (Revised). In Proc. Implementation of Functional Languages (IFL'02), Madrid, Spain, number 2670 in Lecture Notes in Computer Science. Springer-Verlag, 2003."},{"doi-asserted-by":"publisher","key":"e_1_2_1_39_1","DOI":"10.1023\/A:1008119029962"},{"doi-asserted-by":"publisher","key":"e_1_2_1_40_1","DOI":"10.1145\/113446.113470"},{"key":"e_1_2_1_42_1","volume-title":"1st International Symposium on Leveraging Applications of Formal Methods (ISOLA'04)","author":"Sandell D.","year":"2004","unstructured":"{42} D. Sandell , A. Ermedahl , J. Gustafsson , and B. Lisper . Static timing analysis of real-time operating system code . In 1st International Symposium on Leveraging Applications of Formal Methods (ISOLA'04) , Cyprus , October 2004 . {42} D. Sandell, A. Ermedahl, J. Gustafsson, and B. Lisper. Static timing analysis of real-time operating system code. In 1st International Symposium on Leveraging Applications of Formal Methods (ISOLA'04), Cyprus, October 2004."},{"key":"e_1_2_1_43_1","volume-title":"Static WCET analysis of task-oriented code for construction vehicles. Master's thesis","author":"Sehlberg D.","year":"2005","unstructured":"{43} D. Sehlberg . Static WCET analysis of task-oriented code for construction vehicles. Master's thesis , M\u00e4lardalen University , October 2005 . {43} D. Sehlberg. Static WCET analysis of task-oriented code for construction vehicles. Master's thesis, M\u00e4lardalen University, October 2005."},{"key":"e_1_2_1_44_1","first-page":"21","volume-title":"Proceedings of the 5th Intl Workshop on Worst-Case Execution Time (WCET) Analysis","author":"Souyris J.","year":"2005","unstructured":"{44} J. Souyris , E. Le Pavec , G. Himbert , V. J\u00e9gu , G. Borios , and R. Heckmann . Computing the worst case execution time of an avionics program by abstract interpretation . In Proceedings of the 5th Intl Workshop on Worst-Case Execution Time (WCET) Analysis , pages 21 - 24 , 2005 . {44} J. Souyris, E. Le Pavec, G. Himbert, V. J\u00e9gu, G. Borios, and R. Heckmann. Computing the worst case execution time of an avionics program by abstract interpretation. In Proceedings of the 5th Intl Workshop on Worst-Case Execution Time (WCET) Analysis, pages 21-24, 2005."},{"doi-asserted-by":"publisher","key":"e_1_2_1_45_1","DOI":"10.5555\/827270.829031"},{"doi-asserted-by":"publisher","key":"e_1_2_1_46_1","DOI":"10.1109\/DSN.2003.1209972"},{"doi-asserted-by":"publisher","key":"e_1_2_1_47_1","DOI":"10.1006\/inco.1996.2613"},{"key":"e_1_2_1_48_1","volume-title":"Proc. 1995 Symp. on Functional Programming Languages in Education -- FPLE'95, number 1022 in Lecture Notes in Computer Science","author":"Turner D.","year":"1995","unstructured":"{48} D. Turner . Elementary Strong Functional Programming . In Proc. 1995 Symp. on Functional Programming Languages in Education -- FPLE'95, number 1022 in Lecture Notes in Computer Science . Springer-Verlag , Dec. 1995 . {48} D. Turner. Elementary Strong Functional Programming. In Proc. 1995 Symp. on Functional Programming Languages in Education -- FPLE'95, number 1022 in Lecture Notes in Computer Science. Springer-Verlag, Dec. 1995."},{"issue":"7","key":"e_1_2_1_49_1","first-page":"751","article-title":"Total Functional Programming","volume":"10","author":"Turner D.","year":"2004","unstructured":"{49} D. Turner . Total Functional Programming . Journal of Universal Computing , 10 ( 7 ): 751 - 768 , 2004 . {49} D. Turner. Total Functional Programming. Journal of Universal Computing, 10(7):751-768, 2004.","journal-title":"Journal of Universal Computing"},{"doi-asserted-by":"publisher","key":"e_1_2_1_51_1","DOI":"10.1007\/978-3-540-27861-0_6"},{"doi-asserted-by":"publisher","key":"e_1_2_1_52_1","DOI":"10.1002\/spe.4380250105"},{"doi-asserted-by":"publisher","key":"e_1_2_1_53_1","DOI":"10.1145\/507635.507654"},{"key":"e_1_2_1_54_1","volume-title":"Proc. Intl. Symp. on Cooperative Database Systems for Advanced Applications","author":"Wikstr\u00f6m C.","year":"1996","unstructured":"{54} C. Wikstr\u00f6m and H. Nilsson . Mnesia -- an industrial database with transactions, distribution and a logical query language . In Proc. Intl. Symp. on Cooperative Database Systems for Advanced Applications , 1996 . {54} C. Wikstr\u00f6m and H. Nilsson. Mnesia -- an industrial database with transactions, distribution and a logical query language. In Proc. Intl. Symp. on Cooperative Database Systems for Advanced Applications, 1996."},{"key":"e_1_2_1_55_1","volume-title":"Evaluation of methods for dynamic time analysis for CC-systems AB. Technical report","author":"Zhang Y.","year":"2005","unstructured":"{55} Y. Zhang . Evaluation of methods for dynamic time analysis for CC-systems AB. Technical report , M\u00e4lardalen University , August 2005 . {55} Y. Zhang. Evaluation of methods for dynamic time analysis for CC-systems AB. Technical report, M\u00e4lardalen University, August 2005."}],"container-title":["ACM SIGBED Review"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1183088.1183093","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1183088.1183093","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T15:06:36Z","timestamp":1750259196000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1183088.1183093"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2006,10]]},"references-count":50,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2006,10]]}},"alternative-id":["10.1145\/1183088.1183093"],"URL":"https:\/\/doi.org\/10.1145\/1183088.1183093","relation":{},"ISSN":["1551-3688"],"issn-type":[{"type":"electronic","value":"1551-3688"}],"subject":[],"published":{"date-parts":[[2006,10]]},"assertion":[{"value":"2006-10-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}