Verification in Dezyne focuses on verifying properties that are hard for humans to verify. These properties mainly concern ordering of events, asynchronous behaviour, deadlock and/or livelock. Verifying a component together with its provided and required interfaces ensures that the component behaves correctly in its environment according to the specified behaviour. For a failed check, a sequence of events is returned that leads to the error situation.
What is verified
Components developed in Dezyne can be verified, after proven to be valid
for verification, to ensure that:
There are no protocol violations between a component and its required components (in terms of their provided interfaces) This means that triggers to a required component are only sent if the respective component is in such a state where the trigger is legal, and that the component-under-verification is willing to process any triggers coming from a required component if the trigger is the result of an action specified in the required component.
The component complies to the provided interface(s) This means that all of the behaviour specified in the provided interface(s) is implemented by the component and no action specified in the component violates the protocol to which the provided interface(s) complies to.
How to verify
Press the Model verification button
that can be found on the Dezyne toolbar.
In case the model file has multiple components and or interfaces a pop-up will appear where the model to be verified can be selected.
These are the checks that will be performed:
deadlock: it checks that there are no "dead-ends" in the specified behaviour.
livelock: it checks that no continuous "internal" actions occur without serving, once-in-a-while, an "external" client.
deadlock: it checks that there are no "dead-ends" in the specified behaviour. For example, it is checked that no component requires an action from another component that cannot perform the respective action or that a component waits for an "external" trigger which fails to occur.
deterministic: in Dezyne all components are required to be deterministic. The most common cause of non-determinism in a component is overlapping guards, i.e. two different set of actions for the same might occur in a specific situation.
illegal: it checks that there are no protocol violations between a component and its required interfaces.
compliance: it checks that the component together with the required interfaces implements the behaviour: it checks that the component together with the required interfaces implements the behaviour specified in the provided interface(s).
A dialog box will appear indicating the result of the verification.
If errors were found a sequence will appear in the sequence diagram view displaying the chain of events that lead to an error.