{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,4]],"date-time":"2025-11-04T16:12:49Z","timestamp":1762272769329,"version":"3.41.0"},"reference-count":75,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2021,7,23]],"date-time":"2021-07-23T00:00:00Z","timestamp":1626998400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Softw. Eng. Methodol."],"published-print":{"date-parts":[[2021,10,31]]},"abstract":"<jats:p>Abstract State Machine (ASM) theory is a well-known state-based formal method. As in other state-based formal methods, the proposed specification languages for ASMs still lack easy-to-comprehend abstractions to express structural and behavioral aspects of specifications. Our goal is to investigate object-oriented abstractions such as interfaces and traits for ASM-based specification languages. We report on a controlled experiment with 98 participants to study the specification efficiency and effectiveness in which participants needed to comprehend an informal specification as problem (stimulus) in form of a textual description and express a corresponding solution in form of a textual ASM specification using either interface or trait syntax extensions. The study was carried out with a completely randomized design and one alternative (interface or trait) per experimental group. The results indicate that specification effectiveness of the traits experiment group shows a better performance compared to the interfaces experiment group, but specification efficiency shows no statistically significant differences. To the best of our knowledge, this is the first empirical study studying the specification effectiveness and efficiency of object-oriented abstractions in the context of formal methods.<\/jats:p>","DOI":"10.1145\/3450968","type":"journal-article","created":{"date-parts":[[2021,7,23]],"date-time":"2021-07-23T10:58:28Z","timestamp":1627037908000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Specifying with Interface and Trait Abstractions in Abstract State Machines: A Controlled Experiment"],"prefix":"10.1145","volume":"30","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9954-4881","authenticated-orcid":false,"given":"Philipp","family":"Paulweber","sequence":"first","affiliation":[{"name":"University of Vienna, Faculty of Computer Science, Research Group Software Architecture, Austria"}]},{"given":"Georg","family":"Simhandl","sequence":"additional","affiliation":[{"name":"University of Vienna, Faculty of Computer Science, Research Group Software Architecture, Austria"}]},{"given":"Uwe","family":"Zdun","sequence":"additional","affiliation":[{"name":"University of Vienna, Faculty of Computer Science, Research Group Software Architecture, Austria"}]}],"member":"320","published-online":{"date-parts":[[2021,7,23]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10009-010-0145-y"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44518-8_6"},{"volume-title":"Proceedings of the Workshop on Specification and Verification of Component-Based Systems (SAVCBS\u201901)","year":"2001","author":"Barnett Mike","key":"e_1_2_1_3_1"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1111\/j.2517-6161.1995.tb02031.x"},{"volume-title":"Mathematical Studies of Information Processing","author":"Bj\u00f8rner Dines","key":"e_1_2_1_5_1"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1037\/0021-9010.63.6.689"},{"volume-title":"Modeling Companion for Software Practitioners","author":"B\u00f6rger Egon","key":"e_1_2_1_7_1","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-662-56641-1"},{"volume-title":"Abstract State Machines: A Method for High-level System Design and Analysis","author":"B\u00f6rger Egon","key":"e_1_2_1_8_1"},{"volume-title":"Proceedings of the Conference on Object-oriented Programming Systems, Languages and Applications (OOPSLA\u201989)","author":"Canning P. S.","key":"e_1_2_1_9_1"},{"volume-title":"Proceedings of the 30th Conference on Design Automation. IEEE, 86\u201391","author":"Cheng Kwang-Ting","key":"e_1_2_1_10_1"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/1060168.1060172"},{"volume-title":"Proceedings of the MGA, Advanced Simulation Technologies Conference. 105\u2013110","year":"2004","author":"Christen Gast\u00f3n","key":"e_1_2_1_12_1"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/242223.242257"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1037\/0033-2909.114.3.494"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSA.2017.10"},{"key":"e_1_2_1_16_1","article-title":"On the understandability of temporal properties formalized in linear temporal logic, property specification patterns and event processing language","volume":"46","author":"Czepa Christoph","year":"2018","journal-title":"IEEE Trans. Softw. Eng."},{"volume-title":"Henzinger","year":"2001","author":"Alfaro Luca De","key":"e_1_2_1_17_1"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1214\/aoms\/1177706443"},{"key":"e_1_2_1_19_1","first-page":"1","article-title":"CoreASM: An extensible ASM execution engine","volume":"77","author":"Farahbod Roozbeh","year":"2007","journal-title":"Fundam. Informat."},{"key":"e_1_2_1_20_1","first-page":"1949","article-title":"A metamodel-based language and a simulation engine for abstract state machines","volume":"14","author":"Gargantini Angelo","year":"2008","journal-title":"J. Univ. Comput. Sci."},{"volume-title":"International School on Formal Methods for the Design of Computer, Communication and Software Systems","author":"Garlan David","key":"e_1_2_1_21_1"},{"volume-title":"Design and Analysis of Distributed Embedded Systems","author":"Gl\u00e4sser Uwe","key":"e_1_2_1_22_1"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3195836.3195837"},{"volume-title":"Evolving algebras 1993: Lipari guide\u2014Specification and validation methods","author":"Gurevich Yuri","key":"e_1_2_1_24_1"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/343369.343384"},{"volume-title":"Formal Methods for Components and Objects","author":"Gurevich Yuri","key":"e_1_2_1_26_1"},{"key":"e_1_2_1_27_1","first-page":"917","article-title":"Partial updates","volume":"7","author":"Gurevich Yuri","year":"2001","journal-title":"Exploration. J. Univ. Comput. Sci."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/235321.235322"},{"volume-title":"Tichy","year":"2007","author":"H\u00f6fer Andreas","key":"e_1_2_1_29_1"},{"volume-title":"Proceedings of the 9th International Conference on the Quality of Information and Communications Technology (QUATIC\u201914)","year":"2014","author":"Hoisl Bernhard","key":"e_1_2_1_30_1"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/296333.296345"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/505145.505149"},{"volume-title":"Guide to Advanced Empirical Software Engineering","author":"Jedlitschka Andreas","key":"e_1_2_1_33_1"},{"volume-title":"Moreno","year":"2013","author":"Juristo Natalia","key":"e_1_2_1_34_1"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10664-016-9437-5"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2002.1027796"},{"volume-title":"Software Language Engineering: Creating Domain-specific Languages Using Metamodels","author":"Kleppe Anneke G.","key":"e_1_2_1_37_1"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1080\/01621459.1952.10483441"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177726"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-3540-1_11"},{"volume-title":"Scalable Translation Validation","author":"Lezuo Roland","key":"e_1_2_1_41_1"},{"volume-title":"Proceedings of the Software Engineering (Workshops). 75\u201390","year":"2013","author":"Lezuo Roland","key":"e_1_2_1_42_1"},{"volume-title":"Proceedings of the SIGPLAN\/SIGBED Conference on Languages, Compilers and Tools for Embedded Systems (LCTES\u201914)","year":"2014","author":"Lezuo Roland","key":"e_1_2_1_43_1"},{"key":"e_1_2_1_44_1","first-page":"55","article-title":"A technique for the measurement of attitudes","volume":"22","author":"Likert Rensis","year":"1932","journal-title":"Arch. Psychol."},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/800233.807045"},{"key":"e_1_2_1_46_1","unstructured":"Robert C. Martin. 1998. Java and C++ A critical comparison. Java Gems: jewels from Java Report. 51--68. https:\/\/scholar.googleusercontent.com\/scholar.bib?q=info:02F5mRIaveUJ:scholar.google.com\/&output=citation&scisdr=CgXREBsZELS2tWrC-eg:AAGBfm0AAAAAYJLH4egicEIoE_3m4UOXvIrekiQyHbWN&scisig=AAGBfm0AAAAAYJLH4dmtR4kgjFNWSUeXokivMF34GkuP&scisf=4&ct=citation&cd=-1&hl=de&scfhb=1.  Robert C. Martin. 1998. Java and C++ A critical comparison. Java Gems: jewels from Java Report. 51--68. https:\/\/scholar.googleusercontent.com\/scholar.bib?q=info:02F5mRIaveUJ:scholar.google.com\/&output=citation&scisdr=CgXREBsZELS2tWrC-eg:AAGBfm0AAAAAYJLH4egicEIoE_3m4UOXvIrekiQyHbWN&scisig=AAGBfm0AAAAAYJLH4dmtR4kgjFNWSUeXokivMF34GkuP&scisf=4&ct=citation&cd=-1&hl=de&scfhb=1."},{"volume-title":"Klock II","year":"2014","author":"Matsakis Nicholas D.","key":"e_1_2_1_47_1"},{"volume-title":"Proceedings of the 20th ACM SIGPLAN Conference on Object-oriented Programming, Systems, Languages, and Applications (OOPSLA\u201905)","author":"Murphy-Hill Emerson R.","key":"e_1_2_1_48_1"},{"volume-title":"Programming in Scala","author":"Odersky Martin","key":"e_1_2_1_49_1"},{"key":"e_1_2_1_50_1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/986710.986728","article-title":"-ADL: An architecture description language based on the higher-order typed -calculus for specifying dynamic and mobile software architectures","volume":"29","author":"Oquendo Flavio","year":"2004","journal-title":"ACM SIGSOFT Softw. Eng. Notes"},{"edition":"2","volume-title":"Practical Open Source Office: LibreOffice(TM) and Apache OpenOffice","author":"Parsons June Jamrich","key":"e_1_2_1_51_1"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-91271-4_4"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-48077-6_17"},{"key":"e_1_2_1_54_1","doi-asserted-by":"crossref","unstructured":"Philipp Paulweber Georg Simhandl and Uwe Zdun. 2021. Specifying with Interface and Trait Abstractions in Abstract State Machines: A Controlled Experiment. DOI: https:\/\/doi.org\/10.5281\/zenodo.4517172  Philipp Paulweber Georg Simhandl and Uwe Zdun. 2021. Specifying with Interface and Trait Abstractions in Abstract State Machines: A Controlled Experiment. DOI: https:\/\/doi.org\/10.5281\/zenodo.4517172","DOI":"10.1145\/3450968"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jss.2021.110987"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-33600-8_17"},{"volume-title":"An Introduction to Formal Specification and Z","author":"Potter Ben","key":"e_1_2_1_57_1"},{"volume-title":"Friedel","year":"2018","author":"Potts Anthony","key":"e_1_2_1_58_1"},{"volume-title":"R: A Language and Environment for Statistical Computing","year":"2008","author":"Team R Development Core","key":"e_1_2_1_59_1"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-48077-6"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.5555\/2227134.2227135"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.5555\/2818754.2818836"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/307418.307520"},{"volume-title":"Black","year":"2003","author":"Sch\u00e4rli Nathanael","key":"e_1_2_1_64_1"},{"key":"e_1_2_1_65_1","unstructured":"Joachim Schmid. 2001. Introduction to AsmGofer. Retrieved from http:\/\/www.tydo.de\/AsmGofer.  Joachim Schmid. 2001. Introduction to AsmGofer. Retrieved from http:\/\/www.tydo.de\/AsmGofer."},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1002\/sim.4780110603"},{"key":"e_1_2_1_67_1","doi-asserted-by":"crossref","unstructured":"Y. Shafranovich. 2005. Common Format and MIME Type for Comma-Separated Values (CSV) Files.  Y. Shafranovich. 2005. Common Format and MIME Type for Comma-Separated Values (CSV) Files.","DOI":"10.17487\/rfc4180"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.2307\/2333709"},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4615-5265-9"},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0950-5849(00)00166-X"},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.991322"},{"volume-title":"Verification, Validation","author":"St\u00e4rk Robert F.","key":"e_1_2_1_72_1"},{"key":"e_1_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1145\/1414004.1414055"},{"volume-title":"Encyclopedia of Software Engineering","author":"Solingen Rini Van","key":"e_1_2_1_74_1"},{"key":"e_1_2_1_75_1","doi-asserted-by":"publisher","DOI":"10.5555\/2349018"}],"container-title":["ACM Transactions on Software Engineering and Methodology"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3450968","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3450968","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T17:49:24Z","timestamp":1750268964000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3450968"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,7,23]]},"references-count":75,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2021,10,31]]}},"alternative-id":["10.1145\/3450968"],"URL":"https:\/\/doi.org\/10.1145\/3450968","relation":{},"ISSN":["1049-331X","1557-7392"],"issn-type":[{"type":"print","value":"1049-331X"},{"type":"electronic","value":"1557-7392"}],"subject":[],"published":{"date-parts":[[2021,7,23]]},"assertion":[{"value":"2020-06-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-02-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2021-07-23","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}