{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,16]],"date-time":"2026-10-16T20:23:12Z","timestamp":1792182192510,"version":"4.4.0"},"publisher-location":"Cham","reference-count":35,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030613617","type":"print"},{"value":"9783030613624","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","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":[[2020]]},"DOI":"10.1007\/978-3-030-61362-4_21","type":"book-chapter","created":{"date-parts":[[2020,10,28]],"date-time":"2020-10-28T13:02:36Z","timestamp":1603890156000},"page":"368-384","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["30 Years of Simulation-Based Quantitative Analysis Tools: A Comparison Experiment Between M\u00f6bius and Uppaal SMC"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7196-6609","authenticated-orcid":false,"given":"Davide","family":"Basile","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2930-6367","authenticated-orcid":false,"given":"Maurice H.","family":"ter Beek","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8760-7299","authenticated-orcid":false,"given":"Felicita","family":"Di Giandomenico","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4648-4667","authenticated-orcid":false,"given":"Alessandro","family":"Fantechi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0139-0421","authenticated-orcid":false,"given":"Stefania","family":"Gnesi","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7771-0882","authenticated-orcid":false,"given":"Giorgio O.","family":"Spagnolo","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2020,10,29]]},"reference":[{"issue":"1","key":"21_CR1","doi-asserted-by":"publisher","first-page":"6:1","DOI":"10.1145\/3158668","volume":"28","author":"G Agha","year":"2018","unstructured":"Agha, G., Palmskog, K.: A survey of statistical model checking. ACM Trans. Model. Comput. Simul. 28(1), 6:1\u20136:39 (2018). \nhttps:\/\/doi.org\/10.1145\/3158668","journal-title":"ACM Trans. Model. Comput. Simul."},{"key":"21_CR2","doi-asserted-by":"publisher","unstructured":"Ajmone Marsan, M., Bobbio, A., Donatelli, S.: Petri nets in performance analysis: an introduction. In: Reisig, Rozenberg, [30], pp. 211\u2013256. \nhttps:\/\/doi.org\/10.1007\/3-540-65306-6_17","DOI":"10.1007\/3-540-65306-6_17"},{"issue":"1","key":"21_CR3","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1145\/227595.227602","volume":"43","author":"R Alur","year":"1996","unstructured":"Alur, R., Feder, T., Henzinger, T.A.: The benefits of relaxing punctuality. J. ACM 43(1), 116\u2013146 (1996). \nhttps:\/\/doi.org\/10.1145\/227595.227602","journal-title":"J. ACM"},{"issue":"9","key":"21_CR4","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). \nhttps:\/\/doi.org\/10.1145\/1810891.1810912","journal-title":"Commun. ACM"},{"issue":"2","key":"21_CR5","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1016\/j.jrtpm.2016.03.003","volume":"6","author":"D Basile","year":"2016","unstructured":"Basile, D., Chiaradonna, S., Di Giandomenico, F., Gnesi, S.: A stochastic model-based approach to analyse reliable energy-saving rail road switch heating systems. J. Rail Transp. Plan. Manag. 6(2), 163\u2013181 (2016). \nhttps:\/\/doi.org\/10.1016\/j.jrtpm.2016.03.003","journal-title":"J. Rail Transp. Plan. Manag."},{"key":"21_CR6","doi-asserted-by":"publisher","unstructured":"Basile, D., Degano, P., Ferrari, G.L.: Automata for specifying and orchestrating service contracts. Log. Methods Comp. Sci. 12(4) (2016). \nhttps:\/\/doi.org\/10.2168\/LMCS-12(4:6)2016","DOI":"10.2168\/LMCS-12(4:6)2016"},{"key":"21_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/978-3-319-74781-1_19","volume-title":"Software Engineering and Formal Methods","author":"D Basile","year":"2018","unstructured":"Basile, D., Di Giandomenico, F., Gnesi, S.: A refinement approach to analyse critical cyber-physical systems. In: Cerone, A., Roveri, M. (eds.) SEFM 2017. LNCS, vol. 10729, pp. 267\u2013283. Springer, Cham (2018). \nhttps:\/\/doi.org\/10.1007\/978-3-319-74781-1_19"},{"issue":"2","key":"21_CR8","doi-asserted-by":"publisher","first-page":"199","DOI":"10.1007\/s11334-019-00353-3","volume":"16","author":"D Basile","year":"2019","unstructured":"Basile, D., ter Beek, M.H., Legay, A.: Timed service contract automata. Innov. Syst. Softw. Eng. 16(2), 199\u2013214 (2019). \nhttps:\/\/doi.org\/10.1007\/s11334-019-00353-3","journal-title":"Innov. Syst. Softw. Eng."},{"key":"21_CR9","doi-asserted-by":"publisher","unstructured":"Basile, D., Di Giandomenico, F., Gnesi, S.: Statistical model checking of an energy-saving cyber-physical system in the railway domain. In: Proceedings of the 32nd Symposium on Applied Computing (SAC), pp. 1356\u20131363. ACM (2017). \nhttps:\/\/doi.org\/10.1145\/3019612.3019824","DOI":"10.1145\/3019612.3019824"},{"key":"21_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"762","DOI":"10.1007\/978-3-030-30942-8_46","volume-title":"Formal Methods \u2013 The Next 30 Years","author":"MH ter Beek","year":"2019","unstructured":"ter Beek, M.H., et al.: Adopting formal methods in an industrial setting: the railways case. In: ter Beek, M.H., McIver, A., Oliveira, J.N. (eds.) FM 2019. LNCS, vol. 11800, pp. 762\u2013772. Springer, Cham (2019). \nhttps:\/\/doi.org\/10.1007\/978-3-030-30942-8_46"},{"key":"21_CR11","doi-asserted-by":"publisher","unstructured":"Behrmann, G., et al.: UPPAAL 4.0. In: QEST. pp. 125\u2013126. IEEE (2006). \nhttps:\/\/doi.org\/10.1109\/QEST.2006.59","DOI":"10.1109\/QEST.2006.59"},{"key":"21_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/978-3-642-35632-2_25","volume-title":"Runtime Verification","author":"P Bulychev","year":"2013","unstructured":"Bulychev, P., David, A., Larsen, K.G., Legay, A., Li, G., Poulsen, D.B.: Rewrite-based statistical model checking of WMTL. In: Qadeer, S., Tasiran, S. (eds.) RV 2012. LNCS, vol. 7687, pp. 260\u2013275. Springer, Heidelberg (2013). \nhttps:\/\/doi.org\/10.1007\/978-3-642-35632-2_25"},{"key":"21_CR13","doi-asserted-by":"publisher","unstructured":"Chiaradonna, S., Di Giandomenico, F., Masetti, G.: A stochastic modeling approach for an efficient dependability evaluation of large systems with non-anonymous interconnected components. In: Proceedings of the 28th International Symposium on Software Reliability Engineering (ISSRE), pp. 46\u201355. IEEE (2017). \nhttps:\/\/doi.org\/10.1109\/ISSRE.2017.17","DOI":"10.1109\/ISSRE.2017.17"},{"key":"21_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"481","DOI":"10.1007\/978-3-030-30985-5_28","volume-title":"From Software Engineering to Formal Methods and Tools, and Back","author":"S Chiaradonna","year":"2019","unstructured":"Chiaradonna, S., Di Giandomenico, F., Masetti, G., Basile, D.: A refined framework for model-based assessment of energy consumption in the railway sector. In: ter Beek, M.H., Fantechi, A., Semini, L. (eds.) From Software Engineering to Formal Methods and Tools, and Back. LNCS, vol. 11865, pp. 481\u2013501. Springer, Cham (2019). \nhttps:\/\/doi.org\/10.1007\/978-3-030-30985-5_28"},{"key":"21_CR15","doi-asserted-by":"publisher","unstructured":"Clark, G., et al.: The M\u00f6bius modeling tool. In: Proceedings of the 9th International Workshop on Petri Nets and Performance Models (PNPM), pp. 241\u2013250. IEEE (2001). \nhttps:\/\/doi.org\/10.1109\/PNPM.2001.953373","DOI":"10.1109\/PNPM.2001.953373"},{"issue":"5","key":"21_CR16","doi-asserted-by":"publisher","first-page":"69","DOI":"10.1109\/52.84218","volume":"8","author":"JA Couvillion","year":"1991","unstructured":"Couvillion, J.A., et al.: Performability Modeling with UltraSAN. IEEE Softw. 8(5), 69\u201380 (1991). \nhttps:\/\/doi.org\/10.1109\/52.84218","journal-title":"IEEE Softw."},{"issue":"4","key":"21_CR17","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1007\/s10009-014-0361-y","volume":"17","author":"A David","year":"2015","unstructured":"David, A., Larsen, K.G., Legay, A., Miku\u010dionis, M., Poulsen, D.B.: Uppaal SMC tutorial. Int. J. Softw. Tools Technol. Transf. 17(4), 397\u2013415 (2015). \nhttps:\/\/doi.org\/10.1007\/s10009-014-0361-y","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"21_CR18","doi-asserted-by":"publisher","unstructured":"Ferrari, A., Mazzanti, F., Basile, D., ter Beek, M.H., Fantechi, A.: Comparing formal tools for system design: a judgment study. In: Proceedings of the 42nd International Conference on Software Engineering (ICSE), pp. 62\u201374. ACM (2020). \nhttps:\/\/doi.org\/10.1145\/3377811.3380373","DOI":"10.1145\/3377811.3380373"},{"key":"21_CR19","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511569951","author":"J Hillston","year":"1996","unstructured":"Hillston, J.: A Compositional Approach to Performance Modelling. Cambridge University Press (1996). \nhttps:\/\/doi.org\/10.1017\/CBO9780511569951","journal-title":"Cambridge University Press"},{"key":"21_CR20","doi-asserted-by":"publisher","unstructured":"Kemper, P., Tepper, C.: Traviando - debugging simulation traces with message sequence charts. In: QEST, pp. 135\u2013136. IEEE (2006). \nhttps:\/\/doi.org\/10.1109\/QEST.2006.58","DOI":"10.1109\/QEST.2006.58"},{"issue":"1","key":"21_CR21","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(91)90030-6","volume":"94","author":"KG Larsen","year":"1991","unstructured":"Larsen, K.G., Skou, A.: Bisimulation through probabilistic testing. Inf. Comput. 94(1), 1\u201328 (1991). \nhttps:\/\/doi.org\/10.1016\/0890-5401(91)90030-6","journal-title":"Inf. Comput."},{"key":"21_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"478","DOI":"10.1007\/978-3-319-91908-9_23","volume-title":"Computing and Software Science","author":"A Legay","year":"2019","unstructured":"Legay, A., Lukina, A., Traonouez, L.M., Yang, J., Smolka, S.A., Grosu, R.: Statistical model checking. In: Steffen, B., Woeginger, G. (eds.) Computing and Software Science. LNCS, vol. 10000, pp. 478\u2013504. Springer, Cham (2019). \nhttps:\/\/doi.org\/10.1007\/978-3-319-91908-9_23"},{"key":"21_CR23","doi-asserted-by":"publisher","unstructured":"Limnios, N.: Fault Trees. ISTE (2007). \nhttps:\/\/doi.org\/10.1002\/9780470612484","DOI":"10.1002\/9780470612484"},{"issue":"2","key":"21_CR24","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1145\/384192.384195","volume":"33","author":"B Littlewood","year":"2001","unstructured":"Littlewood, B., Popov, P., Strigini, L.: Modeling software design diversity: a review. ACM Comput. Surv. 33(2), 177\u2013208 (2001). \nhttps:\/\/doi.org\/10.1145\/384192.384195","journal-title":"ACM Comput. Surv."},{"key":"21_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"184","DOI":"10.1007\/978-3-319-66583-2_12","volume-title":"Computer Performance Engineering","author":"G Masetti","year":"2017","unstructured":"Masetti, G., Chiaradonna, S., Di Giandomenico, F.: Model-based simulation in M\u00f6bius: an efficient approach targeting loosely interconnected components. In: Reinecke, P., Di Marco, A. (eds.) EPEW 2017. LNCS, vol. 10497, pp. 184\u2013198. Springer, Cham (2017). \nhttps:\/\/doi.org\/10.1007\/978-3-319-66583-2_12"},{"key":"21_CR26","doi-asserted-by":"publisher","unstructured":"Masetti, G., Chiaradonna, S., Di Giandomenico, F., Feddersen, B., Sanders, W.H.: An efficient strategy for model composition in the M\u00f6bius modeling environment. In: Proceedings of the 14th European Dependable Computing Conference (EDCC), pp. 116\u2013119 (2018). \nhttps:\/\/doi.org\/10.1109\/EDCC.2018.00029","DOI":"10.1109\/EDCC.2018.00029"},{"key":"21_CR27","doi-asserted-by":"publisher","unstructured":"Mazzanti, F., Ferrari, A.: Ten diverse formal models for a CBTC automatic train supervision system. In: Gallagher, J.P., van Glabbeek, R., Serwe, W. (eds.) MARS\/VPT. EPTCS, vol. 268, pp. 104\u2013149 (2018). \nhttps:\/\/doi.org\/10.4204\/EPTCS.268.4","DOI":"10.4204\/EPTCS.268.4"},{"issue":"3","key":"21_CR28","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/s10009-018-0488-3","volume":"20","author":"F Mazzanti","year":"2018","unstructured":"Mazzanti, F., Ferrari, A., Spagnolo, G.O.: Towards formal methods diversity in railways: an experience report with seven frameworks. Int. J. Softw. Tools Technol. Transfer 20(3), 263\u2013288 (2018). \nhttps:\/\/doi.org\/10.1007\/s10009-018-0488-3","journal-title":"Int. J. Softw. Tools Technol. Transfer"},{"key":"21_CR29","doi-asserted-by":"publisher","DOI":"10.1016\/C2009-1-61171-0","volume-title":"An Introduction to Stochastic Modeling","author":"MA Pinsky","year":"2011","unstructured":"Pinsky, M.A., Karlin, S.: An Introduction to Stochastic Modeling, 4th edn. Academic Press, Cambridge (2011). \nhttps:\/\/doi.org\/10.1016\/C2009-1-61171-0","edition":"4"},{"key":"21_CR30","doi-asserted-by":"publisher","unstructured":"Reisig, W., Grzegorz, R. (eds.): ACPN 1996. LNCS, vol. 1491. Springer, Heidelberg (1998). \nhttps:\/\/doi.org\/10.1007\/3-540-65306-6","DOI":"10.1007\/3-540-65306-6"},{"key":"21_CR31","doi-asserted-by":"publisher","unstructured":"Reisig, W., Grzegorz, R. (eds.): ACPN 1996. LNCS, vol. 1492. Springer, Heidelberg (1998). \nhttps:\/\/doi.org\/10.1007\/3-540-65307-4","DOI":"10.1007\/3-540-65307-4"},{"issue":"1","key":"21_CR32","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1016\/0166-5316(95)00012-M","volume":"24","author":"W Sanders","year":"1995","unstructured":"Sanders, W., Obal II, W., Qureshi, M., Widjanarko, F.: The UltraSAN modeling environment. Perform. Eval. 24(1), 89\u2013115 (1995). \nhttps:\/\/doi.org\/10.1016\/0166-5316(95)00012-M","journal-title":"Perform. Eval."},{"key":"21_CR33","unstructured":"Sanders, W.H., Meyer, J.F.: METASAN: a performability evaluation tool based on stochastic acitivity networks. In: Proceedings of the 1986 Fall Joint Computer Conference, pp. 807\u2013816. IEEE (1986)"},{"key":"21_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/978-3-540-27813-9_16","volume-title":"Computer Aided Verification","author":"K Sen","year":"2004","unstructured":"Sen, K., Viswanathan, M., Agha, G.: Statistical model checking of black-box probabilistic systems. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 202\u2013215. Springer, Heidelberg (2004). \nhttps:\/\/doi.org\/10.1007\/978-3-540-27813-9_16"},{"key":"21_CR35","unstructured":"Younes, H.L.S.: Verification and Planning for Stochastic Processes with Asynchronous Events. Ph.D. thesis, Carnegie Mellon University, January 2005. \nhttp:\/\/reports-archive.adm.cs.cmu.edu\/anon\/2005\/CMU-CS-05-105.pdf"}],"container-title":["Lecture Notes in Computer Science","Leveraging Applications of Formal Methods, Verification and Validation: Verification Principles"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-61362-4_21","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,10,28]],"date-time":"2020-10-28T13:12:17Z","timestamp":1603890737000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-61362-4_21"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030613617","9783030613624"],"references-count":35,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-61362-4_21","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"29 October 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ISoLA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Leveraging Applications of Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Rhodes","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Greece","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"20 October 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 October 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"isola2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/isola-conference.org\/isola2020\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}