Hi Michael,

this feature is very fresh and there is no detailed documentation yet. I will try to upload a running example in the next few days. 
Essentially what you need to do is to formalize requirements (i.e. model the violation monitors), and create value bindings (clients are requirement attributes and providers are attributes from the system model). Then create scenarios and define which requirements can be verified using these scenario (i.e. set a "usedToVerify" dependencies from scenarios to requirements). Then define value bindings between scenarios and system model (clients are typically system model attributes, providers are scenario attributes) in order to indicate that this scenario can stimulate the system model. By clicking on the system model you can then let generate verification models (i.e. combinations of scenarios and requirements) for the selected system model. All the required bindings are inferred automatically and you can now generate Modelica code and simulate the verification models in order to see if any of the requirements are violated.

Wladimir

Hi,

I created examples for requirements formalization and Value Bindings:
http://www.ida.liu.se/~pelab/modelica/O … eBindings/
For generating verification models click on the SystemEnvironment class...

Wladimir