This example outlines how the interaction between the Dezyne modelling tool (client, e.g. Eclipse plug-in) and the Verum server can be modelled using the Dezyne Modelling Language.

A number of language elements will be illustrated: how to define asynchronous communication, how to define synchronous communication using return values, and different ways to define behaviour, including how to define conditional behaviour that includes illegal or not allowed behaviour and how to ensure that a client of an interface can be kept in synch with the state of the interface.

Requirements

The main functions of the Dezyne server are:

  • Checking whether a model is semantically correct / well-formed

  • Verifying a model

  • Performing a simulation

  • Generating views based on a model (system-, state diagram, state table)

  • Generating code

These functions can be started from within the Dezyne Client. The Client is running locally on the computer of a user, the Dezyne Server is deployed in a hosted server environment (Cloud service) and available for all users.

For the sake of simplicity this example only takes into account checking and verifying a model.

Before a user can access the services provided by the Dezyne server, the client has to authenticate itself.

In this example we take the case that there is a set of floating licenses available that can be shared among a certain amount of users that belong to a company or department. When authentication is successful, the server will check if there is a license available. If there is a license (or seat) available, access is granted. In addition this example case is such that the client has to re-authenticate when it has been inactive for a certain time.

Step 1: Defining the system to be modelled

To model this case we define a server component responsible for interacting with the client and interacting with other server components that take care of dedicated functions like authentication, checking if a license is available, performing the model check and verification.

image

These are the main parts of the modelled system:

  • DezyneApplication, the main component, i.e. the server

  • IDezyne, the interface between the client and the server

  • IUserDB, the interface for authentication services

  • IAccountDB, the interface for license checking

  • IBackend, the interface to initiate model checks and model verification

  • ITimer, an interface to maintain the session duration

Step 2: modelling the IUserDB.

The main responsibility of the IUserDB interface is to authenticate users. Authentication can be initiated by sending the event “checkUser”. For this example we take the case that the component implementing this interface will start an authentication process and come back with an answer later (asynchronous communication) by responding either UserCredentialsOK, UserCredentialsNOK, UserUnknown. Another option would be to return the result immediately with a return parameter, how to do this will be explored in the the IAccountDB interface.

To model this interface protocol in Dezyne, a simple state machine can be used. Initially the interface is in Idle state and when a checkUser event is received it will jump to Checking state. In this state we define that another checkUser is not allowed (is illegal) and that depending on the specific authentication result either a UserCredentialsOK, UserCredentialsNOK or UserUnknown will be send to the client of this interface (in our case this is DezyneApplication). This will happen at a certain moment, completely determined by the implementation of the interface and to model this in a Dezyne interface that must be implementation independent, the keyword on inevitable is used.

image

Step 3: modelling the IAccountDB

The main responsibility of the IAccountDB interface is to check if there is a license available or if all licenses (seats) or occupied. The check is initiated by sending the checkIfSeatAvailable event.

For this interface we have made the choice to return immediately the result by using a return value. Therefore the first thing you note in the interface definition is the definition of the result type.

The actual behaviour is straightforward: there are two possibilities when the checkIfSeatAvailable is send over the interface, the client of this interface can expect either a seat is available or a seat is not available. This is what is defined in the behaviour section of the interface.

interface IAccountDB
{
/* Interface of the Authorisation Server responsible for user authorisation services.
 * This example models the case where licenses are shared within a group of users
 * and when a user starts a session it needs to be check if a license (=seat) is
 * available.
 */
  enum result // the result of the license check will be returned in a return value
  {
    Available,
    NotAvailable
  };
  in result checkIfSeatAvailable();

  behaviour
  {
    // below the two possible returns are defined.
    on checkIfSeatAvailable:
    {
      reply (result.Available);
    }
    on checkIfSeatAvailable:
    {
      reply (result.NotAvailable);
    }
  }
}

Step 4: defining the IBackend interface

The main responsibility of the IBackend interface is to handle the model check and model verification transactions. Model checking can be initiated by using checkModel and verification can be initiated by verifyModel. At a later moment the results will be (asynchronously) returned by the events checkModelRes and verifyModelRes.

The new complexity introduced in this interface is that we don’t allow to start a new transaction when there is already one ongoing. For this purpose the booleans ModelCheckOngoing and VerificationOngoing are used. For instance, where the event checkModel is received, it is declared with a guarded statement [!ModelCheckOngoing] that checkModel is allowed only when there is no model check already ongoing, otherwise it is declared as illegal behaviour.

IMPORTANT: Defining conditional behaviour that includes illegal behaviour MUST be done using declarative statements (using guards []). In the Dezyne Modelling Language, one could be tempted to specify this behaviour also with an (imperative) if-else statement, but even if this might look the same, it is not and Dezyne will not allow it.

