Armoring (Dezyne Reference Manual)

7.3 Armoring

A common programming adagium is to be liberal what you accept and strict in what you deliver. Verification clearly depends on the accuracy with which the behavior of the environment is described by its interface specifications. Any inconsistency with reality may lead the execution of the code into unverified territory. To avoid this we can apply an approach called armoring. An armor is a defensive layer of components that protects the armored components who rely on their interface contracts from any behavior which would violate those contracts. An armoring component can be developed in Dezyne itself by creating a permissive interface from the strict interface behavior and letting the armor component map one behavior onto the other making sure the permissive behavior never violates the strict behavior.

Consider this simple strict interface

interface istrict
{
  in void request ();
  in void cancel ();
  out void notify ();

  behavior
  {
    bool idle = true;
    [idle] on request: idle = false;
    [!idle]
    {
      on cancel: idle = true;
      on inevitable: {idle = true; notify;}
    }
  }
}

used by this simple proxy component

import istrict.dzn;

/*
component proxy // a proxy pre 2.17.0
{
  provides istrict p;
  requires istrict r;

  behavior
  {
    bool idle = true;
    [idle] on p.request (): {r.request (); idle = false;}
    [!idle]
    {
      on p.cancel (): {r.cancel (); idle = true;}
      on r.notify (): {p.notify (); idle = true;}
    }
  }
}
*/

component proxy // a trivial proxy post 2.17.0
{
  provides istrict p;
  requires istrict r;

  behavior
  {
    on p.request (): r.request ();
    on p.cancel (): r.cancel ();
    on r.notify (): p.notify ();
  }
}

Because the istrict interface is stateful, a problem occurs when the enviroment would erroneously issue a second p.request event before receiving an r.notify.

Now consider this permissive interface

interface ipermissive // derives from istrict
{
  in void request ();
  in void cancel ();
  out void notify ();

  behavior
  {
    on request: {}
    on cancel: {}
    on optional: notify;
  }
}

that shares its event alphabet with istrict. Being permissive means that it will accept any of the events, regardless of the history.

Using the ipermissive interface we can derive a simple top armor component

import istrict.dzn;
import ipermissive.dzn;

component top_armor
{
  provides ipermissive p;
  requires istrict r;

  behavior
  {
    bool idle = true;
    [idle]
    {
      on p.request (): {idle = false; r.request ();}
      on p.cancel (): {}
    }
    [!idle]
    {
      on p.request (): {}
      on p.cancel (): {idle = true; r.cancel ();}
      on r.notify (): {idle = true; p.notify ();}
    }
  }
}

and likewise, a bottom_armor component

import istrict.dzn;
import ipermissive.dzn;
import iwatchdog.dzn;

component bottom_armor
{
  provides istrict p;
  requires ipermissive r;
  requires iwatchdog w;

  behavior
  {
    bool idle = true;
    [idle]
    {
      on p.request (): {idle = false; w.set (); r.request ();}
      on r.notify (): {}
    }
    [!idle]
    {
      on p.cancel (): {idle = true; w.cancel (); r.cancel ();}
      on r.notify (),
         w.timeout (): {idle = true; w.cancel (); p.notify ();}
    }
  }
}

The permissive interface is to be used on both sides of the armored_system. The system connects each permissive interface to a dedicated armor component, one for the top of the system and one for the bottom. Both protecting the inside component called proxy.

import proxy.dzn;
import top_armor.dzn;
import bottom_armor.dzn;

component watchdog
{
  provides iwatchdog w;
}

component armored_system // is permissive, but armored
{
  provides ipermissive p;
  requires ipermissive r;

  system
  {
    p <=> ta.p;
    top_armor ta;

    ta.r <=> m.p;
    proxy m; // the soft but strict middle
    m.r <=> ba.p;

    bottom_armor ba;
    watchdog w;
    ba.w <=> w.w;
    ba.r <=> r;
  }
}