Dezyne 2.18: Implicit Interface Constraints and Shared Interface State
Introduction
Dezyne is a domain specific language with code generation and verification tools developed by Verum. It is used to describe and verify event based systems using state machines. In this article I will introduce some basic concepts of Dezyne. I will start by giving examples of two interfaces and show a basic implementation of a component. Then I will introduce implicit interface constraints which is introduced in Dezyne 2.17 and shared interface state which is introduced in Dezyne 2.18 and show what the impact of these features can be on the implementation of a component.
The Motor Interface
Interfaces in Dezyne do not only define the method calls (called events) but also describes the behavior. You can specify which methods can be called when. Below is an example of an interface of a motor.
enum Result {
Ok,
Fail
};
interface Motor {
in Result Initialize(in string id);
in void Terminate();
in void Start();
in void Stop();
in void Recover();
in void Move(in double position);
in void StopMoving();
out void OnOk();
out void OnError();
behavior {
enum State {
Uninitialized,
Idle,
IdleError,
Starting,
Operational,
OperationalError,
Moving,
};
State state = State.Uninitialized;
[state.Uninitialized]
{
on Initialize: { reply(Result.Ok); state = State.Idle; }
on Initialize: reply(Result.Fail);
on Terminate: {}
}
[state.Idle]
{
on Start: state = State.Starting;
on Stop: {}
on Recover: {}
on Terminate: state = State.Uninitialized;
}
[state.IdleError]
{
on Terminate: state = State.Uninitialized;
on Stop: {}
on Recover: state = State.Idle;
}
[state.Starting]
{
on Stop: state = State.Idle;
on optional: { OnOk; state = State.Operational; }
on inevitable: { OnError; state = State.IdleError; }
}
[state.Operational]
{
on Move: state = State.Moving;
on Stop: state = State.Idle;
on StopMoving: {}
}
[state.OperationalError]
{
on StopMoving: {}
on Stop: state = State.IdleError;
}
[state.Moving]
{
on StopMoving: state = State.Operational;
on optional: { OnOk; state = State.Operational; }
on inevitable: { OnError; state = State.OperationalError; }
}
}
}
At the top the in and out events are defined. The in events are like method calls that can be made and the out events are signals that can be sent.
The interface also describes the behavior. It states when which events can be received and what possible out events can be send. Note that the interface is not always deterministic. For example, the Initialize event has two definitions. It can fail (replies Result.Fail). It can also succeed (replies Result.Ok) and then the state will become State.Idle. There are also the special events optional and inevitable that can be used to describe asynchronous out events. For example when the system is in State.Moving it can emit an OnOk or an OnError event.
The motor interface describes that a motor should be initialized and started. Starting will do a homing procedure. After that the motor can be moved to an absolute position using the Move command. If something goes wrong an OnError event will be send. Then the motor must be recovered and restarted (re-homed).
A goal of Dezyne is that the behavior of the interfaces and components can be verified. It will check for all kinds of problems and in particular it will check if a component correctly uses all of its ports (a port is an instance of an interface). By making the interfaces more strict, you can prevent all kinds of mistakes in the implementation of the components. It’s a bit like the borrow checker in Rust, but in Dezyne you define the usage rules yourself at the abstraction level of the application domain.
The Stage Interface
The next interface I want to introduce is the Stage interface:
interface Stage {
in Result Initialize();
in void Terminate();
in void Start();
in void Stop();
in void Recover();
in void Move(in double x, in double y);
in void StopMoving();
out void OnOk();
out void OnError();
behavior {
enum State {
Uninitialized,
Idle,
IdleError,
Starting,
Operational,
OperationalError,
Moving,
};
State state = State.Uninitialized;
[state.Uninitialized]
{
on Initialize: { reply(Result.Ok); state = State.Idle; }
on Initialize: reply(Result.Fail);
on Terminate: {}
}
[state.Idle]
{
on Start: state = State.Starting;
on Stop: {}
on Recover: {}
on Terminate: state = State.Uninitialized;
}
[state.IdleError]
{
on Stop: {}
on Recover: state = State.Idle;
}
[state.Starting]
{
on optional: { OnOk; state = State.Operational; }
on inevitable: { OnError; state = State.IdleError; }
on Stop: state = State.Idle;
}
[state.Operational]
{
on Move: state = State.Moving;
on Stop: state = State.Idle;
on StopMoving: {}
}
[state.OperationalError]
{
on StopMoving: {}
on Stop: state = State.IdleError;
}
[state.Moving]
{
on StopMoving: state = State.Operational;
on optional: { OnOk; state = State.Operational; }
on inevitable: { OnError; state = State.OperationalError; }
}
}
}
This interface looks a lot like the Motor interface. It is mostly the same but the idea is that it uses two motors to be able to move to (x, y) positions. The two motors will be controlled concurrently.
StageImpl Using Dezyne 2.16
Below is an example of a possible implementation of the Stage component in Dezyne 2.16. You will have to follow the interfaces strictly in this version of Dezyne. When the interface states that for example the Terminate event should be handled, the component must provide an implementation. But also if the interface states that for example the Initialized event should not be handled, the component is not allowed to implement it (like in the State.Operational).
There is no way to inspect the state of the provided and required interfaces. The component should track the state itself to make sure it knows which events are allowed to be send to its ports and which events it must be able to respond to. Design patterns have been developed to make this manageable. These patterns have been applied here, and because of that the implementation still looks pretty okay.
In the example below the state of the Stage interface has been copied and on top of that the Starting and Moving states have been expanded to keep track of the important states of the two Motor ports.
component StageImplOld {
provides Stage api;
requires Motor xaxis;
requires Motor yaxis;
behavior {
enum State {
Uninitialized,
Idle,
IdleError,
StartingTwo,
StartingOne,
Operational,
OperationalError,
MovingTwo,
MovingOne
};
State state = State.Uninitialized;
[state.Uninitialized]
{
on api.Initialize():
{
Result res = Result.Ok;
if (res.Ok) res = xaxis.Initialize($"xaxis"$);
if (res.Ok) res = yaxis.Initialize($"yaxis"$);
if (res.Ok) state = State.Idle;
else xaxis.Terminate();
reply(res);
}
on api.Terminate(): {}
}
[state.Idle]
{
on api.Terminate():
{
xaxis.Terminate();
yaxis.Terminate();
state = State.Uninitialized;
}
on api.Start():
{
xaxis.Start();
yaxis.Start();
state = State.StartingTwo;
}
on api.Stop(): {}
on api.Recover(): {}
}
[state.IdleError]
{
on api.Terminate():
{
xaxis.Terminate();
yaxis.Terminate();
state = State.Uninitialized;
}
on api.Stop():
{
xaxis.Stop();
yaxis.Stop();
}
on api.Recover():
{
xaxis.Recover();
yaxis.Recover();
state = State.Idle;
}
}
[state.StartingOne || state.StartingTwo]
{
on api.Stop():
{
xaxis.Stop();
yaxis.Stop();
state = State.Idle;
}
on xaxis.OnOk(), yaxis.OnOk():
{
[state.StartingTwo] state = State.StartingOne;
[state.StartingOne]
{
api.OnOk();
state = State.Operational;
}
}
on xaxis.OnError(), yaxis.OnError():
{
xaxis.Stop();
yaxis.Stop();
api.OnError();
state = State.IdleError;
}
}
[state.Operational]
{
on api.Stop():
{
xaxis.Stop();
yaxis.Stop();
state = State.Idle;
}
on api.StopMoving(): {}
on api.Move(x, y):
{
xaxis.Move(x);
yaxis.Move(y);
state = State.MovingTwo;
}
}
[state.OperationalError]
{
on api.Stop():
{
xaxis.Stop();
yaxis.Stop();
state = State.IdleError;
}
on api.StopMoving():
{
xaxis.StopMoving();
yaxis.StopMoving();
}
}
[state.MovingOne || state.MovingTwo]
{
on api.StopMoving():
{
xaxis.StopMoving();
yaxis.StopMoving();
state = State.Operational;
}
on xaxis.OnOk(), yaxis.OnOk():
{
[state.MovingTwo] state = State.MovingOne;
[state.MovingOne]
{
api.OnOk();
state = State.Operational;
}
}
on xaxis.OnError(), yaxis.OnError():
{
xaxis.StopMoving();
yaxis.StopMoving();
api.OnError();
state = State.OperationalError;
}
}
}
}
One could make this implementation more compact by combining events for different states. For example the implementation of Terminate could be shared by State.Unintialized, State.Idle and State.IdleError. I do not like to do that because it is less clear, especially for larger models. I will come back to this when discussing Dezyne 2.18.
Dezyne 2.17 – Introduction of Implicit Interface Constraints
With implicit interface constraints the component can provide an implementation of an in event even if the interface states it will not be received. In our example above we could define the Initialize and Terminate events at the top level, without any guards, because the implementation is always the same. Less state will have to be tracked. This can reduce the amount of needed code and clean up clutter.
Dezyne 2.18 – Introduction of Shared Interface State
For developers who have used ASD or are using Coco, it feels natural that you have to repeat the interface state machine in the implementation of the component. But is this really needed? Why can we not just inspect the state of our ports? The verifier does it, the simulation does it, why not the component itself? I have given some Dezyne based courses and this is a question I have gotten a few times.
Dezyne 2.18 makes it possible to inspect the state of the ports. It can be used in guards and if statements. A good use is to use it for invariant checks. Most importantly, it can obliterate (together with implicit interface constraints) most state management in the component.
Rewrite of the StageImpl
Using these two new features the StageImpl component can be written as follows:
component StageImpl {
provides Stage api;
requires Motor xaxis;
requires Motor yaxis;
behavior {
on api.Initialize():
{
Result res = Result.Ok;
if (res.Ok) res = xaxis.Initialize($"xaxis"$);
if (res.Ok) res = yaxis.Initialize($"yaxis"$);
if (res.Fail) xaxis.Terminate();
reply(res);
}
on api.Terminate():
{
xaxis.Terminate();
yaxis.Terminate();
}
on api.Start():
{
xaxis.Start();
yaxis.Start();
}
on api.Stop():
{
xaxis.Stop();
yaxis.Stop();
}
on api.Recover():
{
xaxis.Recover();
yaxis.Recover();
}
on api.Move(x, y):
{
xaxis.Move(x);
yaxis.Move(y);
}
on api.StopMoving():
{
xaxis.StopMoving();
yaxis.StopMoving();
}
on xaxis.OnOk(), yaxis.OnOk():
{
if (xaxis.state.Operational && yaxis.state.Operational)
{
api.OnOk();
}
}
on xaxis.OnError(), yaxis.OnError():
{
if (api.state.Starting)
{
xaxis.Stop();
yaxis.Stop();
}
else
{
xaxis.StopMoving();
yaxis.StopMoving();
}
api.OnError();
}
}
}
In this example there is no state at all in the component. No tracking of the state. Because of the implicit interface constraints, the implementation the events can be done at the top level. Only for the Starting and Moving states special behavior needs to be in place for the events that are received from the motors. But because the state of the motors can also be inspected we can just check if both of them are done, and then send the OnOk event. By verifying the component you can check that the end result gives correct behavior according to the interface. To find out if the behavior is really as intended it will have to be tested.
An improvement of this implementation is that it is trivial. Besides that, almost all typos one could make will be caught by the verifier. The Initialize event, and in particular the string argument is one of the more riskier parts of this implementation. But this was also the case in the original implementation.
I discussed above that I did not like the combining of states to reduce the number of repetitions for event implementations. And one could argue that this is an extreme case of it. But I think the simplicity this gives here wins me over. I hope that this pattern will repeat for many more models in the future.
Conclusion
I think Dezyne 2.18 has introduced a very unique feature, and I am looking forward to using it more. It breaks with the things we took for granted in the domain of formal verification, and gives us a different perspective.
If you want to try out the code for yourself, you can download it here.