Simulink design verifier verify conditions at the end of execution

Hi everyone.

I created this system that simply forwards a constant =1 to a design verifier module that should prove that the constant is equal to 1, but it fails.

How is it possible that it tries to falsify it? the property constant = 1 should be always verified, or am i wrong? This simple question is related to a larger (and real) project in which i have to verify some liveness properties of a robot swarm simulation.

I tried to follow the documentation but it starts with some far complicated models and i really missed the principle.

How can i fix this? thanks.

[Pat Canny]

Hi Alessandro,

Just so I understand your workflow a bit more clearly - are you simulating the model first? Simulink Design Verifier will try to generate the shortest counterexample possible to falsify a property, but it does not generally take simulation time into account. Have you tried using a Proof Assumption to specify temporal requirements?

[Alessandro Mini]

Hi Pat.

Thanks for your help, i updated the question with a simpler example and a screenshot.

[Pat Canny]

I recreated your example, and was able to prove the property. Are the data types all doubles? (Trying to think how the property would be invalid; if there is a type mismatch, they'd be unequal by default)

[Alessandro Mini]

Hi @Pat Canny thanks for your answer, can you please give me your recreated example in order to study it in detail? i'm pretty new to this part of matlab, it would really help a lot.

I attached my file, i checked that everything is double but it keeps giving error (falsified), the problems is that Matlab seems to just plug in a counterexample value without sticking it to the model.

Even if in the model it is impossible that constant=1, it will try to to find a counterexample only for the assertion part, choosing a random real value not equal to 1, resulting in a "falsification" of the logic behimd property, but not the property itself as the given counterexample has nothing to do with the model (as it does not exist a state in which constant ~=1).

The problem is that i have to prove some safety and liveness properties, so e.g (for the liveness one) i need to check if at the end of execution some property (of the model) is valid or not, in this case constant = 1.

Maybe there is something wrong in my configuration as you succeded in proving this property, i can't really figure out what is wrong.

By the way i I really want to thank you for your help.

[Pat Canny]

Hi Alessandro,

Did you change the solver settings to Fixed-step before trying to prove properties? The model you sent usesd Variable-step, which would cause an incompatibility error.

In general, your workflow does not seem like a property proving use case, but I coud be wrong. My concern is your requirement that it be checked at the end of simulation. I'd be curious to learn more - I'm always happy to talk about property proving! Feel free to reach out using the "Contact the Simulink Design Verifier technical team" link on the Simulink Design Verifier product page.

Have you considered "grabbing" the last value using simout and adding an assertion using MATLAB Unit Test?

We also have a framework using MATLAB Unit Test and Simulink Test.