{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,7]],"date-time":"2025-04-07T02:10:03Z","timestamp":1743991803039,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642324680"},{"type":"electronic","value":"9783642324697"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-32469-7_4","type":"book-chapter","created":{"date-parts":[[2012,8,21]],"date-time":"2012-08-21T21:07:27Z","timestamp":1345583247000},"page":"47-62","source":"Crossref","is-referenced-by-count":6,"title":["Waiting for Locks: How Long Does It Usually Take?"],"prefix":"10.1007","author":[{"given":"Christel","family":"Baier","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marcus","family":"Daum","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Benjamin","family":"Engel","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hermann","family":"H\u00e4rtig","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Joachim","family":"Klein","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sascha","family":"Kl\u00fcppelholz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Steffen","family":"M\u00e4rcker","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hendrik","family":"Tews","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marcus","family":"V\u00f6lp","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"1","key":"4_CR1","doi-asserted-by":"publisher","first-page":"6","DOI":"10.1109\/71.80120","volume":"1","author":"T.E. Anderson","year":"1990","unstructured":"Anderson, T.E.: The performance of spin lock alternatives for shared-memory multiprocessors. IEEE Trans. Parallel Distrib. Syst.\u00a01(1), 6\u201316 (1990)","journal-title":"IEEE Trans. Parallel Distrib. Syst."},{"key":"4_CR2","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. MIT Press (2008)"},{"key":"4_CR3","doi-asserted-by":"crossref","unstructured":"Bernat, G., Colin, A., Petters, S.: WCET analysis of probabilistic hard real-time systems. In: RTSS 2002, pp. 279\u2013288. IEEE (2002)","DOI":"10.1109\/REAL.2002.1181582"},{"issue":"4","key":"4_CR4","doi-asserted-by":"publisher","first-page":"857","DOI":"10.1145\/210332.210339","volume":"42","author":"C. Courcoubetis","year":"1995","unstructured":"Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. Journal of the ACM\u00a042(4), 857\u2013907 (1995)","journal-title":"Journal of the ACM"},{"key":"4_CR5","unstructured":"H\u00e4hnel, M.: Energy-utility functions. Diploma thesis, TU Dresden, Germany (2012)"},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"Hamann, C.-J., L\u00f6ser, J., Reuther, L., Sch\u00f6nberg, S., Wolter, J., H\u00e4rtig, H.: Quality-assuring scheduling - using stochastic behavior to improve resource utilization. In: RTSS 2001, pp. 119\u2013128. IEEE (2001)","DOI":"10.1109\/REAL.2001.990603"},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"Haverkort, B.: Performance of Computer Communication Systems: A Model-Based Approach. Wiley (1998)","DOI":"10.1002\/0470841923"},{"issue":"12","key":"4_CR8","doi-asserted-by":"publisher","first-page":"1349","DOI":"10.1109\/TVLSI.2005.862725","volume":"13","author":"S. Irani","year":"2005","unstructured":"Irani, S., Singh, G., Shukla, S.K., Gupta, R.: An overview of the competitive and adversarial approaches to designing dynamic power management strategies. IEEE Trans. VLSI Syst.\u00a013(12), 1349\u20131361 (2005)","journal-title":"IEEE Trans. VLSI Syst."},{"key":"4_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1007\/978-3-540-71209-1_9","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J.-P. Katoen","year":"2007","unstructured":"Katoen, J.-P., Kemna, T., Zapreev, I., Jansen, D.: Bisimulation Minimisation Mostly Speeds Up Probabilistic Model Checking. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol.\u00a04424, pp. 87\u2013101. Springer, Heidelberg (2007)"},{"issue":"2","key":"4_CR10","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1016\/j.peva.2010.04.001","volume":"68","author":"J.-P. Katoen","year":"2011","unstructured":"Katoen, J.-P., Zapreev, I., Hahn, E., Hermanns, H., Jansen, D.: The ins and outs of the probabilistic model checker MRMC. Perform. Eval.\u00a068(2), 90\u2013104 (2011)","journal-title":"Perform. Eval."},{"key":"4_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/978-3-540-71322-7_3","volume-title":"Program Analysis and Compilation, Theory and Practice","author":"S. Knapp","year":"2007","unstructured":"Knapp, S., Paul, W.: Realistic Worst-Case Execution Time Analysis in the Context of Pervasive System Verification. In: Reps, T., Sagiv, M., Bauer, J. (eds.) Program Analysis and Compilation, Theory and Practice. LNCS, vol.\u00a04444, pp. 53\u201381. Springer, Heidelberg (2007)"},{"key":"4_CR12","unstructured":"Kulkarni, V.: Modeling and Analysis of Stochastic Systems. Chapman & Hall (1995)"},{"issue":"2","key":"4_CR13","doi-asserted-by":"publisher","first-page":"128","DOI":"10.1007\/s10009-004-0140-2","volume":"6","author":"M. Kwiatkowska","year":"2004","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Probabilistic symbolic model checking with PRISM: A hybrid approach. STTT\u00a06(2), 128\u2013142 (2004)","journal-title":"STTT"},{"key":"4_CR14","doi-asserted-by":"crossref","unstructured":"Liedtke, J., Islam, N., Jaeger, T., Panteleenko, V., Park, Y.: Irreproducible benchmarks might be sometimes helpful. In: ACM SIGOPS European Workshop, pp. 242\u2013246. ACM (1998)","DOI":"10.1145\/319195.319232"},{"key":"4_CR15","doi-asserted-by":"crossref","unstructured":"Mellor-Crummey, J., Scott, M.: Scalable reader-writer synchronization for shared-memory multiprocessors. In: PPOPP 1991, pp. 106\u2013113. ACM (April 1991)","DOI":"10.1145\/109626.109637"},{"key":"4_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"384","DOI":"10.1007\/978-3-540-24611-4_11","volume-title":"Validation of Stochastic Systems","author":"G. Norman","year":"2004","unstructured":"Norman, G.: Analysing Randomized Distributed Algorithms. In: Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.-P., Siegle, M. (eds.) Validation of Stochastic Systems. LNCS, vol.\u00a02925, pp. 384\u2013418. Springer, Heidelberg (2004)"},{"issue":"2","key":"4_CR17","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"},{"issue":"3","key":"4_CR18","doi-asserted-by":"publisher","first-page":"537","DOI":"10.1137\/0220035","volume":"20","author":"W.K. Shih","year":"1991","unstructured":"Shih, W.K., Liu, J.W.-S., Chung, J.-Y.: Algorithms for scheduling imprecise computations with timing constraints. SIAM J. Comput.\u00a020(3), 537\u2013552 (1991)","journal-title":"SIAM J. Comput."},{"key":"4_CR19","doi-asserted-by":"crossref","unstructured":"Steinberg, U., Kauer, B.: NOVA: a microhypervisor-based secure virtualization architecture. In: EuroSys 2010, pp. 209\u2013222. ACM (2010)","DOI":"10.1145\/1755913.1755935"},{"key":"4_CR20","doi-asserted-by":"crossref","unstructured":"Vardi, M.: Automatic verification of probabilistic concurrent finite-state programs. In: FOCS 1985, pp. 327\u2013338. IEEE (1985)","DOI":"10.1109\/SFCS.1985.12"},{"key":"4_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/3-540-48778-6_16","volume-title":"Formal Methods for Real-Time and Probabilistic Systems","author":"M. Vardi","year":"1999","unstructured":"Vardi, M.: Probabilistic Linear-Time Model Checking: An Overview of the Automata-Theoretic Approach. In: Katoen, J.-P. (ed.) ARTS 1999. LNCS, vol.\u00a01601, pp. 265\u2013276. Springer, Heidelberg (1999)"},{"issue":"3","key":"4_CR22","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1347375.1347389","volume":"7","author":"R. Wilhelm","year":"2008","unstructured":"Wilhelm, R., Engblom, J., Ermedahl, A., Holsti, N., Thesing, S., Whalley, D., Bernat, G., Ferdinand, C., Heckmann, R., Mitra, T., Mueller, F., Puaut, I., Puschner, P., Staschulat, J., Stenstr\u00f6m, P.: The worst-case execution-time problem - overview of methods and survey of tools. Trans. Embedded Comput. Syst.\u00a07(3), 1\u201353 (2008)","journal-title":"Trans. Embedded Comput. Syst."},{"issue":"4","key":"4_CR23","doi-asserted-by":"publisher","first-page":"393","DOI":"10.1145\/1189256.1189259","volume":"24","author":"J. Yang","year":"2006","unstructured":"Yang, J., Twohey, P., Engler, D., Musuvathi, M.: Using model checking to find serious file system errors. ACM Trans. Comput. Syst.\u00a024(4), 393\u2013423 (2006)","journal-title":"ACM Trans. Comput. Syst."}],"container-title":["Lecture Notes in Computer Science","Formal Methods for Industrial Critical Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-32469-7_4.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,4,7]],"date-time":"2025-04-07T01:35:47Z","timestamp":1743989747000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-32469-7_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642324680","9783642324697"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-32469-7_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}