Once the model and constraints have been entered into QVtrace, you are ready to do analysis. QVtrace will rigorously verify if the model and the stated constraints are consistent, and show if and when these are not.
To Run the analysis press on the Play button on the QVtrace toolbar as shown below. While analysis is in progress, the play button will display a “Pause” symbol:
The analysis in QVtrace can be approached in two ways:
- By formally translating sets of requirements specifications and verifying the model meets these, or
- As an interactive querying process where the domain expert iteratively queries the model for expected behaviour as the system components are modelled.
The analysis is done for all constraints present in the Constraints Window and can be run from any subsystem in the model. It is important to note that the analysis will always check the entire model against all constraints present, and not just the subsystem being shown in the Design Navigation Window.
Also, running the analysis checks first the consistency of the constraints and makes sure these are properly expressed. E.g. if you write “param1 == 5” and param1 is actually a boolean variable (true or false), it will not even run the analysis against the model, it will just stop and give you a problem message stating that the constraint is inappropriately written.