This repository contains the complete SysML v2 models used in journal paper Formal verification, validation and safety analysis of SysML v2 models: Towards a unified workflow (as opposed to the model snippets included in the paper) submitted to the Journal of Innovations in Systems and Software Engineering.
Authors: Vince Molnár, Bence Graics, András Vörös, Stefano Tonetta, Luca Cristoforetti, Greg Kimberly, Pamela Dyer, Kristin Giammarco, Manfred Koethe, James G. Smith, Grant Passmore, Sebastian Post and Christoph Grimm.
Abstract:
The 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 and extended capabilities of SysML v2 can enable more integrated formal verification and various forms of automated reasoning like validation and safety analysis. 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 the specified conditions. Other analysis techniques can reason about functional safety or explore allowed behaviors to facilitate a better understanding of our models. Collectively, formal methods can be an indispensable tool in building higher-quality models. Through a detailed examination, we demonstrate how five specific tools - MP-Firebird, SysMD, Gamma, Imandra and SAVVS - can formally verify, validate and 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, constraint solving, contract-based design, or automatic fault injections. We propose a unified analysis and verification workflow (applicable in steps of high-level MBSE workflows or methodologies) for applying formal methods on SysML v2 models orchestrated directly from SysML itself, illustrated by example models and artifacts generated by the above tools. We demonstrate the applicability of our tools and approaches on different case studies.
SysML v2 models: