{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,1]],"date-time":"2026-06-01T08:02:39Z","timestamp":1780300959915,"version":"3.54.0"},"reference-count":62,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2026,8,1]],"date-time":"2026-08-01T00:00:00Z","timestamp":1785542400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2026,8,1]],"date-time":"2026-08-01T00:00:00Z","timestamp":1785542400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2026,8,1]],"date-time":"2026-08-01T00:00:00Z","timestamp":1785542400000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-017"},{"start":{"date-parts":[[2026,8,1]],"date-time":"2026-08-01T00:00:00Z","timestamp":1785542400000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"},{"start":{"date-parts":[[2026,8,1]],"date-time":"2026-08-01T00:00:00Z","timestamp":1785542400000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-012"},{"start":{"date-parts":[[2026,8,1]],"date-time":"2026-08-01T00:00:00Z","timestamp":1785542400000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2026,8,1]],"date-time":"2026-08-01T00:00:00Z","timestamp":1785542400000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-004"}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Science of Computer Programming"],"published-print":{"date-parts":[[2026,8]]},"DOI":"10.1016\/j.scico.2026.103508","type":"journal-article","created":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T06:02:32Z","timestamp":1779084152000},"page":"103508","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":0,"special_numbering":"C","title":["ASMETA: A comprehensive tool set for formal system engineering based on abstract state machines"],"prefix":"10.1016","volume":"253","author":[{"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"}]},{"given":"Angelo","family":"Gargantini","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Elvinia","family":"Riccobene","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Patrizia","family":"Scandurra","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"78","reference":[{"key":"10.1016\/j.scico.2026.103508_bib0001","series-title":"Abstract State Machines","author":"B\u00f6rger","year":"2003"},{"key":"10.1016\/j.scico.2026.103508_bib0002","series-title":"Modeling Companion for Software Practitioners","author":"B\u00f6rger","year":"2018"},{"key":"10.1016\/j.scico.2026.103508_bib0003","series-title":"Structures of Computing - A Guide to Practice-Oriented Theory","author":"B\u00f6rger","year":"2024"},{"key":"10.1016\/j.scico.2026.103508_bib0004","series-title":"The ASMETA Approach to Safety Assurance of Software Systems","first-page":"215","author":"Arcaini","year":"2021"},{"key":"10.1016\/j.scico.2026.103508_bib0005","series-title":"Software Technology: Methods and Tools","first-page":"89","article-title":"Developing medical devices from abstract state machines to embedded systems: a smart pill box case study","author":"Bombarda","year":"2019"},{"key":"10.1016\/j.scico.2026.103508_bib0006","doi-asserted-by":"crossref","first-page":"148","DOI":"10.1016\/j.scico.2017.07.003","article-title":"Integrating formal methods into medical software development: the ASM approach","volume":"158","author":"Arcaini","year":"2018","journal-title":"Sci. Comput. Program."},{"key":"10.1016\/j.scico.2026.103508_bib0007","series-title":"2015 ACM\/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE)","first-page":"80","article-title":"Formal validation and verification of a medical software critical component","author":"Arcaini","year":"2015"},{"issue":"2","key":"10.1016\/j.scico.2026.103508_bib0008","doi-asserted-by":"crossref","DOI":"10.1002\/stvr.1835","article-title":"RATE: a model-based testing approach that combines model refinement and test execution","volume":"33","author":"Bombarda","year":"2023","journal-title":"Softw. Test. Verif. Reliab."},{"key":"10.1016\/j.scico.2026.103508_bib0009","doi-asserted-by":"crossref","DOI":"10.1016\/j.scico.2025.103299","article-title":"Formal specification and validation of the MVM-adapt system using compositional I\/O abstract state machines","volume":"244","author":"Bonfanti","year":"2025","journal-title":"Sci. Comput. Program."},{"issue":"2","key":"10.1016\/j.scico.2026.103508_bib0010","doi-asserted-by":"crossref","first-page":"247","DOI":"10.1007\/s10009-015-0394-x","article-title":"Rigorous development process of a safety-critical system: from ASM models to Java code","volume":"19","author":"Arcaini","year":"2017","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"10.1016\/j.scico.2026.103508_bib0011","series-title":"Rigorous State-Based Methods","first-page":"302","article-title":"Modelling an automotive software-intensive system with adaptive features using ASMETA","author":"Arcaini","year":"2020"},{"key":"10.1016\/j.scico.2026.103508_bib0012","series-title":"Rigorous State-Based Methods - 11th International Conference, ABZ 2025, Proceedings, 15728 LNCS of Lecture Notes in Computer Science","first-page":"212- 230","article-title":"Safety enforcement for autonomous driving on a simulated highway using ASMETA models@run.time","author":"Bombarda","year":"2026"},{"key":"10.1016\/j.scico.2026.103508_bib0013","series-title":"Proceedings of the 13th European Conference on Software Architecture - Vol. 2","first-page":"156","article-title":"A formal design of the hybrid european rail traffic management system","author":"Gaspari","year":"2019"},{"key":"10.1016\/j.scico.2026.103508_bib0014","doi-asserted-by":"crossref","DOI":"10.1007\/s10009-025-00812-2","article-title":"Integrating formal specifications in the development and testing of UIs by formal model-view-controller pattern","author":"Bombarda","year":"2025","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"issue":"4","key":"10.1016\/j.scico.2026.103508_bib0015","doi-asserted-by":"crossref","first-page":"567","DOI":"10.1007\/s00165-016-0371-5","article-title":"ASM-based formal design of an adaptivity component for a cloud system","volume":"28","author":"Arcaini","year":"2016","journal-title":"Form. Aspects Comput."},{"issue":"6","key":"10.1016\/j.scico.2026.103508_bib0016","doi-asserted-by":"crossref","first-page":"1077","DOI":"10.1007\/s00165-013-0289-0","article-title":"A formal framework for service modeling and prototyping","volume":"26","author":"Riccobene","year":"2014","journal-title":"Formal Aspects Comput."},{"key":"10.1016\/j.scico.2026.103508_bib0017","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1016\/j.jss.2013.11.002","article-title":"A reliability model for service component architectures","volume":"89","author":"Mirandola","year":"2014","journal-title":"J. Syst. Softw."},{"key":"10.1016\/j.scico.2026.103508_bib0018","doi-asserted-by":"crossref","DOI":"10.1016\/j.cose.2022.103037","article-title":"A model-based approach for vulnerability analysis of IoT security protocols: the Z-wave case study","volume":"127","author":"Braghin","year":"2023","journal-title":"Comput. Secur."},{"key":"10.1016\/j.scico.2026.103508_bib0019","series-title":"Proceedings of the 39th ACM\/SIGAPP Symposium on Applied Computing, SAC 2024","first-page":"1425","article-title":"Modeling and verification of smart contracts with abstract state machines","author":"Braghin","year":"2024"},{"key":"10.1016\/j.scico.2026.103508_bib0020","series-title":"11th International Conference, ABZ 2025, 15728 of Lecture Notes in Computer Science","first-page":"31","article-title":"Rigorous State-Based Methods","author":"Braghin","year":"2025"},{"key":"10.1016\/j.scico.2026.103508_bib0021","series-title":"Proceedings of the 21st International Conference on Security and Cryptography, SECRYPT 2024","first-page":"334","article-title":"An ASM-based approach for security assessment of ethereum smart contracts","author":"Braghin","year":"2024"},{"issue":"4","key":"10.1016\/j.scico.2026.103508_bib0022","doi-asserted-by":"crossref","first-page":"25:1","DOI":"10.1145\/3019598","article-title":"Formal design and verification of self-adaptive systems with decentralized control","volume":"11","author":"Arcaini","year":"2017","journal-title":"ACM Trans. Auton. Adapt. Syst."},{"key":"10.1016\/j.scico.2026.103508_bib0023","doi-asserted-by":"crossref","DOI":"10.1016\/j.jss.2020.110558","article-title":"MSL: a pattern language for engineering self-adaptive systems","volume":"164","author":"Arcaini","year":"2020","journal-title":"J. Syst. Softw."},{"issue":"1-2","key":"10.1016\/j.scico.2026.103508_bib0024","first-page":"71","article-title":"CoreASM: an extensible ASM execution engine","volume":"77","author":"Farahbod","year":"2007","journal-title":"Fundam. Inf."},{"issue":"5","key":"10.1016\/j.scico.2026.103508_bib0025","doi-asserted-by":"crossref","first-page":"13","DOI":"10.1145\/2666357.2597813","article-title":"CASM: optimized compilation of abstract state machines","volume":"49","author":"Lezuo","year":"2014","journal-title":"SIGPLAN Not."},{"key":"10.1016\/j.scico.2026.103508_bib0026","unstructured":"J. Schmid, Introduction to AsmGofer, 2001. https:\/\/tydo.de\/files\/AsmGofer\/AsmGoferIntro.pdf."},{"key":"10.1016\/j.scico.2026.103508_bib0027","unstructured":"E. Riccobene, P. Scandurra, Metamodelling a formal method: applying MDE to abstract state machines (2006). https:\/\/air.unimi.it\/handle\/2434\/29854."},{"issue":"3-4","key":"10.1016\/j.scico.2026.103508_bib0028","doi-asserted-by":"crossref","first-page":"415","DOI":"10.1007\/s10515-009-0053-0","article-title":"A semantic framework for metamodel-based languages","volume":"16","author":"Gargantini","year":"2009","journal-title":"Autom. Softw. Eng."},{"issue":"10","key":"10.1016\/j.scico.2026.103508_bib0029","doi-asserted-by":"crossref","first-page":"64","DOI":"10.1109\/MC.2004.172","article-title":"Meaningful modeling: what\u2019s the semantics of \u201dSemantics\u201d?","volume":"37","author":"Harel","year":"2004","journal-title":"Computer"},{"key":"10.1016\/j.scico.2026.103508_bib0030","series-title":"Implementing Domain-Specific Languages with Xtext and Xtend","author":"Bettini","year":"2013"},{"key":"10.1016\/j.scico.2026.103508_bib0031","series-title":"Computer Aided Verification","first-page":"359","article-title":"NuSMV 2: an opensource tool for symbolic model checking","author":"Cimatti","year":"2002"},{"key":"10.1016\/j.scico.2026.103508_bib0032","series-title":"Computer Aided Verification","first-page":"334","article-title":"The nuxmv symbolic model checker","author":"Cavada","year":"2014"},{"key":"10.1016\/j.scico.2026.103508_bib0033","series-title":"JavaSMT: A Unified Interface for SMT Solvers in Java","first-page":"139-148","author":"Karpenkov","year":"2016"},{"key":"10.1016\/j.scico.2026.103508_bib0034","doi-asserted-by":"crossref","first-page":"88008","DOI":"10.1109\/ACCESS.2023.3302356","article-title":"Behavior driven development: a systematic literature review","volume":"11","author":"Farooq","year":"2023","journal-title":"IEEE Access"},{"key":"10.1016\/j.scico.2026.103508_bib0035","series-title":"Formal Methods","first-page":"492-517","article-title":"ASMETA Tool set for rigorous system design","author":"Bombarda","year":"2024"},{"issue":"5","key":"10.1016\/j.scico.2026.103508_bib0036","doi-asserted-by":"crossref","first-page":"3049","DOI":"10.1007\/s10270-018-00712-x","article-title":"Models@run.time: a guided tour of the state of the art and research challenges","volume":"18","author":"Bencomo","year":"2019","journal-title":"Softw. Syst. Model."},{"key":"10.1016\/j.scico.2026.103508_bib0037","series-title":"Foundations of Computer Software Modeling, Development, and Verification of Adaptive Systems","first-page":"122","article-title":"Formal methods@runtime","author":"Calinescu","year":"2011"},{"key":"10.1016\/j.scico.2026.103508_bib0038","series-title":"Runtime Failure Prevention and Reaction","first-page":"103","author":"Falcone","year":"2018"},{"issue":"5s","key":"10.1016\/j.scico.2026.103508_bib0039","doi-asserted-by":"crossref","DOI":"10.1145\/3126500","article-title":"Runtime enforcement of cyber-physical systems","volume":"16","author":"Pinisetty","year":"2017","journal-title":"ACM Trans. Embed. Comput. Syst."},{"issue":"4","key":"10.1016\/j.scico.2026.103508_bib0040","doi-asserted-by":"crossref","first-page":"14","DOI":"10.1109\/MSP.2013.49","article-title":"Analysis of safety-critical computer failures in medical devices","volume":"11","author":"Alemzadeh","year":"2013","journal-title":"IEEE Secur. Priv."},{"key":"10.1016\/j.scico.2026.103508_bib0041","doi-asserted-by":"crossref","DOI":"10.1016\/j.jss.2022.111605","article-title":"A component framework for the runtime enforcement of safety properties","volume":"198","author":"Bonfanti","year":"2023","journal-title":"J. Syst. Softw."},{"issue":"1-2","key":"10.1016\/j.scico.2026.103508_bib0042","doi-asserted-by":"crossref","first-page":"71","DOI":"10.1504\/IJPD.2005.006669","article-title":"Product lifecycle management: the new paradigm for enterprises","volume":"2","author":"Grieves","year":"2005","journal-title":"Int. J. Prod. Dev."},{"key":"10.1016\/j.scico.2026.103508_bib0043","series-title":"Leveraging Applications of Formal Methods, Verification and Validation. Application Areas: 12th Int. Symposium, ISoLA 2024, Proceedings, Part V","first-page":"9-26","article-title":"Foundation models for the digital twins creation of cyber-physical systems","author":"Ali","year":"2024"},{"key":"10.1016\/j.scico.2026.103508_bib0044","doi-asserted-by":"crossref","first-page":"961","DOI":"10.1016\/j.procs.2010.12.157","article-title":"A formal framework to model and validate event-based software architecture","volume":"3","author":"Asadollahi","year":"2011","journal-title":"Procedia Comput. Sci."},{"issue":"5","key":"10.1016\/j.scico.2026.103508_bib0045","doi-asserted-by":"crossref","first-page":"287","DOI":"10.1016\/j.jvlc.2012.05.002","article-title":"ASM2Bogor: an approach for verification of models specified through asmeta language","volume":"23","author":"Rafe","year":"2012","journal-title":"J. Vis. Lang. Comput."},{"key":"10.1016\/j.scico.2026.103508_bib0046","series-title":"Software Technologies","first-page":"235","article-title":"An ambient ASM model of client-to-client interaction via cloud computing and an anonymously accessible docking service","author":"B\u00f3sa","year":"2014"},{"issue":"12","key":"10.1016\/j.scico.2026.103508_bib0047","doi-asserted-by":"crossref","first-page":"3523","DOI":"10.1007\/s13369-015-1832-5","article-title":"A mutation-based approach for testing AsmetaL specifications","volume":"40","author":"Hassine","year":"2015","journal-title":"Arab. J. Sci. Eng."},{"key":"10.1016\/j.scico.2026.103508_bib0048","series-title":"2015 12th International Conference on Information Technology - New Generations","first-page":"421","article-title":"MuAsmetaL: an experimental mutation system for AsmetaL","author":"Alkrarha","year":"2015"},{"issue":"6","key":"10.1016\/j.scico.2026.103508_bib0049","doi-asserted-by":"crossref","first-page":"292","DOI":"10.1049\/iet-sen.2015.0030","article-title":"Applying selective mutation strategies to the AsmetaL language","volume":"11","author":"Alkrarha","year":"2017","journal-title":"IET Softw."},{"key":"10.1016\/j.scico.2026.103508_bib0050","series-title":"Formal Methods: Foundations and Applications","first-page":"15","article-title":"Abstract state machines and system theoretic process analysis for safety-critical systems","author":"Al-Shareefi","year":"2017"},{"key":"10.1016\/j.scico.2026.103508_bib0051","series-title":"Abstract State Machines, Alloy, B, TLA, VDM, and Z","first-page":"189","article-title":"Clarification of ambiguity for the simple authentication and security layer","author":"Al-Shareefi","year":"2018"},{"key":"10.1016\/j.scico.2026.103508_bib0052","series-title":"Verification and Evaluation of Computer and Communication Systems","first-page":"47","article-title":"Analysing security protocols using scenario based simulation","author":"Al-Shareefi","year":"2019"},{"key":"10.1016\/j.scico.2026.103508_bib0053","series-title":"Formal Methods and Software Engineering","first-page":"19","article-title":"Modularization of refinement steps for agile formal methods","author":"Benduhn","year":"2017"},{"key":"10.1016\/j.scico.2026.103508_bib0054","series-title":"2017 IEEE 41st Annual Computer Software and Applications Conference (COMPSAC)","first-page":"181","article-title":"Towards an ASM specification for monitoring and adaptation services of large-scale distributed systems","author":"Buga","year":"2017"},{"key":"10.1016\/j.scico.2026.103508_bib0055","series-title":"Database and Expert Systems Applications","first-page":"505","article-title":"A formal approach for failure detection in large-scale distributed systems using abstract state machines","author":"Buga","year":"2017"},{"key":"10.1016\/j.scico.2026.103508_bib0056","series-title":"2017 8th International Conference on Information, Intelligence, Systems & Applications (IISA)","first-page":"1","article-title":"Adopting formal approaches for monitoring and adaptation for large-scale distributed systems","author":"Nemes","year":"2017"},{"key":"10.1016\/j.scico.2026.103508_bib0057","series-title":"Proceedings of the Seventh International Symposium on Business Modeling and Software Design","first-page":"193","article-title":"Towards modeling adaptation services for large-scale distributed systems with abstract state machines","author":"Nemes","year":"2017"},{"key":"10.1016\/j.scico.2026.103508_bib0058","series-title":"Software Engineering and Formal Methods","first-page":"153","article-title":"Formalizing monitoring processes for large-scale distributed systems using abstract state machines","author":"Buga","year":"2018"},{"key":"10.1016\/j.scico.2026.103508_bib0059","series-title":"Proceedings of the 12th European Conference on Software Architecture: Companion Proceedings","first-page":"1","article-title":"MOTION: an application of ASMETA to mobile ad-hoc NETworks domain","author":"Bevilacqua","year":"2018"},{"key":"10.1016\/j.scico.2026.103508_bib0060","series-title":"2021 19th International Conference on Emerging eLearning Technologies and Applications (ICETA)","first-page":"48","article-title":"Modeling routing protocols in AsmetaL","author":"Campanella","year":"2021"},{"key":"10.1016\/j.scico.2026.103508_bib0061","series-title":"Logic, Computation and Rigorous Methods","first-page":"187","article-title":"Analysis of mobile networks\u2019 protocols based on abstract state machine","author":"Covino","year":"2021"},{"key":"10.1016\/j.scico.2026.103508_bib0062","series-title":"10th International Conference, ABZ 2024, 14759 of Lecture Notes in Computer Science","first-page":"215","article-title":"Rigorous State-Based Methods","author":"Castillo","year":"2024"}],"container-title":["Science of Computer Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0167642326000742?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0167642326000742?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2026,6,1]],"date-time":"2026-06-01T07:25:02Z","timestamp":1780298702000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0167642326000742"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,8]]},"references-count":62,"alternative-id":["S0167642326000742"],"URL":"https:\/\/doi.org\/10.1016\/j.scico.2026.103508","relation":{},"ISSN":["0167-6423"],"issn-type":[{"value":"0167-6423","type":"print"}],"subject":[],"published":{"date-parts":[[2026,8]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"ASMETA: A comprehensive tool set for formal system engineering based on abstract state machines","name":"articletitle","label":"Article Title"},{"value":"Science of Computer Programming","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/j.scico.2026.103508","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"\u00a9 2026 Elsevier B.V. All rights are reserved, including those for text and data mining, AI training, and similar technologies.","name":"copyright","label":"Copyright"}],"article-number":"103508"}}