{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,7]],"date-time":"2026-02-07T13:14:41Z","timestamp":1770470081336,"version":"3.49.0"},"publisher-location":"New York, NY, USA","reference-count":37,"publisher":"ACM","license":[{"start":{"date-parts":[[2024,9,22]],"date-time":"2024-09-22T00:00:00Z","timestamp":1726963200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"German BMBF"},{"name":"EUREKA","award":["022-1.2.4-EUREKA-2023-00013"],"award-info":[{"award-number":["022-1.2.4-EUREKA-2023-00013"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2024,9,22]]},"DOI":"10.1145\/3652620.3687820","type":"proceedings-article","created":{"date-parts":[[2024,10,31]],"date-time":"2024-10-31T18:06:36Z","timestamp":1730397996000},"page":"1086-1095","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":10,"title":["Towards the Formal Verification of SysML v2 Models"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8204-7595","authenticated-orcid":false,"given":"Vince","family":"Moln\u00e1r","sequence":"first","affiliation":[{"name":"Department of Artificial Intelligence and Systems Engineering, Budapest University of Technology and Economics, Budapest, Hungary"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5546-5970","authenticated-orcid":false,"given":"Bence","family":"Graics","sequence":"additional","affiliation":[{"name":"Department of Artificial Intelligence and Systems Engineering, Budapest University of Technology and Economics, Budapest, Hungary"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7617-3563","authenticated-orcid":false,"given":"Andr\u00e1s","family":"V\u00f6r\u00f6s","sequence":"additional","affiliation":[{"name":"Department of Artificial Intelligence and Systems Engineering, Budapest University of Technology and Economics, Budapest, Hungary"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9091-7899","authenticated-orcid":false,"given":"Stefano","family":"Tonetta","sequence":"additional","affiliation":[{"name":"Fondazione Bruno Kessler, Trento, Italy"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8519-6342","authenticated-orcid":false,"given":"Luca","family":"Cristoforetti","sequence":"additional","affiliation":[{"name":"Fondazione Bruno Kessler, Trento, Italy"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-2192-4276","authenticated-orcid":false,"given":"Greg","family":"Kimberly","sequence":"additional","affiliation":[{"name":"The Boeing Company, Seattle, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-7603-4327","authenticated-orcid":false,"given":"Pamela","family":"Dyer","sequence":"additional","affiliation":[{"name":"Naval Postgraduate School, Monterey, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8859-8320","authenticated-orcid":false,"given":"Kristin","family":"Giammarco","sequence":"additional","affiliation":[{"name":"Naval Postgraduate School, Monterey, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-1223-3530","authenticated-orcid":false,"given":"Manfred","family":"Koethe","sequence":"additional","affiliation":[{"name":"88solutions Corporation, San Diego, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0007-7032-0340","authenticated-orcid":false,"given":"John","family":"Hester","sequence":"additional","affiliation":[{"name":"Imandra, Austin, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0009-3945-5639","authenticated-orcid":false,"given":"Jamie","family":"Smith","sequence":"additional","affiliation":[{"name":"Imandra, Austin, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5930-7563","authenticated-orcid":false,"given":"Christoph","family":"Grimm","sequence":"additional","affiliation":[{"name":"Kaiserslautern University of Technology, Kaiserslautern, Germany"}]}],"member":"320","published-online":{"date-parts":[[2024,10,31]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Proceedings of the 24th ACM SIGPLAN Conference Companion on Object Oriented Programming systems languages and applications. ACM, 1031--1040","author":"Auguston Mikhail","year":"2009","unstructured":"Mikhail Auguston. 2009. Monterey Phoenix, or how to make software architecture executable. In Proceedings of the 24th ACM SIGPLAN Conference Companion on Object Oriented Programming systems languages and applications. ACM, 1031--1040."},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1598732.1598733"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1002\/inst.12367"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1109\/QEST.2006.59"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-76773-0"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1002\/sys.21675"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-43681-9_5"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10270-020-00806-5"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.3390\/systems6040046"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-021-00532-9"},{"key":"e_1_3_2_1_11_1","volume-title":"The nuXmv Symbolic Model Checker","author":"Cavada Roberto","unstructured":"Roberto Cavada, Alessandro Cimatti, Michele Dorigatti, Alberto Griggio, Alessandro Mariotti, Andrea Micheli, Sergio Mover, Marco Roveri, and Stefano Tonetta. 2014. The nuXmv Symbolic Model Checker. In Computer Aided Verification, Armin Biere and Roderick Bloem (Eds.). Springer International Publishing, Cham, 334--342."},{"key":"e_1_3_2_1_12_1","volume-title":"OCRA: A Tool for Checking the Refinement of Temporal Contracts. In 28th IEEE\/ACM International Conference on Automated Software Engineering (ASE)","author":"Cimatti Alessandro","year":"2013","unstructured":"Alessandro Cimatti, Michele Dorigatti, and Stefano Tonetta. 2013. OCRA: A Tool for Checking the Refinement of Temporal Contracts. In 28th IEEE\/ACM International Conference on Automated Software Engineering (ASE), Ewen Denney, Tevfik Bultan, and Andreas Zeller (Eds.). IEEE, 702--705."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.5220\/0010269702620269"},{"key":"e_1_3_2_1_14_1","volume-title":"Proc. 5th Int. Workshop of Software Verification and Formal Methods for ML-Enabled Autonomous Systems (FoMLAS) and 15th Int. Workshop on Numerical Software Verification (NSV). 78--95","author":"Desmartin Remi","year":"2022","unstructured":"Remi Desmartin, Grant O. Passmore, and Ekaterina Komendantskaya. 2022. Neural Networks in Imandra: Matrix Representation as a Verification Choice. In Proc. 5th Int. Workshop of Software Verification and Formal Methods for ML-Enabled Autonomous Systems (FoMLAS) and 15th Int. Workshop on Numerical Software Verification (NSV). 78--95."},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3551357.3551372"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11219-023-09617-5"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1002\/stvr.402"},{"key":"e_1_3_2_1_18_1","volume-title":"System Behavior Specification Verification and Validation (V&V)","author":"Giammarco Kristin","unstructured":"Kristin Giammarco. 2024. System Behavior Specification Verification and Validation (V&V). John Wiley & Sons, Hoboken, NJ, 219--240."},{"key":"e_1_3_2_1_19_1","volume-title":"Documentation of the Gamma Statechart Composition Framework v0.9","author":"Graics Bence","unstructured":"Bence Graics. 2016. Documentation of the Gamma Statechart Composition Framework v0.9. Technical Report. Budapest Univ. of Technology and Economics, Dept. of Measurement and Information Systems. https:\/\/tinyurl.com\/yeywrkd6"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-52183-6_2"},{"key":"e_1_3_2_1_21_1","unstructured":"Alex Hazle and James Towers. 2020. Good Practice in MBSE Model Verification and Validation."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/32.588521"},{"key":"e_1_3_2_1_23_1","volume-title":"Software Abstractions: Logic, Language, and Analysis","author":"Jackson Daniel","year":"2012","unstructured":"Daniel Jackson. 2012. Software Abstractions: Logic, Language, and Analysis. The MIT Press, Cambridge, Massachusetts."},{"key":"e_1_3_2_1_24_1","volume-title":"Formal Methods for Open Object-Based Distributed Systems","author":"Latella Diego","unstructured":"Diego Latella, Istvan Majzik, and Mieke Massink. 1999. Towards a Formal Operational Semantics of UML Statechart Diagrams. In Formal Methods for Open Object-Based Distributed Systems, Paolo Ciancarini, Alessandro Fantechi, and Robert Gorrieri (Eds.). Springer US, Boston, MA, 331--347."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ifacol.2017.08.1309"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/SYSOSE.2015.7151961"},{"key":"e_1_3_2_1_27_1","unstructured":"OMG. 2024. Kernel Modeling Language. http:\/\/www.omg.org\/spec\/KerML\/1.0"},{"key":"e_1_3_2_1_28_1","unstructured":"OMG. 2024. OMG Systems Modeling API and Services. http:\/\/www.omg.org\/spec\/SystemsModelingAPI\/1.0"},{"key":"e_1_3_2_1_29_1","unstructured":"OMG. 2024. OMG Systems Modeling Language. http:\/\/www.omg.org\/spec\/SysML\/2.0"},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-51054-1_30"},{"key":"e_1_3_2_1_31_1","volume-title":"Proc. 24th Int. Symposium on Formal Methods (FM). 717--721","author":"Passmore Grant Olney","year":"2021","unstructured":"Grant Olney Passmore. 2021. Some Lessons Learned in the Industrialization of Formal Methods for Financial Algorithms. In Proc. 24th Int. Symposium on Formal Methods (FM). 717--721."},{"key":"e_1_3_2_1_32_1","volume-title":"Automated Deduction - CADE 26, Leonardo de Moura (Ed.)","author":"Passmore Grant Olney","unstructured":"Grant Olney Passmore and Denis Ignatovich. 2017. Formal Verification of Financial Algorithms. In Automated Deduction - CADE 26, Leonardo de Moura (Ed.). Springer International Publishing, Cham, 26--41."},{"key":"e_1_3_2_1_33_1","volume-title":"22nd International Conference on Software & Systems Engineering and their Applications","author":"P\u00e9tin Jean-Fran\u00e7ois","year":"2010","unstructured":"Jean-Fran\u00e7ois P\u00e9tin, Dominique Evrot, G\u00e9rard Morel, and Pascal Lamy. 2010. Combining SysML and formal methods for safety requirements verification. In 22nd International Conference on Software & Systems Engineering and their Applications. Paris, France, CDROM."},{"key":"e_1_3_2_1_34_1","volume-title":"DVCon Europe 2023","author":"Post Sebastian","unstructured":"Sebastian Post and Christoph Grimm. 2023. Co-Design of Automotive Boardnet Topology and Architecture. In DVCon Europe 2023; Design and Verification Conference and Exhibition Europe. VDE-Verlag, 42--49."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1109\/SOSE62659.2024.10620947"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.23919\/FMCAD.2017.8102257"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.3311\/MINISY2024-008"}],"event":{"name":"MODELS Companion '24: ACM\/IEEE 27th International Conference on Model Driven Engineering Languages and Systems","location":"Linz Austria","acronym":"MODELS Companion '24","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering","Johannes Kepler University Linz","IEEE CS"]},"container-title":["Proceedings of the ACM\/IEEE 27th International Conference on Model Driven Engineering Languages and Systems"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3652620.3687820","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3652620.3687820","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T00:04:01Z","timestamp":1750291441000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3652620.3687820"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,9,22]]},"references-count":37,"alternative-id":["10.1145\/3652620.3687820","10.1145\/3652620"],"URL":"https:\/\/doi.org\/10.1145\/3652620.3687820","relation":{},"subject":[],"published":{"date-parts":[[2024,9,22]]},"assertion":[{"value":"2024-10-31","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}