Stateflow verification of models

I have two questions regarding verification of design.

Firstly, I need to verify my stateflow design, a sample model as shown below. I know that there is a component called Simulink verification tool (i.e. Model Advisor), which checks the design against popular tests. But I could not find " reachability " check. Is there any ways to have reachability check on design? Say, I want to make sure I never reach S4. If not already there, I found somewhere that we can define custom checks, but I could not find how, and could not find a working example how to define a custom check. More help is needed.

2) My second question is about the generated C/C++ code. It is very cool that we can generate C/C++ code of our Stateflow code. Is there any ways to verify C/C++ code (not visual model) in Matlab?

Answer 1

[Azzi Abdelmalek]

Maybe you need this toolbox: SystemTest

[Ariana]

Thanks. Just searched around it. How can I run this toolbox?

Answer 2

[Orion]

Hi,

You're actually asking for several toolboxes

1) The Model Advisor allows you to chek some design rules, that's all, some additional options are available

To know the model coverage rate or MC/DC, you need the toolbox V&V

To generate all possible combinations of input and try to reach every part of a model : Simulink Design Verifier

2) To Verify some C code (generated or not) : polyspace code prover and polyspace bug finder