Towards the Formal Verification of SysML v2 Models

Abstraction

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.

较早探讨有关SysML v2模型的论文，虽然只是发在MODELS-C上。本文的作者团队来自是布达佩斯大学ftsrg组(Fault Tolerant Systems Research Group)。本文围绕SysML v2，介绍了几种形式化验证工具，并结合案例进行了说明。第二节介绍SysML v2中的与本文有关的要素。第三节介绍了形式化方法的一些特点。第四节介绍了五款工具，分别是：

  • SysMD（一种基于SysML v2进行需求建模与开发的工具）
  • MP-Firebird（美国海军用于形式化建模的框架+工具）
  • Gamma（ftsrg组研发的一套Eclipse开源形式化验证套件）
  • Imandra（一种云自动推理平台）
  • SAVVS（用于SysML v2的安全分析与验证的Eclispe工具）

第五节一口气介绍了五小段SysML v2的例子，然后用上述这些工具应用在这些案例中，分别展现他们各自的功能。结论是向大家展示SysML v2在形式化验证方面的能力，特别是文本的输入输出是如何被呈现的。