Towards the Formal Verification of SysML v2 Models

https://m2.mtmt.hu/ eng 2026-05-25 04:04 BookChapter 35500643 VALIDATED true Funding Agency and Grant Number: German BMBF [2022-1.2.4-EUREKA-2023-00013, 2022-1.2.4-EUREKA] Funding text: We would like to thank every member of the Formal Methods Working Group who helped us write this paper with their insights and comments. We are also grateful to Ed Seidewitz and Conrad Bock, who never get tired of answering our questions. SysMD received support (GENIAL, KI4BoardNet) from the German BMBF. Gamma received support project no. 2022-1.2.4-EUREKA-2023-00013 under the 2022-1.2.4-EUREKA funding scheme. 0 false 2026-05-24T07:48:35.800+0000 2024-11-20T15:40:01.905+0000 2024-11-05T13:29:09.726+0000 true 10068239 Graics Bence /api/author/10068239 Author Bence Graics (informatika) true 2025-03-21T01:58:19.718+0000 2025-03-13T18:45:41.042+0000 true 521 Szuper Admin /api/admin/521 Admin Admin Szuper (admin) true true false true 25 25 /api/publicationtype/25 PublicationType Chapter in Book 2 true 25 BookChapter true 10000312 Conference paper true 25 25 /api/publicationtype/25 PublicationType Chapter in Book 2 true 25 BookChapter /api/subtype/10000312 Konferenciaközlemény SubType Conference paper (Chapter in Book) 228 true 10000312 true 1 /api/category/1 Category Scientific true 1 Molnár, Vince Towards the Formal Verification of SysML v2 Models 1086 1095 1086 10 2024 true true 2024 true true true true true false NONE 2026-05-24 false 11 3 11 10 0 9 11 7 1 7 7 6 6 10 1 0 11 10 11 10 0 7 7 Folyóiratcikk Journal Article 24 1 Könyvrészlet Chapter in Book 25 10 Könyv Book 23 0 Egyéb konferenciaközlemény Conference paper 31 0 Egyéb konferenciakötet Conference proceedings 32 0 Oltalmi formák Protection forms 26 0 Disszertáció Thesis 28 0 Egyéb Miscellaneous 29 0 Alkotás Achievement 22 0 Kutatási adat Research data 33 0 Folyóiratcikk Journal Article 24 0 0 0 Könyvrészlet Chapter in Book 25 0 0 0 Könyv Book 23 0 0 0 Egyéb konferenciaközlemény Conference paper 31 0 0 0 Egyéb konferenciakötet Conference proceedings 32 0 0 0 Oltalmi formák Protection forms 26 0 0 0 Disszertáció Thesis 28 0 0 0 Egyéb Miscellaneous 29 0 0 0 Alkotás Achievement 22 0 0 0 Kutatási adat Research data 33 0 0 0 2025 0 5 4 5 4 2026 0 6 6 6 6 false false false false 2025-02-03T13:29:10.342+0000 Kritikus Rendszerek Kutatócsoport (BME / VIK / MIT); Mesterséges Intelligencia és Rendszertervezés T... (BME / VIK) 3 8 2 12 0 true true 10002 English /api/language/10002 Angol Language English true 2 false true 10367 true 10017 /api/country/10017 Country United States of America true 13 /api/city/10367 City New York City, United States of America true 870 true 27759775 /api/publicationidentifier/27759775 https://doi.org/10.1145/3652620 10.1145/3652620 PublicationIdentifier DOI: 10.1145/3652620 true 6 DOI https://doi.org/@@@ /api/publicationsource/6 DOI PlainSource DOI true true 10001 /api/publicationsourcetype/10001 PublicationSourceType DOI true true 6 true false true 27759776 /api/publicationidentifier/27759776 https://www.worldcat.org/search?q=isbn%3A9798400706226 9798400706226 PublicationIdentifier ISBN: 9798400706226 true 122 ISBN https://www.worldcat.org/search?q=isbn%3A@@@ /api/publicationsource/122 ISBN PlainSource ISBN true true 10002 /api/publicationsourcetype/10002 PublicationSourceType Egyéb true false 122 true false /api/publication/35500644 ACM [ed.]. MODELS Companion '24: Proceedings of the ACM/IEEE 27th International Conference on Model Driven Engineering Languages and Systems. (2024) ISBN:9798400706226 true true 23 23 /api/publicationtype/23 PublicationType Book 3 true 23 Book MODELS Companion '24: Proceedings of the ACM/IEEE 27th International Conference on Model Driven Engineering Languages and Systems false 35500644 false true true true true 10000144 Conference proceedings true 23 23 /api/publicationtype/23 PublicationType Book 3 true 23 Book /api/subtype/10000144 Konferenciakötet SubType Conference proceedings (Book) 345 true 10000144 false Book 2024 true 1 /api/category/1 Category Scientific true 1 false Language 10002 /api/language/10002 English Angol English true 2 true PersonAuthorship 121167089 /api/authorship/121167089 Molnár, Vince [Molnár, Vince (informatika), author] Critical Systems Research Group (BUTE / FEEI / MIT); Department of Artificial Intelligence and Syst... (BUTE / FEEI) 1 0.083 true false false Author 10049620 /api/author/10049620 Vince Molnár (informatika) Molnár Vince true 10049620 true Molnár Vince true false false AuthorshipType 1 /api/authorshiptype/1 Author 0 true 0 true false true PersonAuthorship 121167090 /api/authorship/121167090 Graics, Bence [Graics, Bence (informatika), author] Critical Systems Research Group (BUTE / FEEI / MIT); Department of Artificial Intelligence and Syst... (BUTE / FEEI) 2 0.083 false false false Author 10068239 /api/author/10068239 Bence Graics (informatika) Graics Bence true true Graics Bence true false false AuthorshipType 1 /api/authorshiptype/1 Author 0 true 0 true false true PersonAuthorship 121167091 /api/authorship/121167091 Vörös, András [Vörös, András (informatika), author] Critical Systems Research Group (BUTE / FEEI / MIT); Department of Artificial Intelligence and Syst... (BUTE / FEEI) 3 0.083 false false false Author 10042280 /api/author/10042280 András Vörös (informatika) Vörös András true 10042280 true Vörös András true false false AuthorshipType 1 /api/authorshiptype/1 Author 0 true 0 true false true PersonAuthorship 121167092 /api/authorship/121167092 Tonetta, Stefano 4 0.083333336 false false false Tonetta Stefano true false false AuthorshipType 1 /api/authorshiptype/1 Author 0 true 0 true false true PersonAuthorship 121167093 /api/authorship/121167093 Cristoforetti, Luca 5 0.083333336 false false false Cristoforetti Luca true false false AuthorshipType 1 /api/authorshiptype/1 Author 0 true 0 true false true PersonAuthorship 121167094 /api/authorship/121167094 Kimberly, Greg 6 0.083333336 false false false Kimberly Greg true false false AuthorshipType 1 /api/authorshiptype/1 Author 0 true 0 true false true PersonAuthorship 121167095 /api/authorship/121167095 Dyer, Pamela 7 0.083333336 false false false Dyer Pamela true false false AuthorshipType 1 /api/authorshiptype/1 Author 0 true 0 true false true PersonAuthorship 121167096 /api/authorship/121167096 Giammarco, Kristin 8 0.083333336 false false false Giammarco Kristin true false false AuthorshipType 1 /api/authorshiptype/1 Author 0 true 0 true false true PersonAuthorship 121167097 /api/authorship/121167097 Koethe, Manfred 9 0.083333336 false false false Koethe Manfred true false false AuthorshipType 1 /api/authorshiptype/1 Author 0 true 0 true false true PersonAuthorship 121167098 /api/authorship/121167098 Hester, John 10 0.083333336 false false false Hester John true false false AuthorshipType 1 /api/authorshiptype/1 Author 0 true 0 true false true PersonAuthorship 121167099 /api/authorship/121167099 Smith, Jamie 11 0.083333336 false false false Smith Jamie true false false AuthorshipType 1 /api/authorshiptype/1 Author 0 true 0 true false true PersonAuthorship 121167100 /api/authorship/121167100 Grimm, Christoph 12 0.083333336 false true false Grimm Christoph true false false AuthorshipType 1 /api/authorshiptype/1 Author 0 true 0 true false true PublicationIdentifier 27759777 /api/publicationidentifier/27759777 DOI: 10.1145/3652620.3687820 PlainSource 6 /api/publicationsource/6 DOI PublicationSourceType 10001 /api/publicationsourcetype/10001 DOI true true true DOI DOI https://doi.org/@@@ true true 6 true IDENTICAL 10.1145/3652620.3687820 https://doi.org/10.1145/3652620.3687820 false true PublicationIdentifier 28116192 /api/publicationidentifier/28116192 WoS: 001351589800145 PlainSource 1 /api/publicationsource/1 WoS PublicationSourceType 10003 /api/publicationsourcetype/10003 Indexelő adatbázis false true true WoS WoS https://www.webofscience.com/wos/woscc/full-record/@@@ true true 1 true IDENTICAL 001351589800145 https://www.webofscience.com/wos/woscc/full-record/001351589800145 false true PublicationIdentifier 28158213 /api/publicationidentifier/28158213 Scopus: 85212206268 PlainSource 3 /api/publicationsource/3 Scopus PublicationSourceType 10003 /api/publicationsourcetype/10003 Indexelő adatbázis false true true Scopus Scopus http://www.scopus.com/record/display.url?origin=inward&eid=2-s2.0-@@@ true true 3 true IDENTICAL 85212206268 http://www.scopus.com/record/display.url?origin=inward&eid=2-s2.0-85212206268 false true PublicationIdentifier 27759778 /api/publicationidentifier/27759778 Other URL: https://dl.acm.org/doi/10.1145/3652620.3687820 PlainSource 40 /api/publicationsource/40 Other URL PublicationSourceType 10006 /api/publicationsourcetype/10006 Link true true true Egyéb URL Other URL @@@ true true 40 true https://dl.acm.org/doi/10.1145/3652620.3687820 https://dl.acm.org/doi/10.1145/3652620.3687820 false true Reference 59497965 /api/reference/59497965 1. 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. 1 false true Reference 59497966 /api/reference/59497966 2. DOI: 10.1145/1598732.1598733 2 10.1145/1598732.1598733 false true Reference 59497967 /api/reference/59497967 3. DOI: 10.1002/inst.12367 3 10.1002/inst.12367 false true Reference 59497968 /api/reference/59497968 4. DOI: 10.1109/QEST.2006.59 4 10.1109/QEST.2006.59 false true Reference 59497969 /api/reference/59497969 5. DOI: 10.1007/978-3-030-76773-0 5 10.1007/978-3-030-76773-0 false true Reference 59497970 /api/reference/59497970 6. DOI: 10.1002/sys.21675 6 10.1002/sys.21675 false true Reference 59497971 /api/reference/59497971 7. DOI: 10.1007/978-3-031-43681-9_5 7 10.1007/978-3-031-43681-9_5 false true Reference 59497972 /api/reference/59497972 8. DOI: 10.1007/s10270-020-00806-5 8 10.1007/s10270-020-00806-5 false true Reference 59497973 /api/reference/59497973 9. DOI: 10.3390/systems6040046 9 10.3390/systems6040046 false true Reference 59497974 /api/reference/59497974 10. DOI: 10.1007/s00165-021-00532-9 10 10.1007/s00165-021-00532-9 false true Reference 59497975 /api/reference/59497975 11. 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. 11 false true Reference 59497976 /api/reference/59497976 12. 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. 12 false true Reference 59497977 /api/reference/59497977 13. DOI: 10.5220/0010269702620269 13 10.5220/0010269702620269 false true Reference 59497978 /api/reference/59497978 14. 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. 14 false true Reference 59497979 /api/reference/59497979 15. DOI: 10.1145/3551357.3551372 15 10.1145/3551357.3551372 false true Reference 59497980 /api/reference/59497980 16. DOI: 10.1007/s11219-023-09617-5 16 10.1007/s11219-023-09617-5 false true Reference 59497981 /api/reference/59497981 17. DOI: 10.1002/stvr.402 17 10.1002/stvr.402 false true Reference 59497982 /api/reference/59497982 18. Kristin Giammarco. 2024. System Behavior Specification Verification and Validation (V&V). John Wiley & Sons, Hoboken, NJ, 219--240. 18 false true Reference 59497983 /api/reference/59497983 19. 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 19 false true Reference 59497984 /api/reference/59497984 20. DOI: 10.1007/978-3-031-52183-6_2 20 10.1007/978-3-031-52183-6_2 false true Reference 59497985 /api/reference/59497985 21. Alex Hazle and James Towers. 2020. Good Practice in MBSE Model Verification and Validation. 21 false true Reference 59497986 /api/reference/59497986 22. DOI: 10.1109/32.588521 22 10.1109/32.588521 false true Reference 59497987 /api/reference/59497987 23. Daniel Jackson. 2012. Software Abstractions: Logic, Language, and Analysis. The MIT Press, Cambridge, Massachusetts. 23 false true Reference 59497988 /api/reference/59497988 24. 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. 24 false true Reference 59497989 /api/reference/59497989 25. DOI: 10.1016/j.ifacol.2017.08.1309 25 10.1016/j.ifacol.2017.08.1309 false true Reference 59497990 /api/reference/59497990 26. DOI: 10.1109/SYSOSE.2015.7151961 26 10.1109/SYSOSE.2015.7151961 false true Reference 59497991 /api/reference/59497991 27. OMG. 2024. Kernel Modeling Language. http://www.omg.org/spec/KerML/1.0 27 false true Reference 59497992 /api/reference/59497992 28. OMG. 2024. OMG Systems Modeling API and Services. http://www.omg.org/spec/SystemsModelingAPI/1.0 28 false true Reference 59497993 /api/reference/59497993 29. OMG. 2024. OMG Systems Modeling Language. http://www.omg.org/spec/SysML/2.0 29 false true Reference 59497994 /api/reference/59497994 30. DOI: 10.1007/978-3-030-51054-1_30 30 10.1007/978-3-030-51054-1_30 false true Reference 59497995 /api/reference/59497995 31. 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. 31 false true Reference 59497996 /api/reference/59497996 32. 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. 32 false true Reference 59497997 /api/reference/59497997 33. Jean-François Pétin, Dominique Evrot, Gérard 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. 33 false true Reference 59497998 /api/reference/59497998 34. 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. 34 false true Reference 59497999 /api/reference/59497999 35. DOI: 10.1109/SOSE62659.2024.10620947 35 10.1109/SOSE62659.2024.10620947 false true Reference 59498000 /api/reference/59498000 36. DOI: 10.23919/FMCAD.2017.8102257 36 10.23919/FMCAD.2017.8102257 false true Reference 59498001 /api/reference/59498001 37. DOI: 10.3311/MINISY2024-008 37 10.3311/MINISY2024-008 false true /api/publication/35500643 Molnár Vince et al. Towards the Formal Verification of SysML v2 Models. (2024) In: MODELS Companion '24: Proceedings of the ACM/IEEE 27th International Conference on Model Driven Engineering Languages and Systems pp. 1086-1095<div class="BookChapter Publication long-list"> <div class="authors"> <img title="Forrásközlemény" style="float: left" src="/frontend/resources/grid/publication-core-icon.png"> <img title="Idézőközlemény" style="float: left" src="/frontend/resources/grid/publication-citation-icon.png"> <div class="autype autype0"> <span class="author-name" mtid="10049620"><a href="/gui2/?type=authors&mode=browse&sel=10049620" target="_blank">Molnár Vince (<span class="authorship-author-name">Molnár Vince</span> <span class="authorAux-mtmt"> informatika</span>) </a> </span> <span class="author-affil"><span title="Budapest University of Technology and Economics">BUTE</span>/<span title="Faculty of Electrical Engineering and Informatics">FEEI</span>/<span title=" Department of Artificial Intelligence and Systems Engineering">MIT</span>/Critical Systems Research Group; <span title="Budapest University of Technology and Economics">BUTE</span>/<span title="Faculty of Electrical Engineering and Informatics">FEEI</span>/ Department of Artificial Intelligence and Systems Engineering</span> ;    <span class="author-name" mtid="10068239"><a href="/gui2/?type=authors&mode=browse&sel=10068239" target="_blank">Graics Bence (<span class="authorship-author-name">Graics Bence</span> <span class="authorAux-mtmt"> informatika</span>) </a> </span> <span class="author-affil"><span title="Budapest University of Technology and Economics">BUTE</span>/<span title="Faculty of Electrical Engineering and Informatics">FEEI</span>/<span title=" Department of Artificial Intelligence and Systems Engineering">MIT</span>/Critical Systems Research Group; <span title="Budapest University of Technology and Economics">BUTE</span>/<span title="Faculty of Electrical Engineering and Informatics">FEEI</span>/ Department of Artificial Intelligence and Systems Engineering</span> ;    <span class="author-name" mtid="10042280"><a href="/gui2/?type=authors&mode=browse&sel=10042280" target="_blank">Vörös András (<span class="authorship-author-name">Vörös András</span> <span class="authorAux-mtmt"> informatika</span>) </a> </span> <span class="author-affil"><span title="Budapest University of Technology and Economics">BUTE</span>/<span title="Faculty of Electrical Engineering and Informatics">FEEI</span>/<span title=" Department of Artificial Intelligence and Systems Engineering">MIT</span>/Critical Systems Research Group; <span title="Budapest University of Technology and Economics">BUTE</span>/<span title="Faculty of Electrical Engineering and Informatics">FEEI</span>/ Department of Artificial Intelligence and Systems Engineering</span> ;    <span class="author-name" >Tonetta Stefano </span> ;    <span class="author-name" >Cristoforetti Luca </span> ;    <span class="author-name" >Kimberly Greg </span> ;    <span class="author-name" >Dyer Pamela </span> ;    <span class="author-name" >Giammarco Kristin </span> ;    <span class="author-name" >Koethe Manfred </span> ;    <span class="author-name" >Hester John </span> ;    <span class="author-name" >Smith Jamie </span> ;    <span class="author-name" >Grimm Christoph </span> </div> </div> <div class="title"><a href="/gui2/?mode=browse&params=publication;35500643" target="_blank">Towards the Formal Verification of SysML v2 Models</a></div> <div class="InBook"><div class="chapter-in">In:</div> <div class="authors"> <div class="autype autype-1"> <span class="author-affil">ACM</span> (eds.) </div> </div> <div class="booktitle"><a href="/gui2/?mode=browse&params=publication;35500644" target="_blank">MODELS Companion '24: Proceedings of the ACM/IEEE 27th International Conference on Model Driven Engineering Languages and Systems </a></div> <div class="conference"> Conference: <span class="location">Linz, Austria <span class="conference-date">2024.09.22. - 2024.09.27.</span> </div> <span class="publishedAt">New York City: <span class="publishers">ACM</span>, <span class="page"> pp 1086-1095 </span> <span class="year">(2024)</span> </div> <div class="pub-footer"> <span class="language" xmlns="http://www.w3.org/1999/html">Language: English | </span> <span class="identifiers"> <span class="id identifier oa_none" title="none"> <a style="color:blue" title="10.1145/3652620.3687820" target="_blank" href="https://doi.org/10.1145/3652620.3687820"> DOI </a> </span> <span class="id identifier oa_none" title="none"> <a style="color:blue" title="001351589800145" target="_blank" href="https://www.webofscience.com/wos/woscc/full-record/001351589800145"> WoS </a> </span> <span class="id identifier oa_none" title="none"> <a style="color:blue" title="85212206268" target="_blank" href="http://www.scopus.com/record/display.url?origin=inward&eid=2-s2.0-85212206268"> Scopus </a> </span> <span class="id identifier oa_none" title="none"> <a style="color:black" title="https://dl.acm.org/doi/10.1145/3652620.3687820" target="_blank" href="https://dl.acm.org/doi/10.1145/3652620.3687820"> Other URL </a> </span> </span> <span class="bookchapter-ids">Book link(s):</span> <span class="identifiers"> <span class="id identifier oa_none" title="none"> <a style="color:black" title="10.1145/3652620" target="_blank" href="https://doi.org/10.1145/3652620"> DOI </a> </span> <span class="id identifier oa_none" title="none"> <span class="isbnOrIssn"> ISBN: </span> <a style="color:black" title="9798400706226" target="_blank" href="https://www.worldcat.org/search?q=isbn%3A9798400706226"> 9798400706226 </a> </span> </span> <div class="publication-citation" style="margin-left: 0.5cm;"> <span title="" class="citingPub-count">Citing papers: 11</span> | Independent citation: 10 | Self citation: 1 | Unknown citation: 0 | Number of citations in WoS: 7 | Number of citations in Scopus: 1 | WoS/Scopus assigned: 7 | Number of citations with DOI: 11 (Not published: 3) </div> <div class="publication-citation"> <a target="_blank" href="/api/publication?cond=citations.related;eq;35500643&sort=publishedYear,desc&sort=title"> Number of cited publications: 7 </a> </div> <div class="mtid"><span class="long-pub-mtid">Publication: 35500643</span> | <span class="status-data status-VALIDATED"> Validated </span> <span class="long-book-mtid">Book: 35500644</span> Core Citing | <span class="type-subtype">Chapter in Book ( Conference paper ) </span> | <span class="pub-category">Scientific</span> | <span class="publication-sourceOfData">kézi felvitel</span> </div> <div class="lastModified">Last Modified: 2024.11.20. 16:40 Bence Graics (informatika) </div> <pre class="comment" style="margin-top: 0; margin-bottom: 0;"><u>Comments</u>: Funding Agency and Grant Number: German BMBF [2022-1.2.4-EUREKA-2023-00013, 2022-1.2.4-EUREKA] Funding text: We would like to thank every member of the Formal Methods Working Group who helped us write this paper with their insights and comments. We are also grateful to Ed Seidewitz and Conrad Bock, who never get tired of answering our questions. SysMD received support (GENIAL, KI4Bo...</pre> </div> </div>