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.

What is verified

Components developed in Dezyne can be verified, after proven to be valid for verification

These are the checks that can be performed:

completeness

Guards in Dezyne enable and disable event clauses. It is a required that in every state of a model each event is enabled, either by being unguarded, or by having a guard that evaluates to "true" for the given state.
Upon violation, one of the following errors is reported:

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.
Upon violation, the following error is reported:

illegal

It checks that there are no protocol violations between a component and its required interfaces.
Upon violation, one of the following errors is reported:

range error

It checks that each subint variable is always within its defined range.
Upon violation, one of the following errors is reported:

type error

When a non-void event is triggered, a value has to be replied. The type of that value has to match the return type of the event.
Upon violation, the following error is reported:

queue full

A Dezyne model with provides ports has a queue where notification events are stored before they are processed. During verification it is checked that that this queue does not overflow, i.e. that it remains non-blocking. + For external requires ports a queue is used to verify the effects of communication delay. A queue size limit is used to check that events can not be delayed indefinitely.
The queue size can be specified for verification with the "-q" option. The default size is 4.
Upon violation, the following error is reported:

deadlock

A deadlock is a situation where none of the components in a system can make progress; nothing can happen and the system simply does not respond. This commonly occurs when two components each require an action from the other before they can perform any further action themselves. Another common cause is when a component is waiting for some external event which fails to occur.
In general, deadlocks can be hard to find, because the entire system needs to be reviewed to discover them and freedom from deadlocks is a property of the system as a whole. For example, component A might be waiting for B which is waiting for C while C is waiting for A. Dezyne ensures that this never happens in the following way:
Each component by itself can be verified as being deadlock free; Components can only be composed in ways that have been proven not to cause deadlock. Note: Dezyne can only verify what it knows; therefore, e.g. handwritten code can still cause deadlocks.
Upon violation, the following error is reported:

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).
Upon violation, one of the following errors is reported:

livelock

A component is said to be livelocked when it is permanently busy with internal behaviour but ceases to serve its clients. For example, due to a design error such that the design is constantly interacting with its used components and starving the client; or due to the arrival rate of unconstrained external events such that processing them starves the client. As seen from the outside of a component, this appears very similar to deadlock. The difference is that a deadlocked component does nothing at all whereas a livelocked component might be performing lots of actions, but none of them are visible to the component’s clients.
Upon violation, the following error is reported:

The checks that are executed differ for interfaces and components:

  • For interfaces:

    • completeness

    • deadlock

    • illegal

    • range error

    • type error

    • livelock

  • For components:

    • completeness

    • deterministic

    • illegal

    • range error

    • type error

    • queue full

    • deadlock

    • compliance

    • livelock

For interfaces, the illegal check, range error check, and type error check are reported as part of the deadlock check. For components, the range error check, the type error check, and queue full check are reported as part of the illegal check.

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