{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,14]],"date-time":"2025-06-14T05:23:46Z","timestamp":1749878626660},"publisher-location":"Cham","reference-count":74,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319741826"},{"type":"electronic","value":"9783319741833"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-74183-3_8","type":"book-chapter","created":{"date-parts":[[2018,1,17]],"date-time":"2018-01-17T13:02:43Z","timestamp":1516194163000},"page":"223-248","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Using Runtime Quantitative Verification to Provide Assurance Evidence for Self-Adaptive Software"],"prefix":"10.1007","author":[{"given":"Radu","family":"Calinescu","sequence":"first","affiliation":[]},{"given":"Simos","family":"Gerasimou","sequence":"additional","affiliation":[]},{"given":"Kenneth","family":"Johnson","sequence":"additional","affiliation":[]},{"given":"Colin","family":"Paterson","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,1,18]]},"reference":[{"issue":"1","key":"8_CR1","doi-asserted-by":"crossref","first-page":"46","DOI":"10.1145\/2728816.2728827","volume":"2","author":"R Alur","year":"2015","unstructured":"Alur, R., Henzinger, T.A., Vardi, M.Y.: Theory in practice for system design and verification. ACM SIGLOG News 2(1), 46\u201351 (2015)","journal-title":"ACM SIGLOG News"},{"issue":"6","key":"8_CR2","doi-asserted-by":"crossref","first-page":"369","DOI":"10.1109\/TSE.2007.1011","volume":"33","author":"D Ardagna","year":"2007","unstructured":"Ardagna, D., Pernici, B.: Adaptive service composition in flexible processes. IEEE Trans. Softw. Eng. 33(6), 369\u2013384 (2007)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"1","key":"8_CR3","doi-asserted-by":"crossref","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 1(1), 162\u2013170 (2000)","journal-title":"ACM Trans. Comput. Logic"},{"key":"8_CR4","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.-P.: Principles of Model Checking. The MIT Press, Cambridge (2008)"},{"key":"8_CR5","unstructured":"Bianculli, D., Filieri, A., Ghezzi, C., Mandrioli, D.: A syntactic-semantic approach to incremental verification. CoRR, abs\/1304.8034 (2013)"},{"issue":"1","key":"8_CR6","doi-asserted-by":"crossref","first-page":"47","DOI":"10.1016\/j.scico.2013.11.026","volume":"97","author":"D Bianculli","year":"2015","unstructured":"Bianculli, D., Filieri, A., Ghezzi, C., Mandrioli, D.: Syntactic-semantic incrementality for agile verification. Sci. Comput. Program. 97(1), 47\u201354 (2015)","journal-title":"Sci. Comput. Program."},{"key":"8_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1007\/978-3-642-36249-1_11","volume-title":"Assurances for Self-Adaptive Systems: Principles, Models, and Techniques","author":"R Calinescu","year":"2013","unstructured":"Calinescu, R.: Emerging techniques for the engineering of self-adaptive high-integrity software. In: C\u00e1mara, J., de Lemos, R., Ghezzi, C., Lopes, A. (eds.) Assurances for Self-Adaptive Systems: Principles, Models, and Techniques. LNCS, vol. 7740, pp. 297\u2013310. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36249-1_11"},{"key":"8_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"235","DOI":"10.1007\/978-3-662-46675-9_16","volume-title":"Fundamental Approaches to Software Engineering","author":"R Calinescu","year":"2015","unstructured":"Calinescu, R., Gerasimou, S., Banks, A.: Self-adaptive software with decentralised control loops. In: Egyed, A., Schaefer, I. (eds.) FASE 2015. LNCS, vol. 9033, pp. 235\u2013251. Springer, Heidelberg (2015). https:\/\/doi.org\/10.1007\/978-3-662-46675-9_16"},{"issue":"99","key":"8_CR9","first-page":"1","volume":"PP","author":"R Calinescu","year":"2015","unstructured":"Calinescu, R., Ghezzi, C., Johnson, K., Pezze, M., Rafiq, Y., Tamburrelli, G.: Formal verification with confidence intervals to establish quality of service properties of software systems. IEEE Trans. Reliab. PP(99), 1\u201319 (2015)","journal-title":"IEEE Trans. Reliab."},{"issue":"9","key":"8_CR10","doi-asserted-by":"crossref","first-page":"69","DOI":"10.1145\/2330667.2330686","volume":"55","author":"R Calinescu","year":"2012","unstructured":"Calinescu, R., Ghezzi, C., Kwiatkowska, M., Mirandola, R.: Self-adaptive software needs quantitative verification at runtime. Commun. ACM 55(9), 69\u201377 (2012)","journal-title":"Commun. ACM"},{"issue":"3","key":"8_CR11","doi-asserted-by":"crossref","first-page":"387","DOI":"10.1109\/TSE.2010.92","volume":"37","author":"R Calinescu","year":"2011","unstructured":"Calinescu, R., Grunske, L., Kwiatkowska, M., Mirandola, R., Tamburrelli, G.: Dynamic QoS management and optimization in service-based systems. IEEE Trans. Softw. Eng. 37(3), 387\u2013409 (2011)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"8_CR12","doi-asserted-by":"crossref","unstructured":"Calinescu, R., Johnson, K., Paterson, C.: FACT: a probabilistic model checker for formal verification with confidence intervals. In: 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS) (2016)","DOI":"10.1007\/978-3-662-49674-9_32"},{"key":"8_CR13","doi-asserted-by":"crossref","unstructured":"Calinescu, R., Johnson, K., Rafiq, Y.: Using observation ageing to improve Markovian model learning in QoS engineering. In: 2nd ACM\/SPEC International Conference on Performance Engineering (ICPE 2011), pp. 505\u2013510 (2011)","DOI":"10.1145\/1958746.1958823"},{"key":"8_CR14","doi-asserted-by":"crossref","unstructured":"Calinescu, R., Johnson, K., Rafiq, Y.: Developing self-verifying service-based systems. In: 28th IEEE\/ACM International Conference on Automated Software Engineering (ASE 2013), pp. 734\u2013737 (2013)","DOI":"10.1109\/ASE.2013.6693145"},{"key":"8_CR15","unstructured":"Calinescu, R., Johnson, K., Rafiq, Y.: Using continual verification to automate service selection in service-based systems. Technical report YCS-2013-484, Department of Computer Science, University of York (2013). http:\/\/www.cs.york.ac.uk\/ftpdir\/reports\/2013\/YCS\/484\/YCS-2013-484.pdf"},{"key":"8_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-642-21292-5_7","volume-title":"Foundations of Computer Software. Modeling, Development, and Verification of Adaptive Systems","author":"R Calinescu","year":"2011","unstructured":"Calinescu, R., Kikuchi, S.: Formal methods @ runtime. In: Calinescu, R., Jackson, E. (eds.) Monterey Workshop 2010. LNCS, vol. 6662, pp. 122\u2013135. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-21292-5_7"},{"key":"8_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1007\/978-3-642-34059-8_16","volume-title":"Large-Scale Complex IT Systems. Development, Operation and Management","author":"R Calinescu","year":"2012","unstructured":"Calinescu, R., Kikuchi, S., Johnson, K.: Compositional reverification of probabilistic safety properties for large-scale complex IT systems. In: Calinescu, R., Garlan, D. (eds.) Monterey Workshop 2012. LNCS, vol. 7539, pp. 303\u2013329. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-34059-8_16"},{"key":"8_CR18","doi-asserted-by":"crossref","unstructured":"Calinescu, R., Kwiatkowska, M.: Using quantitative analysis to implement autonomic IT systems. In: 31st IEEE International Conference on Software Engineering (ICSE 2009), pp. 100\u2013110 (2009)","DOI":"10.1109\/ICSE.2009.5070512"},{"key":"8_CR19","doi-asserted-by":"crossref","unstructured":"Calinescu, R., Rafiq, Y., Johnson, K., Bakir, M.E.: Adaptive model learning for continual verification of non-functional properties. In: 5th ACM\/SPEC International Conference on Performance Engineering (ICPE 2014), pp. 87\u201398 (2014)","DOI":"10.1145\/2568088.2568094"},{"key":"8_CR20","doi-asserted-by":"crossref","unstructured":"C\u00e1mara, J., de Lemos, R.: Evaluation of resilience in self-adaptive systems using probabilistic model-checking. In: 2012 ICSE Workshop on Software Engineering for Adaptive and Self-Managing Systems (SEAMS), pp. 53\u201362, June 2012","DOI":"10.1109\/SEAMS.2012.6224391"},{"key":"8_CR21","doi-asserted-by":"crossref","unstructured":"C\u00e1mara, J., Garlan, D., Schmerl, B., Pandey, A.: Optimal planning for architecture-based self-adaptation via model checking of stochastic games. In: Proceedings of the 10th DADS Track of the 30th ACM Symposium on Applied Computing, Salamanca, Spain, 13\u201317 April 2015","DOI":"10.1145\/2695664.2695680"},{"key":"8_CR22","doi-asserted-by":"crossref","unstructured":"C\u00e1mara, J., Moreno, G.A., Garlan, D.: Stochastic game analysis and latency awareness for proactive self-adaptation. In: Proceedings of the 9th International Symposium on Software Engineering for Adaptive and Self-Managing Systems, SEAMS 2014, pp. 155\u2013164. ACM, New York (2014)","DOI":"10.1145\/2593929.2593933"},{"issue":"5","key":"8_CR23","doi-asserted-by":"crossref","first-page":"1138","DOI":"10.1109\/TSE.2011.68","volume":"38","author":"V Cardellini","year":"2012","unstructured":"Cardellini, V., Casalicchio, E., Grassi, V., Iannucci, S., Lo Presti, F., Mirandola, R.: Moses: a framework for QoS driven runtime adaptation of service-oriented systems. IEEE Trans. Softw. Eng. 38(5), 1138\u20131159 (2012)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"2","key":"8_CR24","doi-asserted-by":"crossref","first-page":"118","DOI":"10.1109\/TSE.1980.234477","volume":"6","author":"R Cheung","year":"1980","unstructured":"Cheung, R.: A user-oriented software reliability model. IEEE Trans. Softw. Eng. 6(2), 118\u2013125 (1980)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"4","key":"8_CR25","doi-asserted-by":"crossref","first-page":"328","DOI":"10.1109\/TSE.2005.52","volume":"31","author":"D Coppit","year":"2005","unstructured":"Coppit, D., Yang, J., Khurshid, S., Le, W., Sullivan, K.: Software assurance by bounded exhaustive testing. IEEE Trans. Softw. Eng. 31(4), 328\u2013339 (2005)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"8_CR26","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. 3407, pp. 280\u2013294. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-31862-0_21"},{"key":"8_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-35813-5_1","volume-title":"Software Engineering for Self-Adaptive Systems II","author":"R Lemos de","year":"2013","unstructured":"de Lemos, R., et al.: Software engineering for self-adaptive systems: a second research roadmap. In: de Lemos, R., Giese, H., M\u00fcller, H.A., Shaw, M. (eds.) Software Engineering for Self-Adaptive Systems II. LNCS, vol. 7475, pp. 1\u201332. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-35813-5_1"},{"key":"8_CR28","doi-asserted-by":"crossref","unstructured":"D\u2019Ippolito, N., Braberman, V., Kramer, J., Magee, J., Sykes, D., Uchitel, S.: Hope for the best, prepare for the worst: multi-tier control for adaptive systems. In: Proceedings of the 36th International Conference on Software Engineering, ICSE 2014, pp. 688\u2013699. ACM, New York (2014)","DOI":"10.1145\/2568225.2568264"},{"key":"8_CR29","doi-asserted-by":"crossref","unstructured":"D\u2019Ippolito, N., Braberman, V., Piterman, N., Uchitel, S.: Synthesis of live behaviour models for fallible domains. In: 33rd International Conference on Software Engineering (ICSE), pp. 211\u2013220, May 2011","DOI":"10.1145\/1985793.1985823"},{"key":"8_CR30","doi-asserted-by":"crossref","unstructured":"D\u2019Ippolito, N.R., Braberman, V., Piterman, N., Uchitel, S.: Synthesis of live behaviour models. In: Proceedings of the Eighteenth ACM SIGSOFT International Symposium on Foundations of Software Engineering, FSE 2010, pp. 77\u201386. ACM, New York (2010)","DOI":"10.1145\/1882291.1882305"},{"key":"8_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"531","DOI":"10.1007\/978-3-642-54862-8_44","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"K Dr\u00e4ger","year":"2014","unstructured":"Dr\u00e4ger, K., Forejt, V., Kwiatkowska, M., Parker, D., Ujma, M.: Permissive controller synthesis for probabilistic systems. In: \u00c1brah\u00e1m, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 531\u2013546. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54862-8_44"},{"key":"8_CR32","doi-asserted-by":"crossref","unstructured":"Dubslaff, C., Kl\u00fcppelholz, S., Baier, C.: Probabilistic model checking for energy analysis in software product lines. In: Proceedings of the 13th International Conference on Modularity, MODULARITY 2014, pp. 169\u2013180. ACM, New York (2014)","DOI":"10.1145\/2577080.2577095"},{"key":"8_CR33","doi-asserted-by":"crossref","unstructured":"Epifani, I., Ghezzi, C., Mirandola, R., Tamburrelli, G.: Model evolution by run-time parameter adaptation. In: 31st IEEE International Conference on Software Engineering (ICSE 2009), pp. 111\u2013121 (2009)","DOI":"10.1109\/ICSE.2009.5070513"},{"key":"8_CR34","doi-asserted-by":"crossref","unstructured":"Filieri, A., Ghezzi, C.: Further steps towards efficient runtime verification: handling probabilistic cost models. In: Formal Methods Software Engineering: Rigorous and Agile Approaches (FormSERA 2012), pp. 2\u20138 (2012)","DOI":"10.1109\/FormSERA.2012.6229785"},{"key":"8_CR35","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), pp. 341\u2013350 (2011)","DOI":"10.1145\/1985793.1985840"},{"issue":"2","key":"8_CR36","doi-asserted-by":"crossref","first-page":"163","DOI":"10.1007\/s00165-011-0207-2","volume":"24","author":"A Filieri","year":"2012","unstructured":"Filieri, A., Ghezzi, C., Tamburrelli, G.: A formal approach to adaptive software: continuous assurance of non-functional requirements. Formal Aspects Comput. 24(2), 163\u2013186 (2012)","journal-title":"Formal Aspects Comput."},{"key":"8_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1007\/978-3-642-36249-1_2","volume-title":"Assurances for Self-Adaptive Systems: Principles, Models, and Techniques","author":"A Filieri","year":"2013","unstructured":"Filieri, A., Tamburrelli, G.: Probabilistic verification at runtime for self-adaptive systems. In: C\u00e1mara, J., de Lemos, R., Ghezzi, C., Lopes, A. (eds.) Assurances for Self-Adaptive Systems: Principles, Models, and Techniques. LNCS, vol. 7740, pp. 30\u201359. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36249-1_2"},{"key":"8_CR38","doi-asserted-by":"crossref","unstructured":"Forejt, V., Kwiatkowska, M., Parker, D., Qu, H., Ujma, M.: Incremental runtime verification of probabilistic systems. Technical report RR-12-05, Department of Computer Science, University of Oxford (2012)","DOI":"10.1007\/978-3-642-35632-2_30"},{"key":"8_CR39","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"314","DOI":"10.1007\/978-3-642-35632-2_30","volume-title":"Runtime Verification","author":"V Forejt","year":"2013","unstructured":"Forejt, V., Kwiatkowska, M., Parker, D., Qu, H., Ujma, M.: Incremental runtime verification of probabilistic systems. In: Qadeer, S., Tasiran, S. (eds.) RV 2012. LNCS, vol. 7687, pp. 314\u2013319. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-35632-2_30"},{"key":"8_CR40","doi-asserted-by":"crossref","unstructured":"Gerasimou, S., Calinescu, R., Banks, A.: Efficient runtime quantitative verification using caching, lookahead, and nearly-optimal reconfiguration. In: 9th International Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS 2014), pp. 115\u2013124 (2014)","DOI":"10.1145\/2593929.2593932"},{"key":"8_CR41","doi-asserted-by":"crossref","unstructured":"Gerasimou, S., Tamburrelli, G., Calinescu, R.: Search-based synthesis of probabilistic models for quality-of-service software engineering. In: 30th IEEE\/ACM International Conference on Automated Software Engineering (ASE), pp. 319\u2013330, November 2015","DOI":"10.1109\/ASE.2015.22"},{"key":"8_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/978-3-642-34059-8_19","volume-title":"Large-Scale Complex IT Systems. Development, Operation and Management","author":"C Ghezzi","year":"2012","unstructured":"Ghezzi, C.: Evolution, adaptation, and the quest for incrementality. In: Calinescu, R., Garlan, D. (eds.) Monterey Workshop 2012. LNCS, vol. 7539, pp. 369\u2013379. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-34059-8_19"},{"key":"8_CR43","doi-asserted-by":"crossref","unstructured":"Ghezzi, C., Greenyer, J., La Manna, V.P.: Synthesizing dynamically updating controllers from changes in scenario-based specifications. In: Proceedings of the 7th International Symposium on Software Engineering for Adaptive and Self-Managing Systems, SEAMS 2012, pp. 145\u2013154. IEEE Press, Piscataway (2012)","DOI":"10.1109\/SEAMS.2012.6224401"},{"key":"8_CR44","doi-asserted-by":"crossref","unstructured":"Ghezzi, C., Pezz\u00e8, M., Sama, M., Tamburrelli, G.: Mining behavior models from user-intensive web applications. In: 36th International Conference on Software Engineering (ICSE 2014), pp. 277\u2013287 (2014)","DOI":"10.1145\/2568225.2568234"},{"issue":"1","key":"8_CR45","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1007\/s10009-010-0146-x","volume":"13","author":"E Hahn","year":"2011","unstructured":"Hahn, E., Hermanns, H., Zhang, L.: Probabilistic reachability for parametric Markov models. Int. J. Softw. Tools Technol. Transfer 13(1), 3\u201319 (2011)","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"8_CR46","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/978-3-642-20398-5_12","volume-title":"NASA Formal Methods","author":"EM Hahn","year":"2011","unstructured":"Hahn, E.M., Han, T., Zhang, L.: Synthesis for PCTL in parametric Markov decision processes. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 146\u2013161. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-20398-5_12"},{"key":"8_CR47","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"660","DOI":"10.1007\/978-3-642-14295-6_56","volume-title":"Computer Aided Verification","author":"EM Hahn","year":"2010","unstructured":"Hahn, E.M., Hermanns, H., Wachter, B., Zhang, L.: PARAM: a model checker for parametric Markov models. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 660\u2013664. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_56"},{"key":"8_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/978-3-642-02652-2_10","volume-title":"Model Checking Software","author":"EM Hahn","year":"2009","unstructured":"Hahn, E.M., Hermanns, H., Zhang, L.: Probabilistic reachability for parametric Markov models. In: P\u0103s\u0103reanu, C.S. (ed.) SPIN 2009. LNCS, vol. 5578, pp. 88\u2013106. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02652-2_10"},{"issue":"1","key":"8_CR49","doi-asserted-by":"crossref","first-page":"11:1","DOI":"10.1145\/2379776.2379787","volume":"45","author":"M Harman","year":"2012","unstructured":"Harman, M., Mansouri, S.A., Zhang, Y.: Search-based software engineering: trends, techniques and applications. ACM Comput. Surv. 45(1), 11:1\u201311:61 (2012)","journal-title":"ACM Comput. Surv."},{"issue":"10","key":"8_CR50","doi-asserted-by":"crossref","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare, C.A.R.: An axiomatic basis for computer programming. Commun. ACM 12(10), 576\u2013580 (1969)","journal-title":"Commun. ACM"},{"key":"8_CR51","doi-asserted-by":"crossref","unstructured":"Johnson, K., Calinescu, R., Kikuchi, S.: An incremental verification framework for component-based software systems. In: 16th International Symposium on Component-Based Software Engineering (CBSE 2013), pp. 33\u201342 (2013)","DOI":"10.1145\/2465449.2465456"},{"issue":"2","key":"8_CR52","doi-asserted-by":"crossref","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.S., Hahn, E.M., Hermanns, H., Jansen, D.N.: The ins and outs of the probabilistic model checker MRMC. Perform. Eval. 68(2), 90\u2013104 (2011)","journal-title":"Perform. Eval."},{"issue":"1","key":"8_CR53","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1109\/MC.2003.1160055","volume":"36","author":"J Kephart","year":"2003","unstructured":"Kephart, J., Chess, D.: The vision of autonomic computing. Computer 36(1), 41\u201350 (2003)","journal-title":"Computer"},{"key":"8_CR54","doi-asserted-by":"crossref","unstructured":"Komuravelli, A., Pasareanu, C.S., Clarke, E.M.: Learning probabilistic systems from tree samples. In: 27th IEEE\/ACM Symposium on Logic in Computer Science (LICS 2012), pp. 441\u2013450 (2012)","DOI":"10.1109\/LICS.2012.54"},{"key":"8_CR55","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M.: Quantitative verification: models, techniques and tools. In: 6th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC\/FSE 2007), pp. 449\u2013458 (2007)","DOI":"10.1145\/1295014.1295018"},{"key":"8_CR56","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585\u2013591. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47"},{"key":"8_CR57","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1007\/978-3-642-12002-2_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M Kwiatkowska","year":"2010","unstructured":"Kwiatkowska, M., Norman, G., Parker, D., Qu, H.: Assume-guarantee verification for probabilistic systems. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 23\u201337. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-12002-2_3"},{"issue":"1","key":"8_CR58","doi-asserted-by":"crossref","first-page":"33","DOI":"10.1007\/s10703-006-0005-2","volume":"29","author":"M Kwiatkowska","year":"2006","unstructured":"Kwiatkowska, M., Norman, G., Parker, D., Sproston, J.: Performance analysis of probabilistic timed automata using digital clocks. Formal Methods Syst. Des. 29(1), 33\u201378 (2006)","journal-title":"Formal Methods Syst. Des."},{"key":"8_CR59","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Parker, D., Qu, H.: Incremental quantitative verification for Markov decision processes. In: 41st IEEE\/IFIP International Conference on Dependable Systems Networks (DSN 2011), pp. 359\u2013370 (2011)","DOI":"10.1109\/DSN.2011.5958249"},{"key":"8_CR60","doi-asserted-by":"crossref","unstructured":"Meedeniya, I., Grunske, L.: An efficient method for architecture-based reliability evaluation for evolving systems with changing parameters. In: 21st IEEE International Symposium on Software Reliability Engineering (ISSRE 2010), pp. 229\u2013238 (2010)","DOI":"10.1109\/ISSRE.2010.19"},{"issue":"5","key":"8_CR61","doi-asserted-by":"crossref","first-page":"591","DOI":"10.1109\/TSE.2012.53","volume":"39","author":"V Nallur","year":"2013","unstructured":"Nallur, V., Bahsoon, R.: A decentralized self-adaptation mechanism for service-based applications in the cloud. IEEE Trans. Softw. Eng. 39(5), 591\u2013612 (2013)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"8_CR62","doi-asserted-by":"crossref","unstructured":"Naskos, A., Stachtiari, E., Gounaris, A., Katsaros, P., Tsoumakos, D., Konstantinou, I., Sioutas, S.: Dependable horizontal scaling based on probabilistic model checking. In: 15th IEEE\/ACM International Symposium on Cluster, Cloud and Grid Computing (CCGrid 2015) (2015)","DOI":"10.1109\/CCGrid.2015.91"},{"key":"8_CR63","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/978-3-642-82453-1_5","volume-title":"Logics and Models of Concurrent Systems","author":"A Pnueli","year":"1985","unstructured":"Pnueli, A.: In transition from global to modular temporal reasoning about programs. In: Apt, K.R. (ed.) Logics and Models of Concurrent Systems, pp. 123\u2013144. Springer, New York (1985). https:\/\/doi.org\/10.1007\/978-3-642-82453-1_5"},{"issue":"2","key":"8_CR64","first-page":"250","volume":"2","author":"R Segala","year":"1995","unstructured":"Segala, R., Lynch, N.A.: Probabilistic simulations for probabilistic processes. Nord. J. Comput. 2(2), 250\u2013273 (1995)","journal-title":"Nord. J. Comput."},{"key":"8_CR65","doi-asserted-by":"crossref","unstructured":"Sen, K., Viswanathan, M., Agha, G.: Learning continuous time Markov chains from sample executions. In: Quantitative Evaluation of Systems, pp. 146\u2013155 (2004)","DOI":"10.1109\/QEST.2004.1348029"},{"key":"8_CR66","doi-asserted-by":"crossref","unstructured":"Sykes, D., Magee, J., Kramer, J.: Flashmob: distributed adaptive self-assembly. In: 6th International Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS 2011), pp. 100\u2013109 (2011)","DOI":"10.1145\/1988008.1988023"},{"key":"8_CR67","doi-asserted-by":"crossref","unstructured":"Weyns, D., Calinescu, R.: Tele assistance system: an examplar for self-adaptive service-based systems. In: 10th International Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS 2015) (2015, to appear)","DOI":"10.1109\/SEAMS.2015.27"},{"issue":"1","key":"8_CR68","doi-asserted-by":"crossref","first-page":"3:1","DOI":"10.1145\/1671948.1671951","volume":"5","author":"D Weyns","year":"2010","unstructured":"Weyns, D., Haesevoets, R., Helleboogh, A., Holvoet, T., Joosen, W.: The MACODO middleware for context-driven dynamic agent organizations. ACM Trans. Auton. Adapt. Syst. 5(1), 3:1\u20133:28 (2010)","journal-title":"ACM Trans. Auton. Adapt. Syst."},{"key":"8_CR69","doi-asserted-by":"crossref","unstructured":"Weyns, D., Malek, S., Andersson, J.: On decentralized self-adaptation: lessons from the trenches and challenges for the future. In: 5th International Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS 2010), pp. 84\u201393 (2010)","DOI":"10.1145\/1808984.1808994"},{"key":"8_CR70","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1007\/978-3-642-35813-5_4","volume-title":"Software Engineering for Self-Adaptive Systems II","author":"D Weyns","year":"2013","unstructured":"Weyns, D., et al.: On patterns for decentralized control in self-adaptive systems. In: de Lemos, R., Giese, H., M\u00fcller, H.A., Shaw, M. (eds.) Software Engineering for Self-Adaptive Systems II. LNCS, vol. 7475, pp. 76\u2013107. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-35813-5_4"},{"key":"8_CR71","doi-asserted-by":"crossref","unstructured":"Wongpiromsarn, T., Ulusoy, A., Belta, C., Frazzoli, E., Rus, D.: Incremental synthesis of control policies for heterogeneous multi-agent systems with linear temporal logic specifications. In: 2013 IEEE International Conference on Robotics and Automation (ICRA), pp. 5011\u20135018, May 2013","DOI":"10.1109\/ICRA.2013.6631293"},{"issue":"4","key":"8_CR72","doi-asserted-by":"crossref","first-page":"19:1","DOI":"10.1145\/1592434.1592436","volume":"41","author":"J Woodcock","year":"2009","unstructured":"Woodcock, J., Larsen, P.G., Bicarregui, J., Fitzgerald, J.: Formal methods: practice and experience. ACM Comput. Surv. 41(4), 19:1\u201319:36 (2009)","journal-title":"ACM Comput. Surv."},{"key":"8_CR73","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":"HLS Younes","year":"2005","unstructured":"Younes, H.L.S.: Ymer: a statistical model checker. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 429\u2013433. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/11513988_43"},{"issue":"5","key":"8_CR74","doi-asserted-by":"crossref","first-page":"311","DOI":"10.1109\/TSE.2004.11","volume":"30","author":"L Zeng","year":"2004","unstructured":"Zeng, L., Benatallah, B., Ngu, A., Dumas, M., Kalagnanam, J., Chang, H.: QoS-aware middleware for web services composition. IEEE Trans. Softw. Eng. 30(5), 311\u2013327 (2004)","journal-title":"IEEE Trans. Softw. Eng."}],"container-title":["Lecture Notes in Computer Science","Software Engineering for Self-Adaptive Systems III. Assurances"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-74183-3_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,10,25]],"date-time":"2020-10-25T19:06:59Z","timestamp":1603652819000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-74183-3_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319741826","9783319741833"],"references-count":74,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-74183-3_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}