SAWS2 - Safety Analysis, Validation and Verification for SysML v2
SAWS2 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.
SAWS2 is a 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.
SAWS2 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, nuXmv, and xSAP.
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.
The integration with nuXmv enables the verification of SysML v2 state machines with powerful state of the art SMT-based model checking algorithms that combine search-based techniques with automated deduction and abstraction refinement.
Thanks to the integration with OCRA, SAWS2 provides validation of assumption/guarantee properties in contracts as well as checks on contract refinements and composite contract implementations exploiting the model checker. Model checking of state machines can be therefore scaled up by analyzing the system model compositionally, exploiting the contract-based decomposition.
Finally, fault injection enables Fault Tree Analysis and Failure Mode and Effect Analysis. SAWS2 uses xSAP as backend to generate fault trees and FMEA tables. A partial support to Fault Detection and Isolation provides Diagnosability Analysis and generation of minimum observables set. Counterexample traces, fault trees, and FMEA tables are reported in the tool by means of dedicated views.
Publications
[1] Molnár Vince; Graics Bence; Vörös András; Tonetta Stefano; Cristoforetti Luca; Kimberly Greg; Dyer Pamela; Giammarco Kristin; Koethe Manfred; Hester John; Smith Jamie; Grimm Christoph, Towards the Formal Verification of SysML v2 Models.
[2] Alberto Debiasi., Felicien Ihirwe., Pierluigi Pierini., Silvia Mazzini., and Stefano Tonetta. 2021. Model-based Analysis Support for Dependable Complex Systems in CHESS. In Proceedings of the 9th International Conference on Model-Driven Engineering and Software Development - MODELSWARD. INSTICC, SciTePress, 262–269.
Contacts
Stefano Tonetta <tonettas@fbk.eu>
Luca Cristoforetti <cristofo@fbk.eu>