Towards the Formal Verification of SysML v2 Models. Molnár, V., Graics, B., Vörös, A., Tonetta, S., Cristoforetti, L., Kimberly, G., Dyer, P., Giammarco, K., Koethe, M., Hester, J., Smith, J., & Grimm, C. In Proceedings of the ACM/IEEE 27th International Conference on Model Driven Engineering Languages and Systems, of MODELS Companion '24, pages 1086–1095, New York, NY, USA, 2024. Association for Computing Machinery. doi abstract bibtex Systems Modeling Language (SysML) is the de facto standard in the industry for modeling complex systems. SysML v2 is the new version of the language with reworked fundamentals. In this paper, we explore how the new formal semantics of SysML v2 can enable formal verification and various forms of automated reasoning. Formal verification involves mathematically proving the correctness of a system's design with respect to certain specifications or properties. This rigorous approach ensures that models behave as intended under all possible conditions. Through a detailed examination, we demonstrate how five specific tools - Gamma, MP-Firebird, Imandra, SAVVS, and SysMD - can formally analyze SysML v2 models. We show how these tools support the different concepts in the language, as well as the set of features and technologies they provide to users of SysML v2, such as model checking, theorem proving, contract-based design, or automatic fault injections. We propose a workflow for applying formal methods on SysML v2 models, illustrated by example models and artifacts generated by the above tools.
@inproceedings {molnar_graics_modevva24,
author = {Moln\'{a}r, Vince and Graics, Bence and V\"{o}r\"{o}s, Andr\'{a}s and Tonetta, Stefano and Cristoforetti, Luca and Kimberly, Greg and Dyer, Pamela and Giammarco, Kristin and Koethe, Manfred and Hester, John and Smith, Jamie and Grimm, Christoph},
title = {Towards the Formal Verification of {SysML v2} Models},
year = {2024},
isbn = {9798400706226},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
doi = {10.1145/3652620.3687820},
abstract = {Systems Modeling Language (SysML) is the de facto standard in the industry for modeling complex systems. SysML v2 is the new version of the language with reworked fundamentals. In this paper, we explore how the new formal semantics of SysML v2 can enable formal verification and various forms of automated reasoning. Formal verification involves mathematically proving the correctness of a system's design with respect to certain specifications or properties. This rigorous approach ensures that models behave as intended under all possible conditions. Through a detailed examination, we demonstrate how five specific tools - Gamma, MP-Firebird, Imandra, SAVVS, and SysMD - can formally analyze SysML v2 models. We show how these tools support the different concepts in the language, as well as the set of features and technologies they provide to users of SysML v2, such as model checking, theorem proving, contract-based design, or automatic fault injections. We propose a workflow for applying formal methods on SysML v2 models, illustrated by example models and artifacts generated by the above tools.},
booktitle = {Proceedings of the ACM/IEEE 27th International Conference on Model Driven Engineering Languages and Systems},
pages = {1086–1095},
numpages = {10},
keywords = {SysML V2, systems modeling, formal methods, verification and validation, automated reasoning, tools},
location = {Linz, Austria},
series = {MODELS Companion '24}
}
Downloads: 0
{"_id":"a9YrDQ45Xom3dKJSg","bibbaseid":"molnr-graics-vrs-tonetta-cristoforetti-kimberly-dyer-giammarco-etal-towardstheformalverificationofsysmlv2models-2024","author_short":["Molnár, V.","Graics, B.","Vörös, A.","Tonetta, S.","Cristoforetti, L.","Kimberly, G.","Dyer, P.","Giammarco, K.","Koethe, M.","Hester, J.","Smith, J.","Grimm, C."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","author":[{"propositions":[],"lastnames":["Molnár"],"firstnames":["Vince"],"suffixes":[]},{"propositions":[],"lastnames":["Graics"],"firstnames":["Bence"],"suffixes":[]},{"propositions":[],"lastnames":["Vörös"],"firstnames":["András"],"suffixes":[]},{"propositions":[],"lastnames":["Tonetta"],"firstnames":["Stefano"],"suffixes":[]},{"propositions":[],"lastnames":["Cristoforetti"],"firstnames":["Luca"],"suffixes":[]},{"propositions":[],"lastnames":["Kimberly"],"firstnames":["Greg"],"suffixes":[]},{"propositions":[],"lastnames":["Dyer"],"firstnames":["Pamela"],"suffixes":[]},{"propositions":[],"lastnames":["Giammarco"],"firstnames":["Kristin"],"suffixes":[]},{"propositions":[],"lastnames":["Koethe"],"firstnames":["Manfred"],"suffixes":[]},{"propositions":[],"lastnames":["Hester"],"firstnames":["John"],"suffixes":[]},{"propositions":[],"lastnames":["Smith"],"firstnames":["Jamie"],"suffixes":[]},{"propositions":[],"lastnames":["Grimm"],"firstnames":["Christoph"],"suffixes":[]}],"title":"Towards the Formal Verification of SysML v2 Models","year":"2024","isbn":"9798400706226","publisher":"Association for Computing Machinery","address":"New York, NY, USA","doi":"10.1145/3652620.3687820","abstract":"Systems Modeling Language (SysML) is the de facto standard in the industry for modeling complex systems. SysML v2 is the new version of the language with reworked fundamentals. In this paper, we explore how the new formal semantics of SysML v2 can enable formal verification and various forms of automated reasoning. Formal verification involves mathematically proving the correctness of a system's design with respect to certain specifications or properties. This rigorous approach ensures that models behave as intended under all possible conditions. Through a detailed examination, we demonstrate how five specific tools - Gamma, MP-Firebird, Imandra, SAVVS, and SysMD - can formally analyze SysML v2 models. We show how these tools support the different concepts in the language, as well as the set of features and technologies they provide to users of SysML v2, such as model checking, theorem proving, contract-based design, or automatic fault injections. We propose a workflow for applying formal methods on SysML v2 models, illustrated by example models and artifacts generated by the above tools.","booktitle":"Proceedings of the ACM/IEEE 27th International Conference on Model Driven Engineering Languages and Systems","pages":"1086–1095","numpages":"10","keywords":"SysML V2, systems modeling, formal methods, verification and validation, automated reasoning, tools","location":"Linz, Austria","series":"MODELS Companion '24","bibtex":"@inproceedings {molnar_graics_modevva24,\n\tauthor = {Moln\\'{a}r, Vince and Graics, Bence and V\\\"{o}r\\\"{o}s, Andr\\'{a}s and Tonetta, Stefano and Cristoforetti, Luca and Kimberly, Greg and Dyer, Pamela and Giammarco, Kristin and Koethe, Manfred and Hester, John and Smith, Jamie and Grimm, Christoph},\n\ttitle = {Towards the Formal Verification of {SysML v2} Models},\n\tyear = {2024},\n\tisbn = {9798400706226},\n\tpublisher = {Association for Computing Machinery},\n\taddress = {New York, NY, USA},\n\tdoi = {10.1145/3652620.3687820},\n\tabstract = {Systems Modeling Language (SysML) is the de facto standard in the industry for modeling complex systems. SysML v2 is the new version of the language with reworked fundamentals. In this paper, we explore how the new formal semantics of SysML v2 can enable formal verification and various forms of automated reasoning. Formal verification involves mathematically proving the correctness of a system's design with respect to certain specifications or properties. This rigorous approach ensures that models behave as intended under all possible conditions. Through a detailed examination, we demonstrate how five specific tools - Gamma, MP-Firebird, Imandra, SAVVS, and SysMD - can formally analyze SysML v2 models. We show how these tools support the different concepts in the language, as well as the set of features and technologies they provide to users of SysML v2, such as model checking, theorem proving, contract-based design, or automatic fault injections. We propose a workflow for applying formal methods on SysML v2 models, illustrated by example models and artifacts generated by the above tools.},\n\tbooktitle = {Proceedings of the ACM/IEEE 27th International Conference on Model Driven Engineering Languages and Systems},\n\tpages = {1086–1095},\n\tnumpages = {10},\n\tkeywords = {SysML V2, systems modeling, formal methods, verification and validation, automated reasoning, tools},\n\tlocation = {Linz, Austria},\n\tseries = {MODELS Companion '24}\n}\n\n","author_short":["Molnár, V.","Graics, B.","Vörös, A.","Tonetta, S.","Cristoforetti, L.","Kimberly, G.","Dyer, P.","Giammarco, K.","Koethe, M.","Hester, J.","Smith, J.","Grimm, C."],"key":"molnar_graics_modevva24","id":"molnar_graics_modevva24","bibbaseid":"molnr-graics-vrs-tonetta-cristoforetti-kimberly-dyer-giammarco-etal-towardstheformalverificationofsysmlv2models-2024","role":"author","urls":{},"keyword":["SysML V2","systems modeling","formal methods","verification and validation","automated reasoning","tools"],"metadata":{"authorlinks":{}}},"bibtype":"inproceedings","biburl":"https://ftsrg.mit.bme.hu/gamma/publications/publications.bib","dataSources":["aKoGt6pfXxS85NpEf","7NW6fZFrbqJL4hmfr"],"keywords":["sysml v2","systems modeling","formal methods","verification and validation","automated reasoning","tools"],"search_terms":["towards","formal","verification","sysml","models","molnár","graics","vörös","tonetta","cristoforetti","kimberly","dyer","giammarco","koethe","hester","smith","grimm"],"title":"Towards the Formal Verification of SysML v2 Models","year":2024}