---

6.1 Verification Checks and Errors

A prerequisite for running the verification checks is for Dezyne code to be syntactically correct: any parse error prohibits the verification from running and must be fixed first. Apart from syntactic parse errors, the parser also checks for a number of so-called “well-formedness” errors. A “well-formedness” error is a static check, i.e. a check that the parser can perform without considering runtime behavior (see See Invoking dzn parse and See Well-formedness).

Dezyne verifies for interfaces and for components:

deadlock

A deadlock in an interface occurs when the interface reaches a state in which no in-events are specified.

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. Each component by itself can be verified as being deadlock free and within Dezyne this deadlock property is compositional, which means that 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:

error: deadlock in model <name>

unreachable code

An unreachable code error occurs when there is no code path possible that ever leads to the execution of the code.

illegal

A trigger that is not handled in a certain state, results in an illegal. For components this is also verified for the use of the interfaces of its requires ports.

Upon violation, the following error is reported:

error: illegal action performed in model <name>

livelock

A livelock in an interface occurs when in a certain state an inevitable event can occur without any restriction, i.e., its state does not change. This could starve the client that is interacting with this interface.

A livelock in a component occurs when it is permanently busy with internal behavior and fails to serve a provides port. For example, due to a design error such that the design is constantly interacting with its requires ports and starving a provides port; or due to the arrival rate of unconstrained external events such that processing them starves a provides port. 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 a component’s provides port.

Upon violation, the following error is reported: livelock in model <name>

range error

Every possible assignment to a subint variable must be within its defined range.

Upon violation, the following error is reported:

error: integer range error in model <name>

type error

A trigger of a typed (i.e., non-void) event must reply a value of the type of the event.

Upon violation, the following error is reported

error: type error in model <name>

Note that trivial cases that can be checked statically, may be reported by the parser (See Well-formedness).

In addition, Dezyne verifies for interfaces:

observable non-determinism

Interfaces may specify non-deterministic behavior, as long as this non-determinism is observable by the client of that interface: after getting the response from the interface, a client must be able to determine what state the interface is in.

The snippet below shows observable non-determinism, i.e., an example of allowed non-determinism:

…
[idle] on hello: {world; idle=false;}
[idle] on hello: cruel;
…

in the idle state, upon sending hello either world or cruel may happen. This non-deterministic choice cannot be predicted. However, when the client sees world, the state of the interface is not idle, after seeing cruel, the state is idle.

This is an example of non-observable non-determinism, which is not allowed:

…
[idle] on hello: {world;idle=false;}
[idle] on hello: world;
…

as for a client it is impossible to tell if the interface is in state idle or in state not idle.

Upon violation, the following error is reported:

error: interface <name> is unobservably non-deterministic

In addition, Dezyne verifies for components:

compliance

The component together with its required interfaces implements the component behavior. The compliance check verifies that the component together with the required interfaces implements the behavior specified in the provided interface(s), i.e., whether the component honors its contracts.

Upon violation, the following error is reported:

error: component <name> is non-compliant with interface(s)\
    of provides port(s)

determinism

Components in Dezyne are required to be deterministic. The most common cause of non-determinism in a component is the ambiguous declaration of an event, often due to overlapping guards, i.e., in one state, for an event two different imperative statements are specified. Upon violation the following error is reported:

error: component <name> is non-deterministic

The event trace will indicate where and under which condition (state) the ambiguity occurs in the component behavior. Simulation of the corresponding event trace can be used to determine the exact location of the error in the input.

queue full

a Dezyne component 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. The component queue size can be specified for verification with the --queue-size option. The default queue size is 3.

Upon violation, the following error is reported

error: queue full in model <name>

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.