Ansys SCADE Suite’s code generator fulfills the specifications provided in the model without the need for code verification. As a result, it is crucial to verify that the model’s behavior is correct. Our software comes equipped with multiple model-level analyses to verify model correctness and ensure a short development time. You’ll be able to perform static analysis of the model. Static analysis of the model (i.e., checks that the model is consistent, data flows are properly typed, initializations are properly done) are achieved by the front-end of the code generator and is therefore qualified at the highest levels for the various software safety standards. With the Rule Checker, you can customize and add specific checks using a Python-based framework that supports a justification mechanism for required or advisory rules.
Ansys SCADE Suite Design Verifier is a verification assistant that formally expresses and assesses safety requirements, providing a productive way to find bugs early in the development process. It is powered by Prover® Technology and supported by a multicore-enabled formal proof engine with floating point computation support.