SAWS² - Safety Analysis, Validation & Verification for SysML v2

SAWS² is a set of plugins to extend the Eclipse framework with the purpose of enabling validation, formal verification, and safety analysis of formal models specified in a fragment of SysML v2. The development of SAWS² has been influenced by the OMG's Formal Methods Working Group in which the FM unit is involved.

SAWS² is the new version of SAVVS [1], rewritten from scratch and without the dependency from the SysML v2 Pilot Implementation. In turn, SAVVS can be seen as the evolution of CHESS [2], a cross-domain, model-driven, component-based and open-source tool for the development of high-integrity systems, which supports SysML v1.

SAWS² features an automatic Model-to-Model transformation, eased by the use of open-source FBK libraries and facilitates the use of formal methods tools OCRA[3], nuXmv[4], and xSAP[5].

The SysML v2 language has been enriched with ad-hoc libraries to support LTL operators, fault injection, and terms to exploit the contract-based methodology.