{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,11,10]],"date-time":"2026-11-10T21:42:51Z","timestamp":1794346971772,"version":"4.9.0"},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540729198","type":"print"},{"value":"9783540729525","type":"electronic"}],"license":[{"start":{"date-parts":[[2007,1,1]],"date-time":"2007-01-01T00:00:00Z","timestamp":1167609600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2007]]},"DOI":"10.1007\/978-3-540-72952-5_18","type":"book-chapter","created":{"date-parts":[[2007,6,26]],"date-time":"2007-06-26T04:10:08Z","timestamp":1182831008000},"page":"285-300","source":"Crossref","is-referenced-by-count":14,"title":["A Probabilistic Formal Analysis Approach to Cross Layer Optimization in Distributed Embedded Systems"],"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":"18_CR1","unstructured":"Forge Project: http:\/\/forge.ics.uci.edu"},{"key":"18_CR2","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: IPDPS \u201905. International Parallel and Distributed Processing Symposium (2005)","DOI":"10.1109\/IPDPS.2005.13"},{"key":"18_CR3","unstructured":"Kim, M., Dutt, N., Venkatasubramanian, N.: Policy construction and validation for energy minimization in cross layered systems: A formal method approach. In: Real-Time and Embedded Technology and Applications Symposium (RTAS \u201906) Work-in-Progress Session. pp. 25\u201328 (2006)"},{"key":"18_CR4","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)"},{"key":"18_CR5","unstructured":"Kim, D., Kim, M., Ha, S.: A Case Study of System Level Specification and Software Synthesis of Multimode Multimedia Terminal. In: Embedded Systems for Real-Time Multimedia (ESTImedia \u201903), pp. 57\u201364 (2003)"},{"issue":"8","key":"18_CR6","doi-asserted-by":"publisher","first-page":"11","DOI":"10.1145\/384196.384202","volume":"36","author":"M. Kim","year":"2001","unstructured":"Kim, M., Ha, S.: Hybrid Run-time Power Management Technique for Real-time Embedded System with Voltage Scalable Processor. ACM SIGPLAN Notices\u00a036(8), 11\u201319 (2001)","journal-title":"ACM SIGPLAN Notices"},{"issue":"3","key":"18_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. SIGMOBILE Mob. Comput. Commun. Rev.\u00a010(3), 58\u201369 (2006)","journal-title":"SIGMOBILE Mob. Comput. Commun. Rev."},{"key":"18_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","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.: The maude 2.0 system. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol.\u00a02706, Springer, Heidelberg (2003)"},{"issue":"2","key":"18_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"},{"issue":"1","key":"18_CR10","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":"18_CR11","unstructured":"Real-Time Maude 2.2: http:\/\/www.ifi.uio.no\/RealTimeMaude ."},{"issue":"2","key":"18_CR12","doi-asserted-by":"publisher","first-page":"213","DOI":"10.1016\/j.entcs.2005.10.040","volume":"153","author":"G.A. Agha","year":"2006","unstructured":"Agha, G.A., Meseguer, J., Sen, K.: PMaude: Rewrite-based specification language for probabilistic object systems. Electr. Notes Theor. Comput. Sci.\u00a0153(2), 213\u2013239 (2006)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"issue":"2","key":"18_CR13","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1214\/aoms\/1177731118","volume":"16","author":"A. Wald","year":"1945","unstructured":"Wald, A.: Sequential tests of statistical hypotheses. Annals of Mathematical Statistics\u00a016(2), 117\u2013186 (1945)","journal-title":"Annals of Mathematical Statistics"},{"key":"18_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/978-3-540-27813-9_16","volume-title":"Computer Aided Verification","author":"K. Sen","year":"2004","unstructured":"Sen, K., Viswanathan, M., Agha, G.: Statistical model checking of black-box probabilistic systems. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 202\u2013215. Springer, Heidelberg (2004)"},{"key":"18_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"429","DOI":"10.1007\/11513988_43","volume-title":"Computer Aided Verification","author":"H. Younes","year":"2005","unstructured":"Younes, H.: Ymer: A statistical model checker. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 429\u2013433. Springer, Heidelberg (2005)"},{"issue":"3","key":"18_CR16","doi-asserted-by":"publisher","first-page":"216","DOI":"10.1007\/s10009-005-0187-8","volume":"8","author":"H. Younes","year":"2006","unstructured":"Younes, H., Kwiatkowska, M., Norman, G., Parker, D.: Numerical vs. statistical probabilistic model checking. International Journal on Software Tools for Technology Transfer (STTT)\u00a08(3), 216\u2013228 (2006)","journal-title":"International Journal on Software Tools for Technology Transfer (STTT)"},{"issue":"2","key":"18_CR17","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":"18_CR18","unstructured":"Hogg, R., Craig, A.: Introduction to Mathematical Statistics. 5th edn. (1995)"},{"issue":"1","key":"18_CR19","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1145\/343369.343402","volume":"1","author":"A. Aziz","year":"2000","unstructured":"Aziz, A., Sanwal, K., Singhal, V., Brayton, R.: Model-checking continuous-time Markov chains. ACM Trans. Comput. Logic\u00a01(1), 162\u2013170 (2000)","journal-title":"ACM Trans. Comput. Logic"},{"key":"18_CR20","unstructured":"Image Process Lab. Univ. British Columbia: TMN 10 (H.263+), ver. 3.2.0 (1998)"},{"key":"18_CR21","unstructured":"http:\/\/www.intel.com\/design\/pca\/prodbref\/252780.htm"},{"key":"18_CR22","doi-asserted-by":"crossref","unstructured":"Kim, M., Stehr, M.O., Talcott, C., Dutt, N., Venkatasubramanian, N.: Modeling and Exploiting Cross-Layer Optimization in Distributed Embedded Systems. Technical Report SRI-CSL-07-02, SRI International (February 2007)","DOI":"10.1007\/978-3-540-72952-5_18"},{"key":"18_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"32","DOI":"10.1007\/978-3-540-39958-2_3","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"N. Kumar","year":"2003","unstructured":"Kumar, N., Sen, K., Meseguer, J., Agha, G.: A rewriting based model for probabilistic distributed object systems. In: Najm, E., Nestmann, U., Stevens, P. (eds.) FMOODS 2003. LNCS, vol.\u00a02884, pp. 32\u201346. Springer, Heidelberg (2003)"},{"key":"18_CR24","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)"}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Open Object-Based Distributed Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-540-72952-5_18","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,29]],"date-time":"2019-04-29T16:20:41Z","timestamp":1556554841000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-540-72952-5_18"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007]]},"ISBN":["9783540729198","9783540729525"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-540-72952-5_18","relation":{"is-part-of":[{"id-type":"doi","id":"https:\/\/doi.org\/10.1007\/978-3-540-72952-5","asserted-by":"object"}]},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007]]}}}