{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T20:10:08Z","timestamp":1784837408009,"version":"3.55.0"},"reference-count":102,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2018,5,17]],"date-time":"2018-05-17T00:00:00Z","timestamp":1526515200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"name":"UK MOD"},{"name":"UK MOD"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Autom Softw Eng"],"published-print":{"date-parts":[[2018,12]]},"DOI":"10.1007\/s10515-018-0235-8","type":"journal-article","created":{"date-parts":[[2018,5,17]],"date-time":"2018-05-17T15:52:33Z","timestamp":1526572353000},"page":"785-831","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":50,"title":["Synthesis of probabilistic models for quality-of-service software engineering"],"prefix":"10.1007","volume":"25","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2706-5272","authenticated-orcid":false,"given":"Simos","family":"Gerasimou","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Radu","family":"Calinescu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Giordano","family":"Tamburrelli","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2018,5,17]]},"reference":[{"key":"235_CR1","doi-asserted-by":"crossref","unstructured":"Alba, E., Chicano, F.: Finding safety errors with ACO. In: 9th International Conference on Genetic and Evolutionary Computation (GECCO\u201907), pp. 1066\u20131073 (2007)","DOI":"10.1145\/1276958.1277171"},{"key":"235_CR2","doi-asserted-by":"crossref","unstructured":"Alba, E., Chicano, F.: Searching for liveness property violations in concurrent systems with ACO. In: 10th International Conference on Genetic and Evolutionary Computation (GECCO\u201908), pp. 1727\u20131734 (2008)","DOI":"10.1145\/1389095.1389431"},{"issue":"5","key":"235_CR3","doi-asserted-by":"publisher","first-page":"658","DOI":"10.1109\/TSE.2012.64","volume":"39","author":"A Aleti","year":"2013","unstructured":"Aleti, A., Buhnova, B., Grunske, L., Koziolek, A., Meedeniya, I.: Software architecture optimization methods: a systematic literature review. IEEE Trans. Softw. Eng. 39(5), 658\u2013683 (2013)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"3","key":"235_CR4","doi-asserted-by":"publisher","first-page":"603","DOI":"10.1007\/s10515-016-0197-7","volume":"24","author":"A Aleti","year":"2017","unstructured":"Aleti, A., Moser, I., Grunske, L.: Analysing the fitness landscape of search-based software testing problems. Autom. Softw. Eng. 24(3), 603\u2013621 (2017)","journal-title":"Autom. Softw. Eng."},{"issue":"1","key":"235_CR5","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1008739929481","volume":"15","author":"R Alur","year":"1999","unstructured":"Alur, R., Henzinger, T.A.: Reactive modules. Form. Methods Syst. Des. 15(1), 7\u201348 (1999)","journal-title":"Form. Methods Syst. Des."},{"issue":"1","key":"235_CR6","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"},{"key":"235_CR7","first-page":"88","volume-title":"Lecture Notes in Computer Science","author":"Suzana Andova","year":"2004","unstructured":"Andova, S., Hermanns, H., Katoen, J.P.: Discrete-time rewards model-checked. In: FORMATS 2003, vol. 2791, pp. 88\u2013104 (2004)"},{"issue":"1","key":"235_CR8","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1109\/TSE.2010.46","volume":"37","author":"J Andrews","year":"2011","unstructured":"Andrews, J., Menzies, T., Li, F.: Genetic algorithms for randomized unit testing. IEEE Trans. Softw. Eng. 37(1), 80\u201394 (2011)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"235_CR9","doi-asserted-by":"crossref","unstructured":"Arcuri, A., Briand, L.: A practical guide for using statistical tests to assess randomized algorithms in software engineering. In: 33rd International Conference on Software Engineering (ICSE\u201911), pp. 1\u201310 (2011)","DOI":"10.1145\/1985793.1985795"},{"issue":"1","key":"235_CR10","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. Log. 1(1), 162\u2013170 (2000)","journal-title":"ACM Trans. Comput. Log."},{"issue":"9","key":"235_CR11","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1145\/1810891.1810912","volume":"53","author":"C Baier","year":"2010","unstructured":"Baier, C., Haverkort, B.R., Hermanns, H., Katoen, J.P.: Performance evaluation and model checking join forces. Commun. ACM 53(9), 76\u201385 (2010)","journal-title":"Commun. ACM"},{"key":"235_CR12","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.P.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"235_CR13","doi-asserted-by":"publisher","first-page":"146","DOI":"10.1007\/3-540-48320-9_12","volume-title":"CONCUR\u201999 Concurrency Theory","author":"Christel Baier","year":"1999","unstructured":"Baier, C., Katoen, J.P., Hermanns, H.: Approximate symbolic model checking of continuous-time Markov chains. In: 10th International Conference on Concurrency Theory (CONCUR\u201999), pp. 146\u2013161 (1999)"},{"key":"235_CR14","doi-asserted-by":"crossref","unstructured":"Baresi, L., Ghezzi, C.: The disappearing boundary between development-time and run-time. In: Proceedings of the FSE\/SDP workshop on Future of software engineering research (FoSER\u201910), pp. 17\u201322 (2010)","DOI":"10.1145\/1882362.1882367"},{"key":"235_CR15","doi-asserted-by":"crossref","unstructured":"Bartocci, E., Grosu, R., Katsaros, P., Ramakrishnan, C., Smolka, S.: Model repair for probabilistic systems. In: 17th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201911), vol. 6605, pp. 326\u2013340. Springer (2011)","DOI":"10.1007\/978-3-642-19835-9_30"},{"key":"235_CR16","doi-asserted-by":"crossref","unstructured":"Behrmann, G., David, A., Larsen, K.G., Hakansson, J., Petterson, P., Yi, W., Hendriks, M.: UPPAAL 4.0. In: 3rd International Conference on the Quantitative Evaluation of Systems (QEST\u201906), pp. 125\u2013126 (2006)","DOI":"10.1109\/QEST.2006.59"},{"key":"235_CR17","doi-asserted-by":"crossref","unstructured":"Bianco, A., Alfaro, L.: Model checking of probabilistic and nondeterministic systems. In: Foundations of Software Technology and Theoretical Computer Science, vol. 1026, pp. 499\u2013513. Springer (1995)","DOI":"10.1007\/3-540-60692-0_70"},{"issue":"2","key":"235_CR18","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1145\/2261417.2261437","volume":"43","author":"B Bonakdarpour","year":"2012","unstructured":"Bonakdarpour, B., Kulkarni, S.S.: Automated model repair for distributed programs. ACM SIGACT News 43(2), 85\u2013107 (2012)","journal-title":"ACM SIGACT News"},{"key":"235_CR19","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1016\/S0004-3702(99)00039-9","volume":"112","author":"F Buccafurri","year":"1999","unstructured":"Buccafurri, F., Eiter, T., Gottlob, G., Leone, N.: Enhancing model checking in verification by AI techniques. Artif. Intell. 112, 57\u2013104 (1999)","journal-title":"Artif. Intell."},{"key":"235_CR20","doi-asserted-by":"crossref","unstructured":"Calinescu, R., Autili, M., Cmara, J., Di Marco, A., Gerasimou, S., Inverardi, P., Perucci, A., Jansen, N., Katoen, J.P., Kwiatkowska, M., Mengshoel, O., Spalazzese, R., Tivoli, M.: Synthesis and Verification of Self-aware Computing Systems, pp. 337\u2013373. Springer (2017)","DOI":"10.1007\/978-3-319-47474-8_11"},{"key":"235_CR21","doi-asserted-by":"crossref","unstructured":"Calinescu, R., Ceska, M., Gerasimou, S., Kwiatkowska, M., Paoletti, N.: Designing robust software systems through parametric Markov chain synthesis. In: 2017 IEEE International Conference on Software Architecture (ICSA), pp. 131\u2013140 (2017)","DOI":"10.1109\/ICSA.2017.16"},{"key":"235_CR22","doi-asserted-by":"publisher","first-page":"304","DOI":"10.1007\/978-3-319-66335-7_20","volume-title":"Quantitative Evaluation of Systems","author":"Radu Calinescu","year":"2017","unstructured":"Calinescu, R., Ceska, M., Gerasimou, S., Kwiatkowska, M., Paoletti, N.: RODES: A robust-design synthesis tool for probabilistic systems. In: 14th International Conference on Quantitative Evaluation of Systems (QEST), pp. 304\u2013308 (2017)"},{"key":"235_CR23","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1007\/978-3-662-46675-9_16","volume-title":"Fundamental Approaches to Software Engineering","author":"Radu Calinescu","year":"2015","unstructured":"Calinescu, R., Gerasimou, S., Banks, A.: Self-adaptive software with decentralised control loops. In: 18th International Conference on Fundamental Approaches to Software Engineering (FASE\u201915), pp. 235\u2013251 (2015)"},{"key":"235_CR24","first-page":"223","volume-title":"Software Engineering for Self-Adaptive Systems III. Assurances","author":"Radu Calinescu","year":"2017","unstructured":"Calinescu, R., Gerasimou, S., Johnson, K., Paterson, C.: Using runtime quantitative verification to provide assurance evidence for self-adaptive software. In: Software Engineering for Self-Adaptive Systems III. Assurances, pp. 223\u2013248. Springer (2017)"},{"issue":"1","key":"235_CR25","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1109\/TR.2015.2452931","volume":"65","author":"R Calinescu","year":"2016","unstructured":"Calinescu, R., Ghezzi, C., Johnson, K., Pezz\u00e9, M., Rafiq, Y., Tamburrelli, G.: Formal verification with confidence intervals to establish quality of service properties of software systems. IEEE Trans. Reliab. 65(1), 107\u2013125 (2016)","journal-title":"IEEE Trans. Reliab."},{"issue":"9","key":"235_CR26","doi-asserted-by":"publisher","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":"235_CR27","doi-asserted-by":"publisher","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":"235_CR28","doi-asserted-by":"crossref","unstructured":"Calinescu, R., Kwiatkowska, M.: Using quantitative analysis to implement autonomic IT systems. In: 31st International Conference on Software Engineering (ICSE\u201909), pp. 100\u2013110 (2009)","DOI":"10.1109\/ICSE.2009.5070512"},{"issue":"99","key":"235_CR29","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1109\/TSE.2017.2738640","volume":"PP","author":"R Calinescu","year":"2017","unstructured":"Calinescu, R., Weyns, D., Gerasimou, S., Iftikhar, M.U., Habli, I., Kelly, T.: Engineering trustworthy self-adaptive software with dynamic assurance cases. IEEE Trans. Softw. Eng. PP(99), 1\u201331 (2017)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"235_CR30","doi-asserted-by":"crossref","unstructured":"Canfora, G., Di\u00a0Penta, M., Esposito, R., Villani, M.L.: An approach for QoS-aware service composition based on genetic algorithms. In: 7th International Conference on Genetic and Evolutionary Computation (GECCO\u201905), pp. 1069\u20131075 (2005)","DOI":"10.1145\/1068009.1068189"},{"key":"235_CR31","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1016\/j.artint.2014.02.005","volume":"211","author":"M Carrillo","year":"2014","unstructured":"Carrillo, M., Rosenblueth, D.A.: CTL update of Kripke models through protections. Artif. Intell. 211, 51\u201374 (2014)","journal-title":"Artif. Intell."},{"key":"235_CR32","doi-asserted-by":"crossref","unstructured":"Chatzieleftheriou, G., Bonakdarpour, B., Smolka, S.A., Katsaros, P.: Abstract model repair. In: NASA Formal Methods, pp. 341\u2013355. Springer (2012)","DOI":"10.1007\/978-3-642-28891-3_32"},{"key":"235_CR33","doi-asserted-by":"crossref","unstructured":"Chen, T., Hahn, E.M., Han, T., Kwiatkowska, M., Qu, H., Zhang, L.: Model repair for Markov decision processes. In: 7th International Symposium on Theoretical Aspects of Software Engineering (TASE\u201913), pp. 85\u201392 (2013)","DOI":"10.1109\/TASE.2013.20"},{"key":"235_CR34","volume-title":"Model Checking","author":"EM Clarke Jr","year":"1999","unstructured":"Clarke Jr., E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)"},{"key":"235_CR35","volume-title":"Evolutionary Algorithms for Solving Multi-objective Problems","author":"CAC Coello","year":"2006","unstructured":"Coello, C.A.C., Lamont, G.B., Veldhuizen, D.A.V.: Evolutionary Algorithms for Solving Multi-objective Problems. Springer, Berlin (2006)"},{"key":"235_CR36","doi-asserted-by":"crossref","unstructured":"Coker, Z., Garlan, D., Le\u00a0Goues, C.: SASS: self-adaptation using stochastic search. In: 10th International Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS\u201915), pp. 168\u2013174 (2015)","DOI":"10.1109\/SEAMS.2015.16"},{"key":"235_CR37","doi-asserted-by":"crossref","unstructured":"Damm, L.O., Lundberg, L.: Company-wide implementation of metrics for early software fault detection. In: ICSE, pp. 560\u2013570 (2007)","DOI":"10.1109\/ICSE.2007.25"},{"issue":"2","key":"235_CR38","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1109\/4235.996017","volume":"6","author":"K Deb","year":"2002","unstructured":"Deb, K., Pratap, A., Agarwal, S., Meyarivan, T.: A fast and elitist multiobjective genetic algorithm: NSGA-II. IEEE Trans. Evol. Comput. 6(2), 182\u2013197 (2002)","journal-title":"IEEE Trans. Evol. Comput."},{"key":"235_CR39","doi-asserted-by":"publisher","first-page":"592","DOI":"10.1007\/978-3-319-63390-9_31","volume-title":"Computer Aided Verification","author":"Christian Dehnert","year":"2017","unstructured":"Dehnert, C., Junges, S., Katoen, J.P., Volk, M.: A Storm is coming: a modern probabilistic model checker. In: 29th International Conference on Computer Aided Verification, pp. 592\u2013600 (2017)"},{"key":"235_CR40","doi-asserted-by":"crossref","unstructured":"Draeger, K., Forejt, V., Kwiatkowska, M., Parker, D., Ujma, M.: Permissive controller synthesis for probabilistic systems. In: 20th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201914), vol. 8413, pp. 531\u2013546 (2014)","DOI":"10.1007\/978-3-642-54862-8_44"},{"key":"235_CR41","doi-asserted-by":"publisher","first-page":"760","DOI":"10.1016\/j.advengsoft.2011.05.014","volume":"42","author":"JJ Durillo","year":"2011","unstructured":"Durillo, J.J., Nebro, A.J.: jMetal: a Java framework for multi-objective optimization. Adv. Eng. Softw. 42, 760\u2013771 (2011)","journal-title":"Adv. Eng. Softw."},{"key":"235_CR42","doi-asserted-by":"crossref","unstructured":"Epifani, I., Ghezzi, C., Mirandola, R., Tamburrelli, G.: Model evolution by run-time parameter adaptation. In: 31st International Conference on Software Engineering (ICSE\u201909), pp. 111\u2013121 (2009)","DOI":"10.1109\/ICSE.2009.5070513"},{"key":"235_CR43","doi-asserted-by":"crossref","unstructured":"Ferrucci, F., Harman, M., Ren, J., Sarro, F.: Not going to take this anymore: multi-objective overtime planning for software engineering projects. In: 35th International Conference on Software Engineering (ICSE\u201913), pp. 462\u2013471 (2013)","DOI":"10.1109\/ICSE.2013.6606592"},{"issue":"1","key":"235_CR44","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1109\/TSE.2015.2421318","volume":"42","author":"A Filieri","year":"2016","unstructured":"Filieri, A., Tamburrelli, G., Ghezzi, C.: Supporting self-adaptation via quantitative verification and sensitivity analysis at run time. Trans. Softw. Eng. 42(1), 75\u201399 (2016)","journal-title":"Trans. Softw. Eng."},{"key":"235_CR45","unstructured":"Fonseca, C.M., Fleming, P.J.: Multiobjective optimization. In: Handbook of Evolutionary Computation, vol. 1, pp. C4.5:1\u2013C4.5:9 (1997)"},{"key":"235_CR46","doi-asserted-by":"publisher","first-page":"317","DOI":"10.1007\/978-3-642-33386-6_25","volume-title":"Automated Technology for Verification and Analysis","author":"Vojt\u011bch Forejt","year":"2012","unstructured":"Forejt, V., Kwiatkowska, M., Parker, D.: Pareto curves for probabilistic model checking. In: 10th International Symposium on Automated Technology for Verification and Analysis (ATVA\u201912), vol. 7561, pp. 317\u2013332 (2012)"},{"key":"235_CR47","doi-asserted-by":"crossref","unstructured":"Fraser, G., Arcuri, A.: The seed is strong: Seeding strategies in search-based software testing. In: Fifth International Conference on Software Testing, Verification and Validation (ICST\u201912), pp. 121\u2013130 (2012)","DOI":"10.1109\/ICST.2012.92"},{"issue":"2","key":"235_CR48","doi-asserted-by":"publisher","first-page":"276","DOI":"10.1109\/TSE.2012.14","volume":"39","author":"G Fraser","year":"2013","unstructured":"Fraser, G., Arcuri, A.: Whole test suite generation. IEEE Trans. Softw. Eng. 39(2), 276\u2013291 (2013)","journal-title":"IEEE Trans. Softw. Eng."},{"key":"235_CR49","unstructured":"Gerasimou, S.: Runtime quantitative verification of self-adaptive systems. Ph.D. thesis, University of York, York, UK (2017)"},{"key":"235_CR50","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\u201914), pp. 115\u2013124 (2014)","DOI":"10.1145\/2593929.2593932"},{"key":"235_CR51","doi-asserted-by":"crossref","unstructured":"Gerasimou, S., Calinescu, R., Shevtsov, S., Weyns, D.: Undersea: an exemplar for engineering self-adaptive unmanned underwater vehicles. In: 12th International Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS\u201917), pp. 83\u201389 (2017)","DOI":"10.1109\/SEAMS.2017.19"},{"key":"235_CR52","doi-asserted-by":"crossref","unstructured":"Gerasimou, S., Stylianou, C., Andreou, A.S.: An investigation of optimal project scheduling and team staffing in software development using particle swarm optimization. In: 14th International Conference on Enterprise Information Systems (ICEIS\u201912), pp. 168\u2013171 (2012)","DOI":"10.5220\/0004001001680171"},{"key":"235_CR53","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 International Conference on Automated Software Engineering (ASE\u201915), pp. 319\u2013330 (2015)","DOI":"10.1109\/ASE.2015.22"},{"key":"235_CR54","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":"Carlo Ghezzi","year":"2012","unstructured":"Ghezzi, C.: Evolution, adaptation, and the quest for incrementality. In: Large-Scale Complex IT Systems. Development, Operation and Management, vol. 7539, pp. 369\u2013379 (2012)"},{"key":"235_CR55","unstructured":"Grefenstette, J.J.: Incorporating problem specific knowledge into genetic algorithms. Genetic algorithms and simulated annealing, pp. 42\u201360 (1987)"},{"issue":"5","key":"235_CR56","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. Form. Asp. Comput. 6(5), 512\u2013535 (1994)","journal-title":"Form. Asp. Comput."},{"key":"235_CR57","doi-asserted-by":"crossref","unstructured":"Harman, M., Jia, Y., Krinke, J., Langdon, W.B., Petke, J., Zhang, Y.: Search based software engineering for software product line engineering: a survey and directions for future work. In: 18th International Software Product Line Conference, pp. 5\u201318 (2014)","DOI":"10.1145\/2648511.2648513"},{"key":"235_CR58","doi-asserted-by":"crossref","unstructured":"Harman, M., Jia, Y., Langdon, W.B., Petke, J., Moghadam, I.H., Yoo, S., Wu, F.: Genetic improvement for adaptive software engineering. In: 9th International Symposium on Software Engineering for Adaptive and Self-Managing Systems (SEAMS\u201914), pp. 1\u20134 (2014)","DOI":"10.1145\/2593929.2600116"},{"issue":"1","key":"235_CR59","doi-asserted-by":"publisher","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 (2012a)","journal-title":"ACM Comput. Surv."},{"key":"235_CR60","doi-asserted-by":"crossref","unstructured":"Harman, M., McMinn, P., de\u00a0Souza, J., Yoo, S.: Search based software engineering: techniques, taxonomy, tutorial. In: Empirical Software Engineering and Verification, vol. 7007, pp. 1\u201359. Springer (2012b)","DOI":"10.1007\/978-3-642-25231-0_1"},{"key":"235_CR61","doi-asserted-by":"publisher","first-page":"889","DOI":"10.1007\/978-3-540-87700-4_88","volume-title":"Parallel Problem Solving from Nature \u2013 PPSN X","author":"Sabine Helwig","year":"2008","unstructured":"Helwig, S., Wanka, R.: Theoretical analysis of initial particle swarm behavior. In: 10th International Conference on Parallel Problem Solving from Nature (PPSN\u201908), pp. 889\u2013898 (2008)"},{"key":"235_CR62","doi-asserted-by":"crossref","unstructured":"Johnson, C.: Genetic programming with fitness based on model checking. In: Genetic Programming, vol. 4445, pp. 114\u2013124. Springer (2007)","DOI":"10.1007\/978-3-540-71605-1_11"},{"key":"235_CR63","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\u201913), pp. 33\u201342 (2013)","DOI":"10.1145\/2465449.2465456"},{"key":"235_CR64","doi-asserted-by":"crossref","unstructured":"Katoen, J.P., Khattri, M., Zapreev, I.S.: A Markov reward model checker. In: Quantitative Evaluation of Systems (QEST\u201905), pp. 243\u2013244 (2005)","DOI":"10.1109\/QEST.2005.2"},{"issue":"2","key":"235_CR65","doi-asserted-by":"publisher","first-page":"90","DOI":"10.1016\/j.peva.2010.04.001","volume":"68","author":"JP 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."},{"key":"235_CR66","doi-asserted-by":"publisher","first-page":"70","DOI":"10.4204\/EPTCS.140.5","volume":"140","author":"Gal Katz","year":"2014","unstructured":"Katz, G., Peled, D.: Synthesis of parametric programs using genetic programming and model checking. In: 15th International Workshop on Verification of Infinite-State Systems (INFINITY\u201913), pp. 70\u201384 (2013)","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"key":"235_CR67","doi-asserted-by":"crossref","unstructured":"Kazimipour, B., Li, X., Qin, A.K.: A review of population initialization techniques for evolutionary algorithms. In: IEEE Congress on Evolutionary Computation (CEC\u201914), pp. 2585\u20132592 (2014)","DOI":"10.1109\/CEC.2014.6900618"},{"issue":"1","key":"235_CR68","doi-asserted-by":"publisher","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":"235_CR69","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M.: Quantitative verification: models, techniques and tools. In: 6th Joint Meeting on European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering: Companion Papers (ESEC-FSE\u201907), pp. 449\u2013458 (2007)","DOI":"10.1145\/1295014.1295018"},{"key":"235_CR70","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: Stochastic model checking. In: Formal Methods for the Design of Computer, Communication and Software Systems: Performance Evaluation (SFM\u201907), pp. 220\u2013270. Springer (2007)","DOI":"10.1007\/978-3-540-72522-0_6"},{"key":"235_CR71","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"Marta Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: 23rd International Conference on Computer Aided Verification (CAV\u201911), pp. 585\u2013591 (2011)"},{"key":"235_CR72","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Norman, G., Parker, D., Qu, H.: Assume-guarantee verification for probabilistic systems. In: 16th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201910), vol. 6015, pp. 23\u201337. Springer (2010)","DOI":"10.1007\/978-3-642-12002-2_3"},{"key":"235_CR73","doi-asserted-by":"crossref","unstructured":"Kwiatkowska, M., Parker, D., Qu, H.: Incremental quantitative verification for Markov decision processes. In: 41st International Conference on Dependable Systems Networks (DSN\u201911), pp. 359\u2013370 (2011)","DOI":"10.1109\/DSN.2011.5958249"},{"key":"235_CR74","doi-asserted-by":"crossref","unstructured":"Martens, A., Koziolek, H., Becker, S., Reussner, R.: Automatically improve software architecture models for performance, reliability, and cost using evolutionary algorithms. In: First Joint WOSP\/SIPEW International Conference on Performance Engineering, WOSP\/SIPEW \u201910, pp. 105\u2013116. ACM (2010)","DOI":"10.1145\/1712605.1712624"},{"key":"235_CR75","doi-asserted-by":"crossref","unstructured":"Martinez-Araiza, U., Lopez-Mellado, E.: A CTL model repair method for Petri Nets. In: World Automation Congress (WAC\u201914), pp. 654\u2013659 (2014)","DOI":"10.1109\/WAC.2014.6936082"},{"key":"235_CR76","doi-asserted-by":"crossref","unstructured":"Mason, G., Calinescu, R., Kudenko, D., Banks, A.: Assured reinforcement learning with formally verified abstract policies. In: 9th International Conference on Agents and Artificial Intelligence (ICAART\u201917), vol.\u00a02, pp. 105\u2013117. SciTe Press (2017)","DOI":"10.5220\/0006156001050117"},{"key":"235_CR77","doi-asserted-by":"crossref","unstructured":"Mason, G., Calinescu, R., Kudenko, D., Banks, A.: Assurance in reinforcement learning using quantitative verification. In: Advances in Hybridization of Intelligent Methods: Models, Systems and Applications, pp. 71\u201396. Springer (2018)","DOI":"10.1007\/978-3-319-66790-4_5"},{"key":"235_CR78","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 International Symposium on Software Reliability Engineering (ISSRE\u201910), pp. 229\u2013238 (2010)","DOI":"10.1109\/ISSRE.2010.19"},{"issue":"4","key":"235_CR79","first-page":"35:1","volume":"22","author":"LL Minku","year":"2013","unstructured":"Minku, L.L., Yao, X.: Software effort estimation as a multiobjective learning problem. Trans. Softw. Eng. Methodol. 22(4), 35:1\u201335:32 (2013)","journal-title":"Trans. Softw. Eng. Methodol."},{"key":"235_CR80","doi-asserted-by":"crossref","unstructured":"Moreno, G.A., C\u00e1mara, J., Garlan, D., Schmerl, B.: Proactive self-adaptation under uncertainty: a probabilistic model checking approach. In: 10th Joint Meeting on European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering (ESEC\/FSE\u201915), pp. 1\u201312 (2015)","DOI":"10.1145\/2786805.2786853"},{"issue":"7","key":"235_CR81","doi-asserted-by":"publisher","first-page":"726","DOI":"10.1002\/int.20358","volume":"24","author":"AJ Nebro","year":"2009","unstructured":"Nebro, A.J., Durillo, J.J., Luna, F., Dorronsoro, B., Alba, E.: MOCell: a cellular genetic algorithm for multiobjective optimization. Int. J. Intell. Syst. 24(7), 726\u2013746 (2009)","journal-title":"Int. J. Intell. Syst."},{"issue":"01","key":"235_CR82","doi-asserted-by":"publisher","first-page":"71","DOI":"10.1142\/S1469026801000056","volume":"01","author":"S Oman","year":"2001","unstructured":"Oman, S., Cunningham, P.: Using case retrieval to seed genetic algorithms. Int. J. Comput. Intell. Appl. 01(01), 71\u201382 (2001)","journal-title":"Int. J. Comput. Intell. Appl."},{"key":"235_CR83","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/978-3-642-82453-1_5","volume":"13","author":"A Pnueli","year":"1985","unstructured":"Pnueli, A.: In transition from global to modular temporal reasoning about programs. Log. Models Concurr. Syst. 13, 123\u2013144 (1985)","journal-title":"Log. Models Concurr. Syst."},{"issue":"2","key":"235_CR84","doi-asserted-by":"publisher","first-page":"264","DOI":"10.1109\/TSE.2010.26","volume":"37","author":"K Praditwong","year":"2011","unstructured":"Praditwong, K., Harman, M., Yao, X.: Software module clustering as a multi-objective search problem. IEEE Trans. Softw. Eng. 37(2), 264\u2013282 (2011)","journal-title":"IEEE Trans. Softw. Eng."},{"issue":"10","key":"235_CR85","doi-asserted-by":"publisher","first-page":"1200","DOI":"10.1109\/43.952737","volume":"20","author":"Q Qiu","year":"2001","unstructured":"Qiu, Q., Qu, Q., Pedram, M.: Stochastic modeling of a power-managed system-construction and optimization. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 20(10), 1200\u20131217 (2001)","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"issue":"3","key":"235_CR86","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1007\/s10586-010-0122-y","volume":"14","author":"A Ramirez","year":"2011","unstructured":"Ramirez, A., Knoester, D., Cheng, B., McKinley, P.: Plato: a genetic algorithm approach to run-time reconfiguration in autonomic computing systems. Clust. Comput. 14(3), 229\u2013244 (2011)","journal-title":"Clust. Comput."},{"key":"235_CR87","doi-asserted-by":"crossref","unstructured":"Ren, J., Harman, M., Di\u00a0Penta, M.: Cooperative co-evolutionary optimization of software project staff assignments and job scheduling. In: 3rd International Symposium on Search Based Software Engineering (SSBSE\u201911), vol. 6956, pp. 127\u2013141. Springer (2011)","DOI":"10.1007\/978-3-642-23716-4_14"},{"issue":"2","key":"235_CR88","doi-asserted-by":"publisher","first-page":"14:1","DOI":"10.1145\/1516533.1516538","volume":"4","author":"M Salehie","year":"2009","unstructured":"Salehie, M., Tahvildari, L.: Self-adaptive software: landscape and research challenges. ACM Trans. Auton. Adapt. Syst. 4(2), 14:1\u201314:42 (2009)","journal-title":"ACM Trans. Auton. Adapt. Syst."},{"key":"235_CR89","doi-asserted-by":"crossref","unstructured":"Sayyad, A., Ingram, J., Menzies, T., Ammar, H.: Scalable product line configuration: A straw to break the camel\u2019s back. In: 28th International Conference on Automated Software Engineering (ASE\u201913), pp. 465\u2013474 (2013)","DOI":"10.1109\/ASE.2013.6693104"},{"issue":"2","key":"235_CR90","doi-asserted-by":"publisher","first-page":"403","DOI":"10.1109\/TCAD.2007.911342","volume":"27","author":"A Sesic","year":"2008","unstructured":"Sesic, A., Dautovic, S., Malbasa, V.: Dynamic power management of a system with a two-priority request queue using probabilistic-model checking. IEEE Trans. Comput. Aided Des. Integr. Circuits Syst. 27(2), 403\u2013407 (2008)","journal-title":"IEEE Trans. Comput. Aided Des. Integr. Circuits Syst."},{"key":"235_CR91","doi-asserted-by":"crossref","unstructured":"Stylianou, C., Gerasimou, S., Andreou, A.: A novel prototype tool for intelligent software project scheduling and staffing enhanced with personality factors. In: 24th International Conference on Tools with Artificial Intelligence (ICTAI\u201912), pp. 277\u2013284 (2012)","DOI":"10.1109\/ICTAI.2012.45"},{"issue":"8","key":"235_CR92","doi-asserted-by":"publisher","first-page":"1130","DOI":"10.1177\/0278364913519000","volume":"33","author":"A Ulusoy","year":"2014","unstructured":"Ulusoy, A., Wongpiromsarn, T., Belta, C.: Incremental controller synthesis in probabilistic environments with temporal logic constraints. Int. J. Robot. Res. 33(8), 1130\u20131144 (2014)","journal-title":"Int. J. Robot. Res."},{"key":"235_CR93","doi-asserted-by":"crossref","unstructured":"Van\u00a0Veldhuizen, D.A.: Multiobjective evolutionary algorithms: classifications, analyses, and new innovations. Ph.D. thesis (1999)","DOI":"10.1145\/298151.298382"},{"issue":"2","key":"235_CR94","first-page":"101","volume":"25","author":"A Vargha","year":"2000","unstructured":"Vargha, A., Delaney, H.D.: A critique and improvement of the CL common language effect size statistics of McGraw and Wong. J. Educ. Behav. Stat. 25(2), 101\u2013132 (2000)","journal-title":"J. Educ. Behav. Stat."},{"issue":"4","key":"235_CR95","doi-asserted-by":"publisher","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":"235_CR96","doi-asserted-by":"crossref","unstructured":"Younes, H.L.S.: Ymer: A statistical model checker. In: 17th International Conference on Computer Aided Verification (CAV\u201905), vol. 3576, pp. 429\u2013433. Springer (2005)","DOI":"10.1007\/11513988_43"},{"key":"235_CR97","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1613\/jair.2420","volume":"31","author":"Y Zhang","year":"2008","unstructured":"Zhang, Y., Ding, Y.: CTL model update for system modifications. J. Artif. Intell. Res. (JAIR) 31, 113\u2013155 (2008)","journal-title":"J. Artif. Intell. Res. (JAIR)"},{"key":"235_CR98","doi-asserted-by":"crossref","unstructured":"Zitzler, E., Brockhoff, D., Thiele, L.: The hypervolume indicator revisited: on the design of Pareto-compliant indicators via weighted integration. In: 4th International Conference on Evolutionary Multi-criterion Optimization (EMO\u201907), pp. 862\u2013876 (2007)","DOI":"10.1007\/978-3-540-70928-2_64"},{"key":"235_CR99","doi-asserted-by":"crossref","unstructured":"Zitzler, E., Knowles, J., Thiele, L.: Quality assessment of Pareto set approximations. In: Multiobjective Optimization, vol. 5252, pp. 373\u2013404. Springer (2008)","DOI":"10.1007\/978-3-540-88908-3_14"},{"key":"235_CR100","unstructured":"Zitzler, E., Laumanns, M., Thiele, L.: SPEA2: Improving the strength Pareto evolutionary algorithm. In: Evolutionary Methods for Design Optimization and Control with Applications to Industrial Problems (EUROGEN\u201901), pp. 95\u2013100 (2001)"},{"issue":"4","key":"235_CR101","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1109\/4235.797969","volume":"3","author":"E Zitzler","year":"1999","unstructured":"Zitzler, E., Thiele, L.: Multiobjective evolutionary algorithms: a comparative case study and the strength pareto approach. IEEE Trans. Evol. Comput. 3(4), 257\u2013271 (1999)","journal-title":"IEEE Trans. Evol. Comput."},{"issue":"2","key":"235_CR102","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1109\/TEVC.2003.810758","volume":"7","author":"E Zitzler","year":"2003","unstructured":"Zitzler, E., Thiele, L., Laumanns, M., Fonseca, C., da Fonseca, V.: Performance assessment of multiobjective optimizers: an analysis and review. IEEE Trans. Evol. Comput. 7(2), 117\u2013132 (2003)","journal-title":"IEEE Trans. Evol. Comput."}],"container-title":["Automated Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10515-018-0235-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10515-018-0235-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10515-018-0235-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T16:09:54Z","timestamp":1751645394000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10515-018-0235-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,5,17]]},"references-count":102,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2018,12]]}},"alternative-id":["235"],"URL":"https:\/\/doi.org\/10.1007\/s10515-018-0235-8","relation":{},"ISSN":["0928-8910","1573-7535"],"issn-type":[{"value":"0928-8910","type":"print"},{"value":"1573-7535","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,5,17]]},"assertion":[{"value":"20 December 2017","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"25 April 2018","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"17 May 2018","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}