Interface, Component and System
When starting to model with Dezyne, it is first essential to get acquainted with the following 3 types of models: Interface, Component and System. On the left side of the figure below a diagram is shown with the well-known ‘lollipops’ that indicate an interface is provided. Such interface is provided by a component. Whereas the round forks require a particular type of interface as requested from the component. Namely, the ‘controller’ component requires an ITimer, which is provided by the ‘timer’ component instance. And the other required interface IHeater shall be supplied externally. It can be hooked up into a greater encapsulating Dezyne system or be implemented by hand as part of integration into the final software environment. Lastly, the dashed rectangle indicates grouping of component instances ‘controller’ and ‘timer’ into a system.
On the right side of the figure below the entire concept is shown in Dezyne with the ‘System View’ option. Instead of ‘lollipops’, Dezyne uses ports as the point where an interface resides. These are the small yellow rectangles with a triangle inside. Depending on its location it is either a provided port (upper boundary of a component) or a required port (on the bottom boundary). The connecting lines between a provided and required port is called a binding. This can be best compared and imagined with the (soldered) traces on a PCB board that interconnect microchips and their terminals.
Each port in a Dezyne system has a name and are specified when creating bindings between ports. In the System View, this name visually appears when hovering above the port with the mouse. As example in the figure the name ‘heater’ is revealed. The next figure shows the System model where the outer ports are introduced with the provides and requires keywords and in between the system clause it is shown how the component are instantiated and equiped with bindings with their direct environment.
Additionally, the Dezyne developer has the freedom to compose systems of systems. This pattern is often used when small subsystems need to be instantiated multiple times. As practical example think of a multi axis motion controller context. Or a logical vacuum pump that actually is composed of multiple smaller vacuum pumps that cooperate together.
Events are crossing the bindings in two directions. The ‘in events’ travel from the required-to-provided interface and the ‘out events’ vice versa. An alternative way of understanding the ‘in events’ are calls from a client to a server. And ‘out events’ can be compared with standalone callbacks from a server to a client.
Interface
With the introduction so far, we now come to the point of diving deeper into the definition of an interface. In the next figure on the left a simple interface of a Toaster controller is shown.
IController
- It first begins with introducing the API/signature (=Syntax). It has one ‘in event’ Toast() and one ‘out event’ Done().
- Then the behavior part (=Semantics), the interface declares an enum to indicate the state of the interface. The state variable defines this enum with an initial value of Ready. In this state the client can start with triggering a Toast() call. From there it transits to the Toasting state where inevitably at a certain point in time, a Done() ‘out event’ is emitted by the server side.
- Finally, as seen from the server side, the interface transits back to Ready. And when the client ‘sees’ and handles the Done() event then at -that- point it also knows the interface state is back in Ready (=Synchronization).
As you may notice, there can be a small time fraction where client and server are out-of-sync related to emiting and final processing of the Done() ‘out event’. This is completely normal for systems that model asynchronous behaviour. That’s being specified in this example.
Also what you may notice is that an Interface in Dezyne is not just a simple API. With syntax, semantics and synchronization the Dezyne developer has to be precise with modelling and the model checker will verify all these aspects.
IHeater
The IHeater interface definition on the right in the figure shows an alternative to the enum State-based solution. Namely a boolean when it only concerns two states. From best practices point of view, the boolean state variable is fine for tiny interfaces and where its naming is unambiguously clear. For larger interfaces the best practice is to organize via State enums. (This topic returns in a seperate article.)
In this interface only ‘in events’ are provided which logically means it is an all synchronous interface. This interface is an example of a strict interface. Meaning the client may only Start() when it is not heating and only Stop() when it was previously started. Any deviating attempt (for instance call Start() twice) will be noticed by the verifier and reported as an error. Such strictness also makes sure that heating is stopped the next time we want to start it again. Concluding, all these benefits leads to a final system that is behaving reliable and predictable.
ITimer
The ITimer interface looks as following:
extern MilliSeconds $size_t$;
interface ITimer
{
in void Sleep(in MilliSeconds waitingTimeMs);
in void Create(in MilliSeconds timeoutValueMs);
in void Cancel();
out void Timeout();
behavior
{
bool running = false;
[!running]
{
on Sleep: {}
on Create: running = true;
on Cancel: {}
}
[running]
{
on Cancel: running = false;
on inevitable: { Timeout; running = false; }
}
} // behaviour
} // interface
Like the IHeater interface earlier it also uses a Boolean to keep track of the current state. The Timer service mainly offers two sorts of functionality. First one is a Sleep() for a specified amount of time and the other one is the running of an expiry timer. Both functionalities can be used in the Toaster case to time the toasting of a sandwich. But as we will learn in the next article, they have their specific side effects on synchronous and asynchronous behaviour. In case of kicking off the expiry timer and have it running, there is a possibility to Cancel() the timer. Also, in the ‘not-running’ state, cancellation is allowed and this follows a pattern to always allow cancellation even when the timer is not running. This makes the using component simpler when it has to deal with more complexity.
To specify the time to Sleep() or Create() you’ll see that the argument type is an extern. This can be viewed as an alias to a string literal which will be used during code generation. In this case the extern ‘MilliSeconds’ translates to the size_t type (in C++). The use of the extern keyword allows for aliasing potentially long string literals. Think of a type with a long trail of namespacing. But in the model, you will use the ‘short’ name of the extern, which keeps the model readable.
When (starting) modelling with Dezyne, the developer always begins with defining interfaces that surround a component before diving into the modelling of a component. Because obviously the component should first know what functionality it has to offer and then which interfaces it needs to control.
Interface as contract and event exchange
One more thing about an interface is needed to be explained. Namely, an interface sits in between two components and therefore it is considered a contract between the two parties. What you notice is that an interface is a ‘black box view’ of the other side and no specific implementation details are included. And that is a good thing because otherwise the state space would blow up exponentially. Also, the beauty of an interface is that it is an independent point where you vary different implementations underneath; as long as they comply of course.
Lastly, with an interface in between two components it means that ‘the only thing’ the components ‘see’ are the events that are exchanged. Observing the order of these events allows the components to keep in sync with state transitions that are modelled in the interface behaviour. When modelling, simulating and diagnosing verification errors it is important to remember thinking in which events were sent around.
Component
The final element explained in this article is the component. As introduced earlier, a component must provide an interface and has the freedom to require other interfaces that it will control. As a best practice, it is advised to use a State-based enum to model the state machine of a component. Initially, one will notice much similarity with the provided interface behaviour. But as soon as when extending the component, more (intermediate) states are expected to be added. In contrary with an interface (black box view), the component model is considered the ‘white box view’ of the functionality. In the component it is exactly being specified how used interfaces are being controlled and with what parameter arguments. You may wonder why parameter arguments were absent in the interface behaviour, that’s because at that point they are not relevant. Only the events and the state transitions. However, inside the component it is relevant because as for example the Timer must know exactly how many milliseconds it must wait before the timer expires with a Timeout() out event.
component Controller
{
provides IController api;
requires IHeater heater;
requires ITimer timer;
behavior
{
enum State {Ready, Toasting};
State s = State.Ready;
[s.Ready]
{
on api.Toast():
{
heater.Start();
timer.Create($60 * 1000$);
s = State.Toasting;
}
}
[s.Toasting]
{
on timer.Timeout():
{
heater.Stop();
s = State.Ready;
api.Done();
}
}
} // behavior
} // component
In this component of the Toaster controller, we modelled a very simple Toast() that will start the heater element and create the expiry timer with 60 seconds. Also here you’ll notice a string literal ($...$) which will be literally be included in the generated code. Later on you will discover Data Variables to store data and to pass on as parameter arguments like this timer. After kicking off the timer the component sits in the Toasting state where it will inevitably receive a Timeout() out event. Subsequently it stops the heater and emits a Done() out event to the interface client.