Introduction

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 Dezyne verification buttonthat 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:

    • For interfaces:

      • 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.

    • For components:

      • 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.

  • In the latter case the chain of events leading to an error can be further explored by stepping back and forward using simulation, see Simulating and replaying execution traces

How to identify (and localise) the cause of a reported problem and how to fix it

The data displayed in the diagram provides information to localise where the problem occurs and what "happened" before the error occurs.

The following might help to identify the cause of the reported problem:

  • inspecting the state changes and other variables via the Watch Window

  • Highlight (and jump to) the location in the model where a transition is defined by clicking on an event in the diagram

  • Rearrange the lifelines

In order to fix the problem you have to edit the model and run the verification again.

For more information about the sequence diagram view and watch window see Viewing sequence diagrams and Using the watch window