{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T03:19:39Z","timestamp":1740107979727,"version":"3.37.3"},"reference-count":42,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2024,5,17]],"date-time":"2024-05-17T00:00:00Z","timestamp":1715904000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,5,17]],"date-time":"2024-05-17T00:00:00Z","timestamp":1715904000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/100015968","name":"Universit\u00e0 degli studi di Bergamo","doi-asserted-by":"crossref","id":[{"id":"10.13039\/100015968","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2024,6]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Modern automotive systems with adaptive control features require rigorous analysis to guarantee correct operation. We report our experience in modeling the automotive case study from the ABZ2020 conference using the ASMETA toolset, based on the Abstract State Machine formal method. We adopted a seamless system engineering method: from an incremental formal specification of high-level requirements to increasingly refined ASMETA models, to the C++ code generation from the model. Along this process, different validation and verification activities were performed. We explored modeling styles and idioms to face the modeling complexity and ensure that the ASMETA models can best capture and reflect specific behavioral patterns. Through this realistic automotive case study, we evaluated the applicability and usability of our formal modeling approach.<\/jats:p>","DOI":"10.1007\/s10009-024-00751-4","type":"journal-article","created":{"date-parts":[[2024,5,17]],"date-time":"2024-05-17T13:01:45Z","timestamp":1715950905000},"page":"379-401","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A journey with ASMETA from requirements to code: application to an automotive system with adaptive features"],"prefix":"10.1007","volume":"26","author":[{"given":"Paolo","family":"Arcaini","sequence":"first","affiliation":[]},{"given":"Silvia","family":"Bonfanti","sequence":"additional","affiliation":[]},{"given":"Angelo","family":"Gargantini","sequence":"additional","affiliation":[]},{"given":"Elvinia","family":"Riccobene","sequence":"additional","affiliation":[]},{"given":"Patrizia","family":"Scandurra","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,5,17]]},"reference":[{"key":"751_CR1","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/978-3-642-11811-1_6","volume-title":"Proc. Of the Second International Conference on Abstract State Machines, Alloy, B and Z, ABZ\u201910","author":"P. Arcaini","year":"2010","unstructured":"Arcaini, P., Gargantini, A., Riccobene, E.: AsmetaSMV: a way to link high-level ASM models to low-level NuSMV specifications. In: Proc. Of the Second International Conference on Abstract State Machines, Alloy, B and Z, ABZ\u201910, pp.\u00a061\u201374. Springer, Berlin (2010). https:\/\/doi.org\/10.1007\/978-3-642-11811-1_6"},{"key":"751_CR2","first-page":"4","volume-title":"Proc. Of the Second NASA Formal Methods Symposium (NFM 2010), NASA\/CP-2010-216215","author":"P. Arcaini","year":"2010","unstructured":"Arcaini, P., Gargantini, A., Riccobene, E.: Automatic review of abstract state machines by meta property verification. In: Mu\u00f1oz, C. (ed.) Proc. Of the Second NASA Formal Methods Symposium (NFM 2010), NASA\/CP-2010-216215, pp.\u00a04\u201313, NASA, Langley Research Center, Hampton (2010)"},{"key":"751_CR3","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1002\/spe.1019","volume":"41","author":"P. Arcaini","year":"2011","unstructured":"Arcaini, P., Gargantini, A., Riccobene, E., Scandurra, P.: A model-driven process for engineering a toolset for a formal method. Softw. Pract. Exp. 41, 155\u2013166 (2011). https:\/\/doi.org\/10.1002\/spe.1019","journal-title":"Softw. Pract. Exp."},{"key":"751_CR4","doi-asserted-by":"publisher","first-page":"80","DOI":"10.1109\/MEMCOD.2015.7340473","volume-title":"ACM\/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE), 2015","author":"P. Arcaini","year":"2015","unstructured":"Arcaini, P., Bonfanti, S., Gargantini, A., Mashkoor, A., Riccobene, E.: Formal validation and verification of a medical software critical component. In: ACM\/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE), 2015, pp.\u00a080\u201389. IEEE, Los Alamitos (2015). https:\/\/doi.org\/10.1109\/MEMCOD.2015.7340473"},{"issue":"2","key":"751_CR5","doi-asserted-by":"publisher","first-page":"247","DOI":"10.1007\/s10009-015-0394-x","volume":"19","author":"P. Arcaini","year":"2015","unstructured":"Arcaini, P., Gargantini, A., Riccobene, E.: Rigorous development process of a safety-critical system: from ASM models to Java code. Int. J. Softw. Tools Technol. Transf. 19(2), 247\u2013269 (2015). https:\/\/doi.org\/10.1007\/s10009-015-0394-x","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"751_CR6","series-title":"Proceedings","doi-asserted-by":"publisher","first-page":"231","DOI":"10.1007\/978-3-319-33600-8_14","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z: 5th International Conference, ABZ 2016","author":"P. Arcaini","year":"2016","unstructured":"Arcaini, P., Bonfanti, S., Dausend, M., Gargantini, A., Mashkoor, A., Raschke, A., Riccobene, E., Scandurra, P., Stegmaier, M.: Unified syntax for abstract state machines. In: Butler, M., Schewe, K.D., Mashkoor, A., Biro, M. (eds.) Abstract State Machines, Alloy, B, TLA, VDM, and Z: 5th International Conference, ABZ 2016, Linz, Austria, May 23\u201327, 2016. Proceedings, vol.\u00a09675, pp.\u00a0231\u2013236. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-33600-8_14"},{"key":"751_CR7","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/978-3-319-41591-8_17","volume-title":"Software Engineering and Formal Methods","author":"P. Arcaini","year":"2016","unstructured":"Arcaini, P., Gargantini, A., Riccobene, E.: SMT-based automatic proof of ASM model refinement. In: De Nicola, R., K\u00fchn, E. (eds.) Software Engineering and Formal Methods, pp.\u00a0253\u2013269. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41591-8_17"},{"issue":"4","key":"751_CR8","doi-asserted-by":"publisher","first-page":"567","DOI":"10.1007\/s00165-016-0371-5","volume":"28","author":"P. Arcaini","year":"2016","unstructured":"Arcaini, P., Holom, R.M., Riccobene, E.: ASM-based formal design of an adaptivity component for a cloud system. Form. Asp. Comput. 28(4), 567\u2013595 (2016). https:\/\/doi.org\/10.1007\/s00165-016-0371-5","journal-title":"Form. Asp. Comput."},{"issue":"4","key":"751_CR9","doi-asserted-by":"publisher","first-page":"25:1","DOI":"10.1145\/3019598","volume":"11","author":"P. Arcaini","year":"2017","unstructured":"Arcaini, P., Riccobene, E., Scandurra, P.: Formal design and verification of self-adaptive systems with decentralized control. ACM Trans. Auton. Adapt. Syst. 11(4), 25:1\u201325:35 (2017). https:\/\/doi.org\/10.1145\/3019598","journal-title":"ACM Trans. Auton. Adapt. Syst."},{"key":"751_CR10","doi-asserted-by":"publisher","first-page":"148","DOI":"10.1016\/j.scico.2017.07.003","volume":"158","author":"P. Arcaini","year":"2018","unstructured":"Arcaini, P., Bonfanti, S., Gargantini, A., Mashkoor, A., Riccobene, E.: Integrating formal methods into medical software development: the ASM approach. Sci. Comput. Program. 158, 148\u2013167 (2018). https:\/\/doi.org\/10.1016\/j.scico.2017.07.003","journal-title":"Sci. Comput. Program."},{"key":"751_CR11","series-title":"Electronic Proceedings in Theoretical Computer Science","doi-asserted-by":"publisher","first-page":"26","DOI":"10.4204\/EPTCS.284.3","volume-title":"Proc. 4th Workshop on Formal Integrated Development Environment","author":"P. Arcaini","year":"2018","unstructured":"Arcaini, P., Melioli, R., Riccobene, E.: AsmetaF: a flattener for the ASMETA framework. In: Masci, P., Monahan, R., Prevosto, V. (eds.) Proc. 4th Workshop on Formal Integrated Development Environment, Oxford, England, 14 July 2018, Electronic Proceedings in Theoretical Computer Science, vol.\u00a0284, pp.\u00a026\u201336. Open Publishing Association (2018). https:\/\/doi.org\/10.4204\/EPTCS.284.3"},{"key":"751_CR12","series-title":"FM 2019 International Workshops","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/978-3-030-54994-7_6","volume-title":"Formal Methods","author":"P. Arcaini","year":"2020","unstructured":"Arcaini, P., Bonfanti, S., Gargantini, A., Riccobene, E., Scandurra, P.: Addressing usability in a formal development environment. In: Sekerinski, E., Moreira, N., Oliveira, J.N., Ratiu, D., Guidotti, R., Farrell, M., Luckcuck, M., Marmsoler, D., Campos, J., Astarte, T., Gonnord, L., Cerone, A., Couto, L., Dongol, B., Kutrib, M., Monteiro, P., Delmas, D. (eds.) Formal Methods. FM 2019 International Workshops, pp.\u00a061\u201376. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-54994-7_6"},{"key":"751_CR13","doi-asserted-by":"publisher","first-page":"302","DOI":"10.1007\/978-3-030-48077-6_25","volume-title":"Rigorous State-Based Methods","author":"P. Arcaini","year":"2020","unstructured":"Arcaini, P., Bonfanti, S., Gargantini, A., Riccobene, E., Scandurra, P.: Modelling an automotive software-intensive system with adaptive features using ASMETA. In: Raschke, A., M\u00e9ry, D., Houdek, F. (eds.) Rigorous State-Based Methods, pp.\u00a0302\u2013317. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-48077-6_25"},{"key":"751_CR14","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2020.110558","volume":"164","author":"P. Arcaini","year":"2020","unstructured":"Arcaini, P., Mirandola, R., Riccobene, E., Scandurra, P.: MSL: a pattern language for engineering self-adaptive systems. J. Syst. Softw. 164, 110558 (2020). https:\/\/doi.org\/10.1016\/j.jss.2020.110558","journal-title":"J. Syst. Softw."},{"key":"751_CR15","doi-asserted-by":"publisher","first-page":"215","DOI":"10.1007\/978-3-030-76020-5_13","volume-title":"Logic, Computation and Rigorous Methods: Essays Dedicated to Egon B\u00f6rger on the Occasion of His 75th Birthday","author":"P. Arcaini","year":"2021","unstructured":"Arcaini, P., Bombarda, A., Bonfanti, S., Gargantini, A., Riccobene, E., Scandurra, P.: The ASMETA approach to safety assurance of software systems. In: Raschke, A., Riccobene, E., Schewe, K.D. (eds.) Logic, Computation and Rigorous Methods: Essays Dedicated to Egon B\u00f6rger on the Occasion of His 75th Birthday, pp.\u00a0215\u2013238. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-76020-5_13"},{"key":"751_CR16","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1016\/j.scico.2014.04.013","volume":"94","author":"R. Banach","year":"2014","unstructured":"Banach, R., Zhu, H., Su, W., Wu, X.: Asm, controller synthesis, and complete refinement. Sci. Comput. Program. 94, 109\u2013129 (2014). https:\/\/doi.org\/10.1016\/j.scico.2014.04.013","journal-title":"Sci. Comput. Program."},{"key":"751_CR17","doi-asserted-by":"publisher","first-page":"578","DOI":"10.1145\/937555.937561","volume":"4","author":"A. Blass","year":"2003","unstructured":"Blass, A., Gurevich, Y.: Abstract state machines capture parallel algorithms. ACM Trans. Comput. Log. 4, 578\u2013651 (2003). https:\/\/doi.org\/10.1145\/937555.937561","journal-title":"ACM Trans. Comput. Log."},{"key":"751_CR18","doi-asserted-by":"publisher","first-page":"89","DOI":"10.1007\/978-3-030-29852-4_7","volume-title":"Software Technology: Methods and Tools","author":"A. Bombarda","year":"2019","unstructured":"Bombarda, A., Bonfanti, S., Gargantini, A.: Developing medical devices from abstract state machines to embedded systems: a smart pill box case study. In: Mazzara, M., Bruel, J.M., Meyer, B., Petrenko, A. (eds.) Software Technology: Methods and Tools, pp.\u00a089\u2013103. Springer, Cham (2019)"},{"key":"751_CR19","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/978-3-030-31280-0_5","volume-title":"Testing Software and Systems","author":"A. Bombarda","year":"2019","unstructured":"Bombarda, A., Bonfanti, S., Gargantini, A., Radavelli, M., Duan, F., Lei, Y.: Combining model refinement and test generation for conformance testing of the IEEE PHD protocol using abstract state machines. In: Gaston, C., Kosmatov, N., Le Gall, P. (eds.) Testing Software and Systems, pp.\u00a067\u201385. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-31280-0_5"},{"key":"751_CR20","doi-asserted-by":"publisher","first-page":"13","DOI":"10.4204\/EPTCS.349.2","volume-title":"Proc. First Workshop on Applicable Formal Methods, AppFM@FM 2021, Virtual, 23rd November 2021, EPTCS","author":"A. Bombarda","year":"2021","unstructured":"Bombarda, A., Bonfanti, S., Gargantini, A., Riccobene, E.: Developing a prototype of a mechanical ventilator controller from requirements to code with ASMETA. In: Gleirscher, M., van de Pol, J., Woodcock, J. (eds.) Proc. First Workshop on Applicable Formal Methods, AppFM@FM 2021, Virtual, 23rd November 2021, EPTCS, vol.\u00a0349, pp.\u00a013\u201329 (2021). https:\/\/doi.org\/10.4204\/EPTCS.349.2"},{"key":"751_CR21","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/978-3-030-77543-8_8","volume-title":"Rigorous State-Based Methods","author":"A. Bombarda","year":"2021","unstructured":"Bombarda, A., Bonfanti, S., Gargantini, A., Riccobene, E.: Extending ASMETA with time features. In: Raschke, A., M\u00e9ry, D. (eds.) Rigorous State-Based Methods, pp.\u00a0105\u2013111. Springer, Cham (2021)"},{"key":"751_CR22","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1007\/978-3-319-91271-4_25","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"S. Bonfanti","year":"2018","unstructured":"Bonfanti, S., Gargantini, A., Mashkoor, A.: AsmetaA: animator for abstract state machines. In: Butler, M., Raschke, A., Hoang, T.S., Reichl, K. (eds.) Abstract State Machines, Alloy, B, TLA, VDM, and Z, pp.\u00a0369\u2013373. Springer, Cham (2018)"},{"issue":"2","key":"751_CR23","doi-asserted-by":"publisher","DOI":"10.1002\/smr.2205","volume":"32","author":"S. Bonfanti","year":"2020","unstructured":"Bonfanti, S., Gargantini, A., Mashkoor, A.: Design and validation of a C++ code generator from abstract state machines specifications. J. Softw. Evol. Process 32(2), e2205 (2020). https:\/\/doi.org\/10.1002\/smr.2205","journal-title":"J. Softw. Evol. Process"},{"key":"751_CR24","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/978-3-030-86044-8_2","volume-title":"Software Architecture","author":"S. Bonfanti","year":"2021","unstructured":"Bonfanti, S., Riccobene, E., Scandurra, P.: A runtime safety enforcement approach by monitoring and adaptation. In: Biffl, S., Navarro, E., L\u00f6we, W., Sirjani, M., Mirandola, R., Weyns, D. (eds.) Software Architecture, pp.\u00a020\u201336. Springer, Cham (2021)"},{"key":"751_CR25","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1007\/s00165-003-0012-7","volume":"15","author":"E. B\u00f6rger","year":"2003","unstructured":"B\u00f6rger, E.: The ASM refinement method. Form. Asp. Comput. 15, 237\u2013257 (2003)","journal-title":"Form. Asp. Comput."},{"key":"751_CR26","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-56641-1","volume-title":"Modeling Companion for Software Practitioners","author":"E. B\u00f6rger","year":"2018","unstructured":"B\u00f6rger, E., Raschke, A.: Modeling Companion for Software Practitioners. Springer, Berlin (2018). https:\/\/doi.org\/10.1007\/978-3-662-56641-1"},{"issue":"5","key":"751_CR27","doi-asserted-by":"publisher","first-page":"469","DOI":"10.1007\/s00236-015-0249-7","volume":"53","author":"E. B\u00f6rger","year":"2016","unstructured":"B\u00f6rger, E., Schewe, K.: Concurrent abstract state machines. Acta Inform. 53(5), 469\u2013492 (2016). https:\/\/doi.org\/10.1007\/s00236-015-0249-7","journal-title":"Acta Inform."},{"key":"751_CR28","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18216-7","volume-title":"Abstract State Machines: A Method for High-Level System Design and Analysis","author":"E. B\u00f6rger","year":"2003","unstructured":"B\u00f6rger, E., St\u00e4rk, R.: Abstract State Machines: A Method for High-Level System Design and Analysis. Springer, Berlin (2003)"},{"key":"751_CR29","doi-asserted-by":"publisher","first-page":"318","DOI":"10.1007\/978-3-030-48077-6_26","volume-title":"Rigorous State-Based Methods","author":"A. Cunha","year":"2020","unstructured":"Cunha, A., Macedo, N., Liu, C.: Validating multiple variants of an automotive light system with electrum. In: Raschke, A., M\u00e9ry, D., Houdek, F. (eds.) Rigorous State-Based Methods, pp.\u00a0318\u2013334. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-48077-6_26"},{"issue":"1\u20132","key":"751_CR30","first-page":"71","volume":"77","author":"R. Farahbod","year":"2007","unstructured":"Farahbod, R., Gervasi, V., Gl\u00e4sser, U.: CoreASM: an extensible ASM execution engine. Fundam. Inform. 77(1\u20132), 71\u2013103 (2007)","journal-title":"Fundam. Inform."},{"key":"751_CR31","doi-asserted-by":"publisher","first-page":"156","DOI":"10.1145\/3344948.3344993","volume-title":"Proc. Of the 13th European Conference on Software Architecture, ECSA\u201919","author":"P. Gaspari","year":"2019","unstructured":"Gaspari, P., Riccobene, E., Gargantini, A.: A formal design of the hybrid European rail traffic management system. In: Proc. Of the 13th European Conference on Software Architecture, ECSA\u201919, vol.\u00a02, pp.\u00a0156\u2013162. Assoc. Comput. Mach., New York (2019). https:\/\/doi.org\/10.1145\/3344948.3344993"},{"key":"751_CR32","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/978-3-030-48077-6_24","volume-title":"Rigorous State-Based Methods","author":"F. Houdek","year":"2020","unstructured":"Houdek, F., Raschke, A.: Adaptive exterior light and speed control system. In: Raschke, A., M\u00e9ry, D., Houdek, F. (eds.) Rigorous State-Based Methods, pp.\u00a0281\u2013301. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-48077-6_24"},{"issue":"1","key":"751_CR33","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1109\/MC.2003.1160055","volume":"36","author":"J.O. Kephart","year":"2003","unstructured":"Kephart, J.O., Chess, D.M.: The vision of autonomic computing. Computer 36(1), 41\u201350 (2003). https:\/\/doi.org\/10.1109\/MC.2003.1160055","journal-title":"Computer"},{"key":"751_CR34","doi-asserted-by":"publisher","first-page":"382","DOI":"10.1007\/978-3-030-48077-6_30","volume-title":"Rigorous State-Based Methods","author":"S. Krings","year":"2020","unstructured":"Krings, S., K\u00f6rner, P., Dunkelau, J., Rutenkolk, C.: A verified low-level implementation of the adaptive exterior light and speed control system. In: Raschke, A., M\u00e9ry, D., Houdek, F. (eds.) Rigorous State-Based Methods, pp.\u00a0382\u2013397. Springer, Cham (2020)"},{"key":"751_CR35","doi-asserted-by":"publisher","first-page":"335","DOI":"10.1007\/978-3-030-48077-6_27","volume-title":"Rigorous State-Based Methods","author":"M. Leuschel","year":"2020","unstructured":"Leuschel, M., Mutz, M., Werth, M.: Modelling and validating an automotive system in classical B and Event-B. In: Raschke, A., M\u00e9ry, D., Houdek, F. (eds.) Rigorous State-Based Methods, pp.\u00a0335\u2013350. Springer, Cham (2020)"},{"key":"751_CR36","doi-asserted-by":"publisher","first-page":"13","DOI":"10.1145\/2597809.2597813","volume-title":"ACM SIGPLAN\/SIGBED Conference on Languages, Compilers and Tools for Embedded Systems, LCTES 2014","author":"R. Lezuo","year":"2014","unstructured":"Lezuo, R., Paulweber, P., Krall, A.: CASM \u2013 optimized compilation of abstract state machines. In: ACM SIGPLAN\/SIGBED Conference on Languages, Compilers and Tools for Embedded Systems, LCTES 2014, pp.\u00a013\u201322. ACM, New York (2014)"},{"key":"751_CR37","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/978-3-030-48077-6_29","volume-title":"Rigorous State-Based Methods","author":"A. Mammar","year":"2020","unstructured":"Mammar, A., Frappier, M.: Modeling of a speed control system using Event-B. In: Raschke, A., M\u00e9ry, D., Houdek, F. (eds.) Rigorous State-Based Methods, pp.\u00a0367\u2013381. Springer, Cham (2020)"},{"key":"751_CR38","doi-asserted-by":"publisher","first-page":"351","DOI":"10.1007\/978-3-030-48077-6_28","volume-title":"Rigorous State-Based Methods","author":"A. Mammar","year":"2020","unstructured":"Mammar, A., Frappier, M., Laleau, R.: An Event-B model of an automotive adaptive exterior light system. In: Raschke, A., M\u00e9ry, D., Houdek, F. (eds.) Rigorous State-Based Methods, pp.\u00a0351\u2013366. Springer, Cham (2020)"},{"key":"751_CR39","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1016\/j.jss.2013.11.002","volume":"89","author":"R. Mirandola","year":"2014","unstructured":"Mirandola, R., Potena, P., Riccobene, E., Scandurra, P.: A reliability model for service component architectures. J. Syst. Softw. 89, 109\u2013127 (2014). https:\/\/doi.org\/10.1016\/j.jss.2013.11.002","journal-title":"J. Syst. Softw."},{"key":"751_CR40","doi-asserted-by":"publisher","first-page":"204","DOI":"10.1007\/978-3-662-43652-3_17","volume-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z","author":"E. Riccobene","year":"2014","unstructured":"Riccobene, E., Scandurra, P.: Towards ASM-based formal specification of self-adaptive systems. In: Ait Ameur, Y., Schewe, K.D. (eds.) Abstract State Machines, Alloy, B, TLA, VDM, and Z, pp.\u00a0204\u2013209. Springer, Berlin (2014)"},{"key":"751_CR41","volume-title":"Formal Methods and Tools for Computer Science, Eurocast","author":"J. Schmid","year":"2001","unstructured":"Schmid, J.: Compiling abstract state machines to C++. In: Moreno-D\u00ecaz, R., Quesanda-Arencibia, A. (eds.) Formal Methods and Tools for Computer Science, Eurocast (2001). Universidad de Las Palmas de Gran Canaria. Extended Abstract"},{"key":"751_CR42","volume-title":"Software Engineering","author":"I. Sommerville","year":"2010","unstructured":"Sommerville, I.: Software Engineering, 9th edn. Addison-Wesley, Reading (2010)","edition":"9"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-024-00751-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-024-00751-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-024-00751-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,6,18]],"date-time":"2024-06-18T10:10:39Z","timestamp":1718705439000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-024-00751-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,5,17]]},"references-count":42,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2024,6]]}},"alternative-id":["751"],"URL":"https:\/\/doi.org\/10.1007\/s10009-024-00751-4","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"type":"print","value":"1433-2779"},{"type":"electronic","value":"1433-2787"}],"subject":[],"published":{"date-parts":[[2024,5,17]]},"assertion":[{"value":"29 April 2024","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"17 May 2024","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}