5 Verifying Models
5.1 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.
5.2 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, The following error is reported :
M is incomplete: e not handled
- 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 :
Component M is non-deterministic due to overlapping guards
- illegal: it checks that there are no protocol violations between a component and
its required interfaces.
Upon violation, The following error is reported :
illegal
- range error: it checks that each subint variable is always within its defined range.
Upon violation, The following error is reported :
integer range error in model M
- 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 :
type error in model M
- 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.
The queue size can be specified for verification with the "-q" option. The default size is 4.
Upon violation, The following error is reported :
queue full
- 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 :
deadlock in model M
- 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, The following error is reported :
Component M is non-compliant with interface of provided port
- 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 :
livelock in model M
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.