{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T09:59:44Z","timestamp":1740131984175,"version":"3.37.3"},"reference-count":66,"publisher":"Institute of Electrical and Electronics Engineers (IEEE)","issue":"11","license":[{"start":{"date-parts":[[2023,11,1]],"date-time":"2023-11-01T00:00:00Z","timestamp":1698796800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/ieeexplore.ieee.org\/Xplorehelp\/downloads\/license-information\/IEEE.html"},{"start":{"date-parts":[[2023,11,1]],"date-time":"2023-11-01T00:00:00Z","timestamp":1698796800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-029"},{"start":{"date-parts":[[2023,11,1]],"date-time":"2023-11-01T00:00:00Z","timestamp":1698796800000},"content-version":"stm-asf","delay-in-days":0,"URL":"https:\/\/doi.org\/10.15223\/policy-037"}],"funder":[{"name":"ANPCyT PICTs","award":["2017-2622","2019-2050","2020-2896"],"award-info":[{"award-number":["2017-2622","2019-2050","2020-2896"]}]},{"name":"EU’s Marie Sklodowska-Curie","award":["101008233"],"award-info":[{"award-number":["101008233"]}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["IIEEE Trans. Software Eng."],"published-print":{"date-parts":[[2023,11]]},"DOI":"10.1109\/tse.2023.3320625","type":"journal-article","created":{"date-parts":[[2023,9,29]],"date-time":"2023-09-29T17:41:39Z","timestamp":1696009299000},"page":"4946-4963","source":"Crossref","is-referenced-by-count":0,"title":["A Study of the Electrum and DynAlloy Dynamic Behavior Notations"],"prefix":"10.1109","volume":"49","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3716-3607","authenticated-orcid":false,"given":"C\u00e9sar","family":"Cornejo","sequence":"first","affiliation":[{"name":"CONICET, Buenos Aires, Argentina"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0979-4623","authenticated-orcid":false,"given":"Germ\u00e1n E.","family":"Regis","sequence":"additional","affiliation":[{"name":"CONICET, Buenos Aires, Argentina"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0532-5296","authenticated-orcid":false,"given":"Nazareno","family":"Aguirre","sequence":"additional","affiliation":[{"name":"CONICET, Buenos Aires, Argentina"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5592-1355","authenticated-orcid":false,"given":"Marcelo F.","family":"Frias","sequence":"additional","affiliation":[{"name":"Department of Computer Science, The University of Texas at El Paso, TX, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"263","reference":[{"key":"ref1","article-title":"Detailed results and replication package for DynAlloy and electrum evaluation"},{"key":"ref2","doi-asserted-by":"publisher","DOI":"10.1109\/MoDRE.2018.00008"},{"key":"ref3","volume-title":"Formal Methods for Industrial Applications, Specifying and Programming the Steam Boiler Control (The Book Grow Out of a Dagstuhl Seminar) (Lecture Notes in Computer Science)","volume":"1165","author":"Abrial","year":"1995"},{"key":"ref4","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(85)90056-0"},{"key":"ref5","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-008-0110-3"},{"key":"ref6","doi-asserted-by":"publisher","DOI":"10.1007\/11841883_22"},{"volume-title":"The Unified Modeling Language User Guide\u2014The Ultimate Tutorial to the UML From the Original Designers","year":"1999","author":"Booch","key":"ref7"},{"key":"ref8","first-page":"71","article-title":"Formal methods","volume-title":"Computing Handbook","author":"Bowen","year":"2014"},{"key":"ref9","doi-asserted-by":"publisher","DOI":"10.1145\/3238147.3240475"},{"key":"ref10","doi-asserted-by":"publisher","DOI":"10.23919\/FMCAD.2018.8603001"},{"key":"ref11","first-page":"1","article-title":"Dynamic software architectures verification using dynalloy","volume":"10","author":"Bucchiarone","year":"2008","journal-title":"Electron. Commun. EASST"},{"key":"ref12","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_22"},{"key":"ref13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-24730-2_15"},{"key":"ref14","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96145-3_10"},{"key":"ref15","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-43652-3_29"},{"key":"ref16","doi-asserted-by":"publisher","DOI":"10.1145\/1146238.1146251"},{"key":"ref17","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008764923992"},{"key":"ref18","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4612-3228-5","volume-title":"Predicate Calculus and Program Semantics. Texts and Monographs in Computer Science","author":"Dijkstra","year":"1990"},{"key":"ref19","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-019-00763-8"},{"key":"ref20","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-007-0059-y"},{"key":"ref21","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2005.1553587"},{"key":"ref22","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-45236-2_37"},{"key":"ref23","doi-asserted-by":"publisher","DOI":"10.1145\/1101815.1101819"},{"key":"ref24","doi-asserted-by":"publisher","DOI":"10.1145\/1314493.1314497"},{"key":"ref25","doi-asserted-by":"publisher","DOI":"10.1145\/567446.567462"},{"key":"ref26","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2013.15"},{"key":"ref27","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-007-0054-3"},{"volume-title":"Fundamentals of Software Engineering","year":"2002","author":"Ghezzi","key":"ref28"},{"key":"ref29","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2018.11.049"},{"key":"ref30","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-007-0057-0"},{"key":"ref31","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/2516.001.0001"},{"key":"ref32","doi-asserted-by":"publisher","DOI":"10.1145\/1378727.1378742"},{"key":"ref33","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"volume-title":"The SPIN Model Checker\u2014Primer and Reference Manual","year":"2004","author":"Holzmann","key":"ref34"},{"key":"ref35","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9780511810275","volume-title":"Logic in Computer Science\u2014Modelling and Reasoning About Systems","author":"Huth","year":"2004"},{"article-title":"A comparison of object modelling notations: Alloy, UML and Z","year":"1999","author":"Jackson","key":"ref36"},{"key":"ref37","doi-asserted-by":"publisher","DOI":"10.1145\/505145.505149"},{"volume-title":"Software Abstractions: Logic, Language, and Analysis","year":"2006","author":"Jackson","key":"ref38"},{"key":"ref39","doi-asserted-by":"publisher","DOI":"10.1145\/503209.503219"},{"key":"ref40","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2011.6100137"},{"key":"ref41","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-50497-0","volume-title":"Decision Procedures\u2014An Algorithmic Point of View","author":"Kroening","year":"2016"},{"volume-title":"Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers","year":"2002","author":"Lamport","key":"ref42"},{"key":"ref43","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-07881-6_24"},{"key":"ref44","doi-asserted-by":"publisher","DOI":"10.1145\/2950290.2950318"},{"volume-title":"Concurrency\u2014State Models and Java Programs","year":"1999","author":"Magee","key":"ref45"},{"key":"ref46","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(84)90003-0"},{"key":"ref47","doi-asserted-by":"publisher","DOI":"10.1145\/1985793.1985863"},{"key":"ref48","doi-asserted-by":"publisher","DOI":"10.1145\/2544136"},{"key":"ref49","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11811-1_10"},{"key":"ref50","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4757-3540-6","volume-title":"Software Reliability Methods. Texts in Computer Science","author":"Peled","year":"2001"},{"key":"ref51","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-007-0058-z"},{"key":"ref52","doi-asserted-by":"publisher","DOI":"10.1145\/3106237.3122826"},{"key":"ref53","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-017-0592-y"},{"key":"ref54","doi-asserted-by":"publisher","DOI":"10.2307\/2687980"},{"key":"ref55","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-022-01012-1"},{"key":"ref56","doi-asserted-by":"publisher","DOI":"10.1109\/REW.2017.70"},{"key":"ref57","doi-asserted-by":"publisher","DOI":"10.1145\/383059.383071"},{"key":"ref58","article-title":"Evaluating state modeling techniques in alloy","volume-title":"Proc. 6th Workshop Softw. Qual. Anal. Monit. Improvement Appl.","volume":"1938","author":"Sullivan","year":"2017"},{"key":"ref59","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-30885-7_11"},{"key":"ref60","first-page":"555","article-title":"Some shortcomings of OCL, the object constraint language of UML","volume-title":"Proc. 34th Int. Conf. Technol. Object-Oriented Lang. Syst. (TOOLS)","author":"Vaziri","year":"2000"},{"key":"ref61","doi-asserted-by":"publisher","DOI":"10.1023\/A:1022920129859"},{"key":"ref62","doi-asserted-by":"publisher","DOI":"10.1016\/S0950-5849(03)00131-9"},{"key":"ref63","doi-asserted-by":"publisher","DOI":"10.1109\/2.58215"},{"key":"ref64","doi-asserted-by":"publisher","DOI":"10.1145\/2185376.2185383"},{"key":"ref65","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-014-0302-2"},{"key":"ref66","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2017.2655056"}],"container-title":["IEEE Transactions on Software Engineering"],"original-title":[],"link":[{"URL":"http:\/\/xplorestaging.ieee.org\/ielx7\/32\/10320136\/10268087.pdf?arnumber=10268087","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,3,2]],"date-time":"2024-03-02T07:22:39Z","timestamp":1709364159000},"score":1,"resource":{"primary":{"URL":"https:\/\/ieeexplore.ieee.org\/document\/10268087\/"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,11]]},"references-count":66,"journal-issue":{"issue":"11"},"URL":"https:\/\/doi.org\/10.1109\/tse.2023.3320625","relation":{},"ISSN":["0098-5589","1939-3520","2326-3881"],"issn-type":[{"type":"print","value":"0098-5589"},{"type":"electronic","value":"1939-3520"},{"type":"electronic","value":"2326-3881"}],"subject":[],"published":{"date-parts":[[2023,11]]}}}