3.1.2 Interfaces as abstraction of a component’s behaviour

In the Dezyne Modelling language, an interface contains the definition of the events, their direction and optionally their parameters, and a specification of the externally visible behaviour of the component that will provide an implementation of the interface.

With behaviour we mean which events (or method calls) can be received and can be sent at which stages in the execution process, or in other words the protocol a user of the interface should obey. In the case of the Application and ProtocolStack the interface defines that the ProtocolStack should first be enabled before anything else can be done with it, that a connectReq must be followed by a connectReqRes and that it is not allowed to send a second connectReq before a connectReqRes has been received.

As described above, components use or provide functionality via interfaces and not by interacting directly with other components. Therefore, interface specifications can not contain component implementation details.

An interface specification that defines part of the ProtocolStack interface (the enabling and disabling) in the example above could look like:

interface IProtocolStack
{
  enum Result                               // enumeration type used for the reply value of
  {                                         // the event enable
    Ok,
    Failed
  };
  in Result enable();                       // in event to enable the ProtocolStack
                                            //   the event will return if enabling was successful or not
  in void disable();                        // in event to disable the ProtocolStack
  behaviour                                 // the specification of the externally visible behaviour
  {
      enum State {OFF, ON};
      State state = State.OFF;
      [state.OFF]
      {
          on enable:                        // One possible response to enable is Ok
          {
             reply(Result.Ok);
             state = State.ON;
          }
          on enable: reply(Result.Failed);  // The other possible response to enable is Failed
          on disable: illegal;              // Disabling the Protocol Stack is not allowed in OFF state
      }
      [state.ON]
      {
          on enable: illegal;               // Enabling the Protocol Stack is not allowed in ON state
          on disable: state = State.OFF;
      }
  }
}

In the interface specification three things stand-out: 1) actions for all possible events have to be specified, 2) events can be marked as ’illegal’ and 3) all possible replies are specified.

1) In the interface specification above a state machine has been introduced to define what is allowed at each stage: the protocol specified by this state machine must be obeyed. In order to have an unambiguously defined interface in each state, the actions for all possible events have to be specified. That is why you see for each state the "on enable" and "on disable" statement. A Dezyne model is complete when it specifies for each possible state and each possible incoming event what happens in terms of actions when this event is received while the interface is in this particular state. Dezyne will check that the specification is complete and thereby ensure that there will be no undefined actions for all possible events. In Dezyne this is referred to as a completeness check.

2) For completely specifying the behaviour of an interface, one must specify also all actions that should not happen or are not allowed at certain stages, i.e., will not be serviced when the component implementing the interface is in a particular state. This is done by marking actions that are not allowed as illegal. The Dezyne verification will verify that all components using the interface will adhere to it and in case a component is sending an event that is illegal at that stage Dezyne will point this out as a interface incompliancy. Note that marking behaviour as illegal is a requirement or design decision, in the example above the ProtocolStack could also be such that it is allowed to send a disable when the component is not yet enabled.

3) To unambiguously define all possible behaviour, an interface must specify all replies that are possible. Definition of all possible replies is described in way that is abstract from implementation details. What you see specified in the OFF state when the enable event is received is an example of how this is done in the Dezyne Modeling language. What is described here is that as a result of the enable event two things can happen: a reply plus a state transition in case enabling is successful and a reply when enabling fails. In Dezyne this is referred to as a non deterministic choice. With this definition it is clear that for a user of this interface that it should be able to deal with both replies at this stage.

In the interface above, there is no definition yet the connectionReq and especially how the connectReqRes will be returned in case processing of the connection request is ready. How to specify this is outlined next.