We’re here to help you

Menu

Introduction

Key concepts: components, interfaces, events

When a software system is built, it is good practice to split it up (decompose) in parts that have high cohesion and low coupling. High cohesion means that the system part performs a dedicated task or responsibility. Low coupling means that the system parts are able to perform their responsibility without much interaction with other parts, system parts thus have simple interfaces to interact with each other. As an illustration, below a picture of a system with four parts where the loader loads raw input into a machine, the processor transforms the raw input into the final product and the output part moves the product out of the machine and the complete process is controlled by the controller.

                       [Controller]
                            |
        ---------------------------------------------
        |                   |                       |
      [Loader]          [Processor]               [Output]

Software development using Dezyne is component based, meaning that the system parts are components

  • A component implements a certain functionality.

  • A component implementation may use the functionality offered by other components.

  • The functionality that is offered by a component to others is defined in the components interface.

  • The functionality of a component can be used by sending and receiving events to and from the component over the interface, which is similar to calling one or more methods on the component interface.

To illustrate this, in the interaction diagram below the component called "Application" requests the component "ProtocolStack" to activate itself, by sending the enable event to the "ProtocolStack" component. The ProtocolStack responds synchronously with a "reply", either a void reply or a value returned as result of the enable.

 [Application]    [ProtocolStack]
     |                     |
     |        enable       |
     |-------------------->|
     |       "reply"       |
     |<- - - - - - - - - - |

Events have a direction. The direction is determined as seen from the component providing the service. For the ProtocolStack component in this example the enable event is an in event.

Synchronous and asynchronous communication

Between components there are two fundamental type of interactions: 1)synchronous and 2) asynchronous. The example above depicts a synchronous action, after sending the event enable to the ProtocolStack, the Application execution will be blocked until the "reply" (either a void reply or a value returned as result) is received. When the ProtocolStack is activated, it can be requested to setup a connection by sending the event "connectReq" to it. After giving a "reply" on this event the ProtocolStack component will start setting up a connection and the two components continue to run concurrently, i.e. are able to perform other tasks while the connection request is being processed by the ProtocolStack component. Once the request is completed the ProtocolStack will send a notification connectReqRes to the Application. This illustrates an asynchronous action.

   [Application]     [ProtocolStack]
        |                     |
        |     connectReq      |
        |-------------------->|
        |      "reply"        |
        |<- - - - - - - - - - |
        |                     |
        |                     |
        |                     |
        |    connectReqRes    |
        |<--------------------|
        |      "reply"        |
        |- - - - - - - - - - >|

Remember that events have a direction. For the ProtocolStack component in this example the connectReqRes event is an out event. The Application, however, receives this event as an in event that has a void return or some other return type (currently Dezyne only supports void out events).

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 Modelling 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.

Modelling events not visible to the outside world but leading to external visible behaviour

The following is crucial for understanding how to develop models in Dezyne. As mentioned, components use or provide functionality via interfaces and not by interacting directly with other components. Therefore, interface specifications can not contain component implementation details. However, when this leads to externally visible behaviour, interfaces necessarily capture decisions that are internal to the implementation. As an example consider in the case above the completion of the connection request that will trigger the server component to return a notification connectReqRes. But how is that captured in an interface specification that should not contain implementation details? There are two options to specify internal events (like the completion of the request initiated by connectReq), that lead to external events in interfaces:

  • by using on inevitable; meaning that when nothing else happens and the system is not triggered externally, the event will eventually always occur. For example a timeout event of a timer will eventually always take place if the timer is not cancelled by the client.

  • by using on optional; meaning that it may or may not occur. For example, an error message may not be generated when the system is working properly.

With this knowledge the interface specification for the ProtocolStack in the example we have been using so-far 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
  in void connectReq();
  out void connectReqRes();

  behaviour                                 // the specification of the externally visible behaviour
  {
    enum State {OFF, ON, CONNECTING, CONNECTED};
    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,connectReq: illegal;
    }
    [state.ON]
    {
      on enable: illegal;
      on disable: state = State.OFF;
      on connectReq: state = State.CONNECTING;
    }
    [state.CONNECTING]
    {
      on enable, connectReq: illegal;
      on disable: state = State.OFF;
      on inevitable:                   // inevitably the connectReq request will be done and a response will be given
      {
        state = State.CONNECTED;
        connectReqRes;
      }
    }
    [state.CONNECTED]
    {
      on enable, connectReq: illegal;
      on disable: state = State.OFF;
    }
  }
}

Dezyne modelling language versus programming languages

The Dezyne modelling language syntax closely resembles C, C++ and Java, making it easy to work with in terms of data types, scope, and so forth. But you must keep in mind always that the Dezyne Modelling language is truly a modelling language, not a language that directly compiles at the same level of abstraction as C/C++/Java, even though it looks and feels like these familiar languages. Instead, verified Dezyne models ultimately generate real C/C++/Java source code, which in turn goes through standard C/C++/Java compilers or interpreters to become actual machine-executable code. Models are compiled by Dezyne into formal language which is then model checked (formally verified) by checking every possible path through the communication and state structures of the modelled system, seeking problems such as interface incompliancies, deadlocks, live-locks, race conditions and unhandled events. Each path has steps like "component A presents information x via interface I to component B, and component B responds through interface I, perhaps now or perhaps later (or perhaps never), with information y intended for A, then A presents y or some transformation of y via interface J to component C, …” Sequences matter, but timing does not matter except for the problem case of “never returns”. Dezyne will either find no problems, or it will find one and tell you, the model developer, the exact sequence of communications and actions that leads to the problem. From this viewpoint, Dezyne and its modelling language are both a specification tool and an exploration tool. You do not need to concern yourself up front about, say, infinite loops or deadlocks; just design what seem to be correct interfaces and component states, and then verify the model. Dezyne will tell you if your conceptual model has a flaw. You might be surprised by what Dezyne tells you. In fact, the power of Dezyne is precisely here: Dezyne uncovers complex, subtle, hard-to-find bugs in your communications and behaviour logic – before you write or generate even one line of C, C++ or Java!

How to use the language help topics

The language help topics are setup in such a way that they provide support on how to use the Dezyne Modelling Language (DML) constructs. For each topic there is a general intent, followed by the syntax and examples. The topics can be read in any order, however, there is a certain sequence that can guide you in setting up your first DML models: First it is outlined how an interface and events should be constructed, next how a component is constructed and how to specify that a component provides or requires an interface. Then you can find how to define variables and how to specify interface and component behaviour with all the possible constructs (functions, conditionals, etc). Finally it is shown how you can decompose components into others / group components into systems.

If you have questions that weren’t answered by this Guide,
let our support team help you out.

Enjoy this article? Don't forget to share.