interface IBackend
{
/* Interface of the Dezyne BackEnd Server responsible for all modelling related services:
 * - well-formedness checking
 * - generating views (state diagram, state table, system view)
 * - verification
 * - simulation
 * - code generation
 *
 * Only checking and verification of models is modelled in this example.
 */
  in void checkModel(); // perform a well-formedness check
  in void verifyModel(); // perform a verification
  out void checkModelRes(); // result of well-formedness check
  out void verifyModelRes(); // result of verification

  behaviour
  {
    bool ModelCheckOngoing = false; // boolean to keep track if model check is already ongoing
    bool VerificationOngoing = false; // boolean to keep track if verification is already ongoing

    on checkModel:
    {
      // indicate that a model check transaction is ongoing
      [!ModelCheckOngoing] ModelCheckOngoing = true;

      // starting another model check is not allowed when there is already one ongoing
      [otherwise] illegal;
    }
    on verifyModel:
    {
      // indicate that a verification transaction is ongoing
      [!VerificationOngoing]  VerificationOngoing = true;

      // starting another verification is not allowed when there is already one ongoing
      [otherwise]illegal;
    }
    on inevitable:
    {
      // eventually the server will return the result of the model check
      [ModelCheckOngoing]
      {
        ModelCheckOngoing = false;
        checkModelRes;
      }

      // eventually the server will return the result of the verification
      [VerificationOngoing]
      {
        VerificationOngoing = false;
        verifyModelRes;
      }
    }
  }
}

Step 5: defining the ITimer interface

The interface for the timer is straight-forward:

interface ITimer
{
  // interface for a basic timer
  in void createTimer(); // create a timer
  in void cancelTimer(); // cancel the timer
  out void timeout();

  behaviour
  {
    enum States { Idle, Busy };
    States state = States.Idle;

    [state.Idle]
    {
      on createTimer: state = States.Busy;
      on cancelTimer: {}
    }
    [state.Busy]
    {
      on cancelTimer: state = States.Idle;
      on createTimer: illegal;
      on inevitable:
      {
        timeout;
        state = States.Idle;
      }
    }
  }
}

Step 6: Defining the IDezyne interface

Now the interface between the Dezyne client and the Dezyne Server can be defined.

What is allowed over this interface is largely determined by the status of authentication. Therefore the main state machine is build around where the authentication process is. Initially a client is only allowed to authenticate. When the user is authorised, model check and verification can be started, but only when there is not already a similar transaction ongoing and only if the session is not expired. The final statement block defines the possible events the client can receive as results of previously initiated actions, in this case results of model check and verification or that a re-authentication is needed when the session is expired.

IMPORTANT: when an interface needs to change state, always ensure that that the client is informed (by sending an out event), otherwise the client will not have the same view on what the state of the interface is.

image

Step 7: defining the DezyneApplication component

Now that all interfaces are in place the component itself can be developed.

First statements are to import the interface definitions needed by the component.

The component follows the same flow / structure as the interface it provides, the IDezyne interface. In the Authenticating state it is checked that there is a license available and if so the session timer is started before jumping to the Authorized state. When the user is authorized, model check and verification can be started, but only when there is not already a similar transaction ongoing and only if the session is not expired.

image

Step 8: composing the system together

As a final step we define the system, where all elements are brought together. New in here are the binding statements used to bind ports of components. In this case the DezyneApplication is bound to its external ports of the system component DezyneSystem, see picture:

image

/* In this example the client - server communication between the Dezyne client (e.g.
 * Eclipse plugin) and the Dezyne Server is modelled.
 *
 * In this example authentication, authorisation and checking + verification of
 * models is modelled.
 */

import IDezyne.dzn; // the interface between Client and Server
import IBackend.dzn; // the interface between the Server and a backend that performs model checks and verification
import IUserDB.dzn; // the interface between the Server and a component / database holding user credentials
import IAccountDB.dzn; // the interface between the Server and a component / database with overview of licenses in use
import DezyneApplication.dzn; // the main Dezyne application, the Server
import ITimer.dzn; // the timer interface that is used to maintain the session duration.

component DezyneSystem
{
  provides IDezyne iDezyne;
  requires IBackend backend;
  requires IUserDB userDB;
  requires IAccountDB accountDB;
  requires ITimer timer;

  system
  {
    DezyneApplication dezyneApplication;

    dezyneApplication.iDezyne <=> iDezyne;
    dezyneApplication.ibackend <=> backend;
    dezyneApplication.userDB <=> userDB;
    dezyneApplication.accountDB <=> accountDB;
    dezyneApplication.timer <=> timer;
  }
}

Summary

In this example we have shown how interaction protocols can be modelled in the Dezyne Modelling Language. The models can be formally verified in Dezyne and when no errors are found during verification, code can be generated that is also fault free.

This example can be loaded in Dezyne: Select 'DezyneApplication' in the list you see when executing File → New → Dezyne Example Project.