{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,18]],"date-time":"2025-11-18T12:15:18Z","timestamp":1763468118426,"version":"3.41.0"},"reference-count":45,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2012,12,1]],"date-time":"2012-12-01T00:00:00Z","timestamp":1354320000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["0615438, 0615436, and 0932397"],"award-info":[{"award-number":["0615438, 0615436, and 0932397"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Embed. Comput. Syst."],"published-print":{"date-parts":[[2012,12]]},"abstract":"<jats:p>Resource-limited mobile embedded systems can benefit greatly from dynamic adaptation of system parameters. We propose a novel approach that employs iterative tuning using lightweight formal verification at runtime with feedback for dynamic adaptation. One objective of this approach is to enable trade-off analysis across multiple layers (e.g., application, middleware, OS) and predict the possible property violations as the system evolves dynamically over time. Specifically, an executable formal specification is developed for each layer of the mobile system under consideration. The formal specification is then analyzed using statistical property checking and statistical quantitative analysis, to determine the impact of various resource management policies for achieving desired timing\/QoS properties. Integration of formal analysis with dynamic behavior from system execution results in a feedback loop that enables model refinement and further optimization of policies and parameters. We demonstrate the applicability of this approach to the adaptive provisioning of resource-limited distributed real-time systems using a mobile multimedia case study.<\/jats:p>","DOI":"10.1145\/2362336.2362340","type":"journal-article","created":{"date-parts":[[2013,1,11]],"date-time":"2013-01-11T15:42:48Z","timestamp":1357918968000},"page":"1-23","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":19,"title":["xTune"],"prefix":"10.1145","volume":"11","author":[{"given":"Minyoung","family":"Kim","sequence":"first","affiliation":[{"name":"SRI International, CA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mark-Oliver","family":"Stehr","sequence":"additional","affiliation":[{"name":"SRI International, CA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Carolyn","family":"Talcott","sequence":"additional","affiliation":[{"name":"SRI International, CA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nikil","family":"Dutt","sequence":"additional","affiliation":[{"name":"University of California, Irvine, CA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nalini","family":"Venkatasubramanian","sequence":"additional","affiliation":[{"name":"University of California, Irvine, CA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2013,1]]},"reference":[{"volume-title":"Proceedings of the 10th IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS'04)","author":"Abdelwahed S.","key":"e_1_2_1_1_1"},{"volume-title":"Proceedings of the International Conference on Dependable Systems and Networks (DSN'04)","author":"Acquaviva A.","key":"e_1_2_1_2_1"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.10.040"},{"volume-title":"Proceedings of the 8th International Conference on Computer Aided Verification (CAV'96)","author":"Aziz A.","key":"e_1_2_1_4_1"},{"volume-title":"Proceedings of the International Conference on Concurrency Theory. 146--161","author":"Baier C.","key":"e_1_2_1_5_1"},{"volume":"4350","volume-title":"Lecture Notes in Computer Science","author":"Clavel M.","key":"e_1_2_1_6_1"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1403375.1403400"},{"key":"e_1_2_1_8_1","first-page":"7","article-title":"AutoSeC: An integrated middleware framework for dynamic service brokering","volume":"2","author":"Han Q.","year":"2001","journal-title":"IEEE Distrib. Syst. Online"},{"key":"e_1_2_1_9_1","unstructured":"Hogg R. and Craig A. 1995. Introduction to Mathematical Statistics 5th Ed. Pearson.  Hogg R. and Craig A. 1995. Introduction to Mathematical Statistics 5th Ed. Pearson."},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1027794.1027796"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/1787497.1787510"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.2307\/1403192"},{"volume-title":"Proceedings of the International Conference on Concurrency Theory.","author":"Jeannet B.","key":"e_1_2_1_13_1"},{"volume-title":"Proceedings of the Logic in Computer Science Symposium (LICS). IEEE Computer Society, 266--277","author":"Jonsson B.","key":"e_1_2_1_14_1"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2009.11"},{"volume-title":"Proceedings of RTAS'06 (WiP Session). 25--28","author":"Kim M.","key":"e_1_2_1_16_1"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/384198.384202"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1148094.1148100"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/1779879.1779898"},{"key":"e_1_2_1_20_1","unstructured":"Kim M. Stehr M.-O. Talcott C. Dutt N. and Venkatasubramanian N. 2007b. Modeling and exploiting cross-layer optimization in distributed embedded systems. Tech. rep. SRI-CSL-07-02 SRI International.  Kim M. Stehr M.-O. Talcott C. Dutt N. and Venkatasubramanian N. 2007b. Modeling and exploiting cross-layer optimization in distributed embedded systems. Tech. rep. SRI-CSL-07-02 SRI International."},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/1772150.1772175"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/1403375.1403531"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-39958-2_3"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2005.10.030"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/49.790486"},{"key":"e_1_2_1_26_1","unstructured":"Lorch J. R. 2001. Operating systems techniques for reducing processor energy consumption. Ph.D. thesis University of California Berkeley.   Lorch J. R. 2001. Operating systems techniques for reducing processor energy consumption. Ph.D. thesis University of California Berkeley."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/581630.581654"},{"key":"e_1_2_1_28_1","unstructured":"McCabe G. P. and Moore D. S. 2005. Introduction to the Practice of Statistics 5th Ed. W.H. Freeman.  McCabe G. P. and Moore D. S. 2005. Introduction to the Practice of Statistics 5th Ed. W.H. Freeman."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90182-F"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1109\/IPDPS.2005.13"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/JSAC.2007.070509"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-005-0062-0"},{"key":"e_1_2_1_33_1","unstructured":"Olsen C. M. and Narayanaswami C. 2003. A work dependent OS timing scheme for power management: Implementation in Linux and modeling of energy savings. Internet draft IBM.  Olsen C. M. and Narayanaswami C. 2003. A work dependent OS timing scheme for power management: Implementation in Linux and modeling of energy savings. Internet draft IBM."},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-007-9001-5"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/378239.379075"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04761-9_11"},{"volume-title":"Proceedings of CAV'04","author":"Sen K.","key":"e_1_2_1_37_1"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_26"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-006-0004-z"},{"key":"e_1_2_1_40_1","unstructured":"TMN 10. 1998. TMN 10 (H.263&plus;) ver. 3.2.0. Image Process. Laboratory University of British Columbia.  TMN 10. 1998. TMN 10 (H.263&plus;) ver. 3.2.0. Image Process. Laboratory University of British Columbia."},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1214\/aoms\/1177731118"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542245.1542268"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-005-0187-8"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1109\/TMC.2006.98"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/1065910.1065939"}],"container-title":["ACM Transactions on Embedded Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2362336.2362340","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2362336.2362340","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T20:14:16Z","timestamp":1750277656000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2362336.2362340"}},"subtitle":["A formal methodology for cross-layer tuning of mobile embedded systems"],"short-title":[],"issued":{"date-parts":[[2012,12]]},"references-count":45,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2012,12]]}},"alternative-id":["10.1145\/2362336.2362340"],"URL":"https:\/\/doi.org\/10.1145\/2362336.2362340","relation":{},"ISSN":["1539-9087","1558-3465"],"issn-type":[{"type":"print","value":"1539-9087"},{"type":"electronic","value":"1558-3465"}],"subject":[],"published":{"date-parts":[[2012,12]]},"assertion":[{"value":"2010-02-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2010-11-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2013-01-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}