Bound Check

Prerequisite: NuSMV/nuXmv

First ensure that nuXmv or NuSMV is installed: see External Tools for instructions.

Activation

You need to ensure that the bound check is activated:
  1. Double click on the root of your project:


  2. And check "All port values are within their bounds":


  3. You will probably observe the following message:


    This informs you that the port bound analysis will be now run on all the components in the current project and that this might therefore take some resources (if your project already contains lots of components). This will be however done only once since, once the check is activated, it is only re-run for the components which are modified.
Be sure also that the configuration in which this check is activated is the one which is the "current objective".

This will trigger the check that all ports of the project are within their bounds and activate the automatic trigger of this check for every component that you might add later on to your project. It will also trigger a check for every component as soon as it is modified.

Example

Consider the following component:
State automaton

Where Input and Output have the same bounds. It is then clear that the upper bound of Output port can be exceeded when Input is set to the maximum value. Therefore, you should see, as soon after you finished drawing this automaton (and specifying the guard accordingly) an error message on the corresponding component in the model navigator:


As well as is in the editor of the containing component:


If you right-click on the error in the model navigator or in the editor, the following context menu will be shown:


Clicking on the entry will open the state automaton editor and provide a short explanation why the port can get out of bound. If you fix the transition by, say, adding a guard "Input < 255", then the error will automatically disappear.

You can also check the status of the check at any time, whether it is successful or not, by simply clicking on the "V&V Dashboard" tab of the state automaton editor:


Example 2

Consider the following component architecture:
State automaton

Where the Output of c1 has bounds "-256...255" and the Input of c2 has however "-256...254". Then you should see, just like before, an error indicating you that the bounds are not matching. You can also get more information in the context menu and see more information in the dashboard.