Solver of proof in Dymola

Question

I am new with Dymola but do you know if a solver of proof exists in Dymola. I am looking for a solver like SLDV in Simulink. SLDV is used in order to identify hidden design errors in models. It can formally verify that the design meets functional requirements. For each design error or requirements violation, it generates a simulation test case for debugging. Also SLDV generates test cases for model coverage and custom objectives to extend existing requirements-based test cases.

Thank you for your answer,

Eloise

Answer 1

There are libraries available for requirement verification. Although not exactly as you describe. Some papers about such libraries can be found here here and here

A Modelica requirement library named Modelica_Requirements may be found here