{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,16]],"date-time":"2026-06-16T23:08:33Z","timestamp":1781651313335,"version":"3.54.5"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031711763","type":"print"},{"value":"9783031711770","type":"electronic"}],"license":[{"start":{"date-parts":[[2024,9,13]],"date-time":"2024-09-13T00:00:00Z","timestamp":1726185600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,9,13]],"date-time":"2024-09-13T00:00:00Z","timestamp":1726185600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>This tutorial paper introduces ASMETA, a comprehensive suite of integrated tools around the formal method Abstract State Machines to specify and analyze the executable behavior of discrete event systems. ASMETA supports the entire system development life-cycle, from the specification of the functional requirements to the implementation of the code, in a systematic and incremental way. This tutorial provides an overview of ASMETA through an illustrative case study, the Pill-Box, related to the design of a smart pillbox device. It illustrates the practical use of the range of modeling and V&amp;V techniques available in ASMETA and C++ code generation from models, to increase the quality and reliability of behavioral system models and source code.<\/jats:p>","DOI":"10.1007\/978-3-031-71177-0_28","type":"book-chapter","created":{"date-parts":[[2024,9,12]],"date-time":"2024-09-12T06:10:51Z","timestamp":1726121451000},"page":"492-517","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":16,"title":["ASMETA Tool Set for\u00a0Rigorous System Design"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4244-9319","authenticated-orcid":false,"given":"Andrea","family":"Bombarda","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9679-4551","authenticated-orcid":false,"given":"Silvia","family":"Bonfanti","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4035-0131","authenticated-orcid":false,"given":"Angelo","family":"Gargantini","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1400-1026","authenticated-orcid":false,"given":"Elvinia","family":"Riccobene","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9209-3624","authenticated-orcid":false,"given":"Patrizia","family":"Scandurra","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2024,9,13]]},"reference":[{"key":"28_CR1","doi-asserted-by":"publisher","unstructured":"Arcaini, P., Bombarda, A., Bonfanti, S., Gargantini, A., Riccobene, E., Scandurra, P.: The ASMETA Approach to Safety Assurance of Software Systems, pp. 215\u2013238. Springer International Publishing, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-76020-5_13","DOI":"10.1007\/978-3-030-76020-5_13"},{"key":"28_CR2","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/978-3-642-11811-1_6","volume-title":"Abstract State Machines, Alloy, B and Z","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: Frappier, M., Gl\u00e4sser, U., Khurshid, S., Laleau, R., Reeves, S. (eds.) Abstract State Machines, Alloy, B and Z, pp. 61\u201374. Springer, Berlin, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-11811-1_6"},{"key":"28_CR3","unstructured":"Arcaini, P., Gargantini, A., Riccobene, E.: Automatic review of Abstract State Machines by meta property verification. In: Mu\u00f1oz, C. (ed.) Proceedings of the Second NASA Formal Methods Symposium (NFM 2010), NASA\/CP-2010-216215, pp. 4\u201313. NASA, Langley Research Center, Hampton VA 23681\u20132199, USA (2010)"},{"key":"28_CR4","doi-asserted-by":"publisher","unstructured":"Arcaini, P., Gargantini, A., Riccobene, E.: SMT-based automatic proof of ASM model refinement. In: De\u00a0Nicola, R., K\u00fchn, E. (eds.) Software Engineering and Formal Methods, pp. 253\u2013269. Springer International Publishing, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41591-8_17","DOI":"10.1007\/978-3-319-41591-8_17"},{"key":"28_CR5","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. Exper. 41, 155\u2013166 (2011). https:\/\/doi.org\/10.1002\/spe.1019","journal-title":"Softw. Pract. Exper."},{"key":"28_CR6","doi-asserted-by":"publisher","unstructured":"ter Beek, M.H.: Formal methods and tools applied in the railway domain. In: Bonfanti, S., Gargantini, A., Leuschel, M., Riccobene, E., Scandurra, P. (eds.) Rigorous State-Based Methods - 10th International Conference, ABZ 2024, Bergamo, Italy, June 25-28, 2024, Proceedings. Lecture Notes in Computer Science, vol. 14759, pp. 3\u201321. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-63790-2_1","DOI":"10.1007\/978-3-031-63790-2_1"},{"key":"28_CR7","doi-asserted-by":"crossref","unstructured":"ter Beek, M.H., et al.: Formal methods in industry. Form. Asp. Comput. (2024)","DOI":"10.1145\/3689374"},{"key":"28_CR8","doi-asserted-by":"publisher","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. 89\u2013103. Springer International Publishing, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-29852-4_7","DOI":"10.1007\/978-3-030-29852-4_7"},{"key":"28_CR9","doi-asserted-by":"publisher","unstructured":"Bombarda, A., Bonfanti, S., Gargantini, A.: From concept to code: unveiling a tool for translating abstract state machines into java code. In: Rigorous State-Based Methods 10th International Conference, ABZ 2024, Bergamo, Italy, June 25-28, 2024, Proceedings, Lecture Notes in Computer Science, vol. 14759. Springer (2024). https:\/\/doi.org\/10.1007\/978-3-031-63790-2_10","DOI":"10.1007\/978-3-031-63790-2_10"},{"key":"28_CR10","doi-asserted-by":"publisher","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. 105\u2013111. Springer International Publishing, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-77543-8_8","DOI":"10.1007\/978-3-030-77543-8_8"},{"key":"28_CR11","doi-asserted-by":"publisher","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. 369\u2013373. Springer International Publishing, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-91271-4_25","DOI":"10.1007\/978-3-319-91271-4_25"},{"key":"28_CR12","doi-asserted-by":"publisher","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","DOI":"10.1002\/smr.2205"},{"key":"28_CR13","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":"28_CR14","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, Heidelberg (2018). https:\/\/doi.org\/10.1007\/978-3-662-56641-1"},{"key":"28_CR15","doi-asserted-by":"publisher","unstructured":"B\u00f6rger, E., St\u00e4rk, R.: Abstract State Machines. Springer, Berlin, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-642-18216-7","DOI":"10.1007\/978-3-642-18216-7"},{"key":"28_CR16","doi-asserted-by":"publisher","unstructured":"Brambilla, M., Cabot, J., Wimmer, M.: Model-Driven Software Engineering in Practice. Springer International Publishing (2017). https:\/\/doi.org\/10.1007\/978-3-031-02549-5","DOI":"10.1007\/978-3-031-02549-5"},{"key":"28_CR17","doi-asserted-by":"publisher","unstructured":"Broy, M., et al.: Does every computer scientist need to know formal methods? Form. Asp. Comput. (2024). https:\/\/doi.org\/10.1145\/3670795","DOI":"10.1145\/3670795"},{"key":"28_CR18","doi-asserted-by":"publisher","unstructured":"Carioni, A., Gargantini, A., Riccobene, E., Scandurra, P.: A scenario-based validation language for ASMs. In: B\u00f6rger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) Abstract State Machines, B and Z, pp. 71\u201384. Springer, Berlin, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-87603-8_7","DOI":"10.1007\/978-3-540-87603-8_7"},{"key":"28_CR19","doi-asserted-by":"publisher","unstructured":"Cavada, R., et al.: The nuxmv symbolic model checker. In: Biere, A., Bloem, R. (eds.) Computer Aided Verification, pp. 334\u2013342. Springer International Publishing, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_22","DOI":"10.1007\/978-3-319-08867-9_22"},{"key":"28_CR20","doi-asserted-by":"publisher","unstructured":"Cimatti, A., et al: NuSMV 2: an opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) Computer Aided Verification, pp. 359\u2013364. Springer, Berlin, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45657-0_29","DOI":"10.1007\/3-540-45657-0_29"},{"key":"28_CR21","doi-asserted-by":"publisher","unstructured":"Garavel, H., Beek, M.H.t., Pol, J.V.D.: The 2020 expert survey on formal methods. In: Formal Methods for Industrial Critical Systems: 25th International Conference, FMICS 2020, Vienna, Austria, September 2\u20133, 2020, Proceedings 25, pp. 3\u201369. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-58298-2_1","DOI":"10.1007\/978-3-030-58298-2_1"},{"issue":"6","key":"28_CR22","doi-asserted-by":"publisher","first-page":"4473","DOI":"10.1007\/s10664-020-09836-5","volume":"25","author":"M Gleirscher","year":"2020","unstructured":"Gleirscher, M., Marmsoler, D.: Formal methods in dependable systems engineering: a survey of professionals from Europe and North America. Empir. Softw. Eng. 25(6), 4473\u20134546 (2020). https:\/\/doi.org\/10.1007\/s10664-020-09836-5","journal-title":"Empir. Softw. Eng."},{"issue":"6","key":"28_CR23","doi-asserted-by":"publisher","first-page":"1737","DOI":"10.1007\/s10270-023-01124-2","volume":"22","author":"M Gleirscher","year":"2023","unstructured":"Gleirscher, M., van de Pol, J., Woodcock, J.: A manifesto for applicable formal methods. Softw. Syst. Model. 22(6), 1737\u20131749 (2023). https:\/\/doi.org\/10.1007\/s10270-023-01124-2","journal-title":"Softw. Syst. Model."}],"container-title":["Lecture Notes in Computer Science","Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-71177-0_28","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,12]],"date-time":"2024-09-12T06:15:16Z","timestamp":1726121716000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-71177-0_28"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,9,13]]},"ISBN":["9783031711763","9783031711770"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-71177-0_28","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,9,13]]},"assertion":[{"value":"13 September 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Formal Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Milan","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 September 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13 September 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fm2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.fm24.polimi.it\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}