{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,29]],"date-time":"2026-07-29T10:55:12Z","timestamp":1785322512242,"version":"3.55.0"},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642362484","type":"print"},{"value":"9783642362491","type":"electronic"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"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":[[2013]]},"DOI":"10.1007\/978-3-642-36249-1_2","type":"book-chapter","created":{"date-parts":[[2013,1,15]],"date-time":"2013-01-15T00:59:05Z","timestamp":1358211545000},"page":"30-59","source":"Crossref","is-referenced-by-count":29,"title":["Probabilistic Verification at Runtime for Self-Adaptive Systems"],"prefix":"10.1007","author":[{"given":"Antonio","family":"Filieri","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Giordano","family":"Tamburrelli","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","reference":[{"key":"2_CR1","doi-asserted-by":"crossref","unstructured":"Andova, S., Hermanns, H., Katoen, J.P.: Discrete-time rewards model-checked. Formal Modeling and Analysis of Timed Systems, 88\u2013104 (2004)","DOI":"10.1007\/978-3-540-40903-8_8"},{"key":"2_CR2","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/3-540-60045-0_48","volume-title":"Computer Aided Verification","author":"A. Aziz","year":"1995","unstructured":"Aziz, A., Singhal, V., Balarin, F., Brayton, R., Sangiovanni-Vincentelli, A.: It usually works: The temporal logic of stochastic systems. In: Computer Aided Verification, pp. 155\u2013165. Springer, Heidelberg (1995)"},{"issue":"2","key":"2_CR3","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1016\/j.entcs.2005.10.034","volume":"153","author":"C. Baier","year":"2006","unstructured":"Baier, C., D\u2019Argenio, P., Groesser, M.: Partial order reduction for probabilistic branching time. Electronic Notes in Theoretical Computer Science\u00a0153(2), 97\u2013116 (2006)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"2_CR4","doi-asserted-by":"publisher","first-page":"524","DOI":"10.1109\/TSE.2003.1205180","volume":"29","author":"C. Baier","year":"2003","unstructured":"Baier, C., Haverkort, B., Hermanns, H., Katoen, J.-P.: Model-checking algorithms for continuous-time markov chains. IEEE Transactions on Software Engineering\u00a029, 524\u2013541 (2003)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"2_CR5","volume-title":"Principles of Model Checking","author":"C. Baier","year":"2008","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. The MIT Press (2008)"},{"issue":"10","key":"2_CR6","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1109\/MC.2006.362","volume":"39","author":"L. Baresi","year":"2006","unstructured":"Baresi, L., Di Nitto, E., Ghezzi, C.: Toward open-world software: Issue and challenges. Computer\u00a039(10), 36\u201343 (2006)","journal-title":"Computer"},{"key":"2_CR7","unstructured":"Calinescu, R., Grunske, L., Kwiatkowska, M., Mirandola, R., Tamburrelli, G.: Dynamic qos management and optimisation in service-based systems. IEEE Transactions on Software Engineering\u00a0(99), 1 (2010)"},{"issue":"2","key":"2_CR8","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1109\/TSE.1980.234477","volume":"6","author":"R.C. Cheung","year":"1980","unstructured":"Cheung, R.C.: A user-oriented software reliability model. IEEE Trans. Softw. Eng.\u00a06(2), 118\u2013125 (1980)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"2_CR9","doi-asserted-by":"crossref","unstructured":"Courcoubetis, C., Yannakakis, M.: The complexity of probabilistic verification. J. ACM\u00a042(4) (1995)","DOI":"10.1145\/210332.210339"},{"key":"2_CR10","doi-asserted-by":"crossref","unstructured":"Davis, T.A.: Direct methods for sparse linear systems. Society for Industrial Mathematics, vol.\u00a02 (2006)","DOI":"10.1137\/1.9780898718881"},{"key":"2_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"280","DOI":"10.1007\/978-3-540-31862-0_21","volume-title":"Theoretical Aspects of Computing - ICTAC 2004","author":"C. Daws","year":"2005","unstructured":"Daws, C.: Symbolic and parametric model checking of discrete-time markov chains. In: Liu, Z., Araki, K. (eds.) ICTAC 2004. LNCS, vol.\u00a03407, pp. 280\u2013294. Springer, Heidelberg (2005)"},{"key":"2_CR12","doi-asserted-by":"crossref","unstructured":"Filieri, A., Ghezzi, C., Tamburrelli, G.: Run-time efficient probabilistic model checking. In: 33rd International Conference on Software Engineering (ICSE 2011) (accepted for publication)","DOI":"10.1145\/1985793.1985840"},{"key":"2_CR13","unstructured":"Antonio Filieri and Carlo Ghezzi. Further steps towards efficient runtime verification: Handling probabilistic cost models. In Formal Methods in Software Engineering: Rigorous and Agile Approaches (FormSERA), Zurich, 2012."},{"issue":"2-3","key":"2_CR14","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1016\/S0166-5316(01)00034-7","volume":"45","author":"K. Goseva-Popstojanova","year":"2001","unstructured":"Goseva-Popstojanova, K., Trivedi, K.S.: Architecture-based approach to reliability assessment of software systems. Performance Evaluation\u00a045(2-3), 179\u2013204 (2001)","journal-title":"Performance Evaluation"},{"key":"2_CR15","unstructured":"Grinstead, C.M., Snell, J.L.: Introduction to Probability. Amer Mathematical Society (1997)"},{"key":"2_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1007\/978-3-540-78499-9_20","volume-title":"Foundations of Software Science and Computational Structures","author":"H. Gruber","year":"2008","unstructured":"Gruber, H., Johannsen, J.: Optimal Lower Bounds on Regular Expression Size Using Communication Complexity. In: Amadio, R.M. (ed.) FOSSACS 2008. LNCS, vol.\u00a04962, pp. 273\u2013286. Springer, Heidelberg (2008)"},{"key":"2_CR17","doi-asserted-by":"crossref","unstructured":"Grunske, L.: Specification patterns for probabilistic quality properties. In: ICSE, pp. 31\u201340 (2008)","DOI":"10.1145\/1368088.1368094"},{"key":"2_CR18","doi-asserted-by":"crossref","unstructured":"Hahn, E., Hermanns, H., Zhang, L.: Probabilistic reachability for parametric markov models. In: Model Checking Software, pp. 88\u2013106 (2009)","DOI":"10.1007\/978-3-642-02652-2_10"},{"issue":"5","key":"2_CR19","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H. Hansson","year":"1994","unstructured":"Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal aspects of computing\u00a06(5), 512\u2013535 (1994)","journal-title":"Formal aspects of computing"},{"key":"2_CR20","unstructured":"Hopcroft, J.E., Motwani, R., Ullman, J.D.: Introduction to automata theory, languages, and computation. Addison-Wesley (2007)"},{"issue":"1","key":"2_CR21","doi-asserted-by":"publisher","first-page":"49","DOI":"10.1007\/s10270-006-0040-x","volume":"7","author":"A. Immonen","year":"2008","unstructured":"Immonen, A., Niemel\u00e4, E.: Survey of reliability and availability prediction methods from the viewpoint of software architecture. Software and Systems Modeling\u00a07(1), 49\u201365 (2008)","journal-title":"Software and Systems Modeling"},{"key":"2_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1007\/978-3-540-77966-7_9","volume-title":"Hardware and Software: Verification and Testing","author":"D.N. Jansen","year":"2008","unstructured":"Jansen, D.N., Katoen, J.-P., Oldenkamp, M., Stoelinga, M., Zapreev, I.: How Fast and Fat Is Your Probabilistic Model Checker? An Experimental Performance Comparison. In: Yorav, K. (ed.) HVC 2007. LNCS, vol.\u00a04899, pp. 69\u201385. Springer, Heidelberg (2008)"},{"key":"2_CR23","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.N.: 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)"},{"key":"2_CR24","doi-asserted-by":"crossref","unstructured":"Kramer, J., Magee, J.: Self-managed systems: An architectural challenge. In: Future of Software Engineering, FOSE 2007, pp. 259\u2013268. IEEE (2007)","DOI":"10.1109\/FOSE.2007.19"},{"key":"2_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"220","DOI":"10.1007\/978-3-540-72522-0_6","volume-title":"Formal Methods for Performance Evaluation","author":"M. Kwiatkowska","year":"2007","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Stochastic Model Checking. In: Bernardo, M., Hillston, J. (eds.) SFM 2007. LNCS, vol.\u00a04486, pp. 220\u2013270. Springer, Heidelberg (2007)"},{"key":"2_CR26","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M.Z., Parker, D., Qu, H.: Incremental quantitative verification for markov decision processes. In: DSN, pp. 359\u2013370 (2011)","DOI":"10.1109\/DSN.2011.5958249"},{"key":"2_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"492","DOI":"10.1007\/978-3-642-17322-6_21","volume-title":"Graph Transformations and Model-Driven Engineering","author":"M. Caporuscio","year":"2010","unstructured":"Caporuscio, M., Funaro, M., Ghezzi, C.: Architectural Issues of Adaptive Pervasive Systems. In: Engels, G., Lewerentz, C., Sch\u00e4fer, W., Sch\u00fcrr, A., Westfechtel, B. (eds.) Nagl Festschrift. LNCS, vol.\u00a05765, pp. 492\u2013511. Springer, Heidelberg (2010)"},{"key":"2_CR28","doi-asserted-by":"crossref","unstructured":"Quarteroni, A., Sacco, R., Saleri, F.: Numerical mathematics, vol.\u00a037. Springer (2007)","DOI":"10.1007\/b98885"},{"key":"2_CR29","volume-title":"Stochastic Processes","author":"S.M. Ross","year":"1996","unstructured":"Ross, S.M.: Stochastic Processes. Wiley, New York (1996)"},{"key":"2_CR30","doi-asserted-by":"crossref","unstructured":"Saad, Y.: Iterative methods for sparse linear systems. Society for Industrial Mathematics (2003)","DOI":"10.1137\/1.9780898718003"}],"container-title":["Lecture Notes in Computer Science","Assurances for Self-Adaptive Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-36249-1_2","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,10]],"date-time":"2019-05-10T14:45:54Z","timestamp":1557499554000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-36249-1_2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642362484","9783642362491"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-36249-1_2","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013]]}}}