Features

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, SAWS² 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. SAWS² 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:

A counterexample trace from nuXmv

A fault tree generated by xSAP

A FMEA table generated by xSAP