{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,11,10]],"date-time":"2026-11-10T22:27:35Z","timestamp":1794349655974,"version":"4.9.0"},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540754534","type":"print"},{"value":"9783540754541","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/978-3-540-75454-1_19","type":"book-chapter","created":{"date-parts":[[2007,9,17]],"date-time":"2007-09-17T21:47:54Z","timestamp":1190065674000},"page":"257-273","source":"Crossref","is-referenced-by-count":7,"title":["Combining Formal Verification with Observed System Execution Behavior to Tune System Parameters"],"prefix":"10.1007","author":[{"given":"Minyoung","family":"Kim","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Mark-Oliver","family":"Stehr","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Carolyn","family":"Talcott","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nikil","family":"Dutt","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Nalini","family":"Venkatasubramanian","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"19_CR1","unstructured":"Kim, M., Dutt, N., Venkatasubramanian, N.: Policy construction and validation for energy minimization in cross layered systems: A formal method approach. In: IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS 2006) Work-in-Progress Session"},{"key":"19_CR2","unstructured":"Forge Project: http:\/\/forge.ics.uci.edu"},{"key":"19_CR3","doi-asserted-by":"crossref","unstructured":"Mohapatra, S., Cornea, R., Oh, H., Lee, K., Kim, M., Dutt, N.D., Gupta, R., Nicolau, A., Shukla, S.K., Venkatasubramanian, N.: A cross-layer approach for power-performance optimization in distributed mobile systems. In: IEEE 19th International Parallel and Distributed Processing Symposium (IPDPS 2005) (2005)","DOI":"10.1109\/IPDPS.2005.13"},{"key":"19_CR4","doi-asserted-by":"crossref","unstructured":"Kim, M., Stehr, M.O., Talcott, C., Dutt, N., Venkatasubramanian, N.: A probabilistic formal analysis approach to cross layer optimization in distributed embedded systems. In: 9th IFIP International Conference on Formal Methods for Open Object-based Distributed Systems (FMOODS 2007). LNCS, vol.\u00a04468, pp. 285\u2013300 (2007)","DOI":"10.1007\/978-3-540-72952-5_18"},{"key":"19_CR5","unstructured":"Kim, D., Kim, M., Ha, S.: A Case Study of System Level Specification and Software Synthesis of Multimode Multimedia Terminal. In: IEEE Workshop on Embedded Systems for Real-Time Multimedia (ESTImedia 2003), pp. 57\u201364 (2003)"},{"key":"19_CR6","doi-asserted-by":"crossref","unstructured":"Kim, M., Ha, S.: Hybrid run-time power management technique for real-time embedded system with voltage scalable processor. In: ACM Conference on Languages, Compilers, and Tools for Embedded Systems (LCTES 2001), pp. 11\u201319 (2001)","DOI":"10.1145\/384196.384202"},{"issue":"3","key":"19_CR7","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1145\/1148094.1148100","volume":"10","author":"M. Kim","year":"2006","unstructured":"Kim, M., Oh, H., Dutt, N., Nicolau, A., Venkatasubramanian, N.: PBPAIR: an energy-efficient error-resilient encoding using probability based power aware intra refresh. ACM SIGMOBILE Mob. Comput. Commun. Rev.\u00a010(3), 58\u201369 (2006)","journal-title":"ACM SIGMOBILE Mob. Comput. Commun. Rev."},{"key":"19_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1007\/3-540-44881-0_7","volume-title":"Rewriting Techniques and Applications","author":"M. Clavel","year":"2003","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.L.: The maude 2.0 system. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol.\u00a02706, pp. 76\u201387. Springer, Heidelberg (2003)"},{"issue":"2","key":"19_CR9","doi-asserted-by":"publisher","first-page":"187","DOI":"10.1016\/S0304-3975(01)00359-0","volume":"285","author":"M. Clavel","year":"2002","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Quesada, J.F.: Maude: specification and programming in rewriting logic. Theoretical Computer Science\u00a0285(2), 187\u2013243 (2002)","journal-title":"Theoretical Computer Science"},{"key":"19_CR10","series-title":"Lecture Notes in Computer Science","volume-title":"All about maude, a high-performance logical framework","author":"M. Clavel","year":"2007","unstructured":"Clavel, M., Dur\u00e1n, F., Eker, S., Lincoln, P., Mart\u00ed-Oliet, N., Meseguer, J., Talcott, C.: All about maude, a high-performance logical framework. LNCS, vol.\u00a04350. Springer, Heidelberg (2007)"},{"issue":"1","key":"19_CR11","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/0304-3975(92)90182-F","volume":"96","author":"J. Meseguer","year":"1992","unstructured":"Meseguer, J.: Conditional Rewriting Logic as a unified model of concurrency. Theoretical Computer Science\u00a096(1), 73\u2013155 (1992)","journal-title":"Theoretical Computer Science"},{"key":"19_CR12","unstructured":"Real-Time Maude: http:\/\/www.ifi.uio.no\/RealTimeMaude"},{"key":"19_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"269","DOI":"10.1007\/3-540-61474-5_75","volume-title":"Computer Aided Verification","author":"A. Aziz","year":"1996","unstructured":"Aziz, A., Sanwal, K., Singhal, V., Brayton, R.K.: Verifying continuous time markov chains. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 269\u2013276. Springer, Heidelberg (1996)"},{"issue":"2","key":"19_CR14","doi-asserted-by":"publisher","first-page":"163","DOI":"10.2307\/1403192","volume":"55","author":"C. Jarque","year":"1987","unstructured":"Jarque, C., Bera, A.: A test for normality of observations and regression residuals. Internat. Statist. Rev.\u00a055(2), 163\u2013172 (1987)","journal-title":"Internat. Statist. Rev."},{"key":"19_CR15","unstructured":"Kim, M., Stehr, M.O., Talcott, C., Lee, K., Dutt, N., Venkatasubramanian, N.: Iterative system tuning for proactive systems by formal verification and system prototype: System prototype program interface. CECS Technical Report, UC Irvine (February 2007)"},{"key":"19_CR16","unstructured":"Signal Process. Multimedia Lab. Univ. British Columbia: TMN 10 (H.263+) encoder\/decoder, version 3.2.0 (September 1998)"},{"key":"19_CR17","unstructured":"Ebony Board: http:\/\/www.amcc.com\/Embedded\/"},{"key":"19_CR18","unstructured":"http:\/\/www.ibm.com\/chips\/techlib\/techlib.nsf\/products\/PowerPC_440_Embedded_Core"},{"key":"19_CR19","unstructured":"Simics Full System Simulation Platform: http:\/\/www.simics.net"},{"key":"19_CR20","unstructured":"Han, Q., Venkatasubramanian, N.: AutoSeC: An Integrated Middleware Framework for Dynamic Service Brokering. IEEE Distributed Systems On-line\u00a02(7) (2001)"},{"issue":"2","key":"19_CR21","doi-asserted-by":"publisher","first-page":"160","DOI":"10.1007\/s00165-005-0062-0","volume":"17","author":"G. Norman","year":"2005","unstructured":"Norman, G., Parker, D., Kwiatkowska, M., Shukla, S., Gupta, R.: Using probabilistic model checking for dynamic power management. Formal Aspects of Computing\u00a017(2), 160\u2013176 (2005)","journal-title":"Formal Aspects of Computing"},{"key":"19_CR22","doi-asserted-by":"crossref","unstructured":"Paleologo, G.A., Benini, L., Bogliolo, A., Micheli, G.D.: Policy optimization for dynamic power management. In: 35th Annual Conference on Design Automation (DAC 1998). pp. 182\u2013187 (1998)","DOI":"10.1145\/277044.277094"},{"key":"19_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/11691372_29","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A. Hinton","year":"2006","unstructured":"Hinton, A., Kwiatkowska, M., Norman, G., Parker, D.: PRISM: A tool for automatic verification of probabilistic systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006 and ETAPS 2006. LNCS, vol.\u00a03920, pp. 441\u2013444. Springer, Heidelberg (2006)"},{"key":"19_CR24","doi-asserted-by":"crossref","unstructured":"Abdelwahed, S., Kandasamy, N., Neema, S.: Online control for self-management in computing systems. In: 10th IEEE Real-Time and Embedded Technology and Applications Symposium (RTAS 2004), p. 368 (2004)","DOI":"10.1109\/RTTAS.2004.1317283"},{"key":"19_CR25","doi-asserted-by":"crossref","unstructured":"Lu, Z., Hein, J., Humphrey, M., Stan, M., Lach, J., Skadron, K.: Control-theoretic dynamic frequency and voltage scaling for multimedia workloads. In: International Conference on Compilers, Architecture, and Synthesis for Embedded Systems (CASES 2002). pp. 156\u2013163 (2002)","DOI":"10.1145\/581630.581654"},{"key":"19_CR26","doi-asserted-by":"crossref","unstructured":"Acquaviva, A., Aldini, A., Bernardo, M., Bogliolo, A., Bonta, E., Lattanzi, E.: Assessing the impact of dynamic power management on the functionality and the performance of battery-powered appliances. In: International Conference on Dependable Systems and Networks (DSN 2004). p. 731 (2004)","DOI":"10.1109\/DSN.2004.1311944"}],"container-title":["Lecture Notes in Computer Science","Formal Modeling and Analysis of Timed Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-75454-1_19.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,27]],"date-time":"2021-04-27T07:01:58Z","timestamp":1619506918000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-75454-1_19"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["9783540754534","9783540754541"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-75454-1_19","relation":{"is-part-of":[{"id-type":"doi","id":"https:\/\/doi.org\/10.1007\/978-3-540-75454-1","asserted-by":"object"}]},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[]}}