Demo Use Case 2 Examples

  1. Home
  2. Use case 2
  3. Demo Use Case 2 Examples

Use case 2 (Philips / Verum / TNO-ESI / Unit040)

Interventional application - examples

 

The examples below demonstrate the different language features developed in the Vivaldy context according to the process depicted here:

 

Figure 1

 

You can find a simplified example specification for Use Case 2 below the system under test, i.e., the composition of SmartCT, the Azurion and the Patient Database depicted here:

 

Figure 2

 


//actors
interface UI
{
  in void startup();
  in void scan();
  in void shutdown();
  out void ready();
  out void error();

  behavior
  {
    enum State {Idle, Ready, Error};
    State s = State.Idle;
    [s.Idle] {
      on startup: {s = State.Error; error;}
      on startup: {s = State.Ready; ready;}
    }
    [s.Ready] {
      on scan: ready;
      on scan: {s = State.Error; error;}
    }
    [!s.Idle] on shutdown: s = State.Idle;
  }
}

interface icontrol
{
  in void expose();
  out void image();
  out void error();

  behavior
  {
    on expose: image;
    on expose: error;
  }
}

interface ipatient
{
  in void connect();
  in void disconnect();
  in bool lookup();
  behavior
  {
    bool connected = false;
    [!connected] on connect: connected = true;
    [connected] on disconnect: connected = false;
    on lookup: reply(true);
    on lookup: reply(false);
  }
}

//functional specification of smartct and azurion interaction
module specification
{
  provides UI ui;
  requires icontrol azurion;

  behavior
  {
    on ui.startup(): ui.error();
    on ui.startup(): ui.ready();
    on ui.scan(): azurion.expose();
    on azurion.image(): ui.ready();
    on azurion.error(): ui.error();
    on ui.shutdown(): {}
  }
}

 

Below are two example scenarios extracted from the functional specification above:

 

Figure 3

 

 

Figure 4

 

All scenarios relevant according to the change impact analysis are verified on the implementation of the system, i.e., running code, by means of Dezyne Model Based Testing using the IO-LTS below generated from the module specification:

 

Figure 5

 

A stitched LTS of a compliant example implementation in Dezyne including patient database access.

 

Figure 6

 

The stitched LTS extracted from the system model below: 


component /*example*/ implementation
{
  provides UI ui;
  system
  {
    ui <=> smartct_.ui;
    smartct smartct_;
    azurion azurion_;
    database database_;
    smartct_.patient <=> database_.patient;
    smartct_.control <=> azurion_.control;
  }
}

component smartct
{
  provides UI ui;
  requires icontrol control;
  requires ipatient patient;

  behavior
  {
    on ui.startup(): {patient.connect(); if(patient.lookup()) ui.ready(); else ui.error();}
    on ui.scan(): control.expose();
    on control.image(): ui.ready();
    on control.error(): ui.error();
    on ui.shutdown(): if(patient.connected) patient.disconnect();
  }
}

component database
{
  provides ipatient patient;
}

component azurion
{
  provides icontrol control;
}