This Dezyne example is Arno Moonen’s submission for the Dezyne Challenge 2016. The goal of the example is to illustrate the modelling of a distributed controller in Dezyne and to show an example of abstraction of required interfaces.
The state machine is distributed over multiple sub-systems. Each sub-system contains its own Dezyne component, executed on its own processor. All sub-systems provide their status/services to the top-level main-controller, which contains a Dezyne component.
The design according to the architecture diagram is shown below.
The following figures illustrate the specified behaviour for the two interfaces:
IMasterControl (the top level interface to the controller):
The behaviour of the Master controller summarises to: When the controller is Available thresholds can be set to the slaves. Additionally, the client of the controller is informed via notifications whether the controller is Available or Unavailable.
ISlaveControl (the sub-system interface):
The behaviour of a slave summarises to: When the slave is available a threshold can be set. Additionally, the client of the slave (in our case the controller) is informed via notifications whether the slave is Available or Unavailable.
The behaviour specified for the Master controller ensures the following:
the Master is available when all its slaves are available
when SetThresholds is received, SetThreshold is sent to all slaves, and the received result is replied: true if all slaves returned true, false if one of the slaves returned false.
The Master controller component makes use of the “external” keyword for all interfaces.
When performing component verification you will get "Error: Queue full!". Verification assumes that the slaves generate output events Available and Unavailable at a higher rate than the master can handle. This results in an infinite queue depth! Therefore, even with a higher queue depth (using -q option) Dezyne is not able to verify this component. Dezyne cannot verify because of a queue full situation but in fact this is a very good error message from Dezyne illustrating that the model is incorrect.
To prevent a full queue, acknowledgement is added on the ISlaveControl interface event. In this way the master has to acknowledge an output event before the slave can send another output event.
After adding the acknowledgements the Master component verification fails due to a race condition. There is a trace where slave1 becomes unavailable, while the master is not aware of it yet, due to delay in communication of the Unavailable event. Therefore, SetThreshold event needs to return (enum value) Unavailable.
After fixing the race condition you will see a successful verification.
Abstraction of required interfaces
In practice, a system can have more than two sub-systems. Therefore, the increase of size of interface ISlaveControl will make the Master controller increase n times the increase of interface ISlaveControl. Proposal is to abstract Inter-Process-Communication (IPC) details into separate Dezyne components. This reduces the number of states in Master controller component and reduces verification time.
The following pictures reflect the differences in behaviour specification for the sub-system interface before and after the abstraction, i.e ISlaveControl versus IpcSlaveControl:
The following figure illustrates the controller system after abstraction:
You can download the example in a zip-file from here.
Note that all of the diagrams included in this document have been produced in and exported from Dezyne. The System View and State Charts are part of the Dezyne editor. The Sequence Trace has been produced using the Dezyne simulation engine.