We’re here to help you

Menu

Armouring patterns

Here we discuss the exhaustive list of Armour patterns separated in armouring either a provides interface or a requires interface. They all come in 2 flavours, with or without error handling. The names were inspired by the error messages that the Dezyne verifier generates.

In Provides interface

  • ArmourIIPRV (IllegalInProvidesReturnsVoid): In-event not allowed by port → an in-event with void return value is defined as illegal in the interface

  • ArmourIIPRB (IllegalInProvidesReturnsBool): In-event not allowed by port → an in-event with bool return value is defined as illegal in the interface

  • ArmourIIPRE (IllegalInProvidesReturnsEnum): In-event not allowed by port → an in-event with enum return value is defined as illegal in the interface (very similar to bool case)

In Requires interface

  • ArmourOENABP (OutEventNotAllowedByPort): Out-event not allowed → context should not generate an asynchronous out-event via requires interface

  • ArmourISOE (IllegalSynchronousOutEvent): Illegal event → context should not generate a synchronous out-event via requires interface

  • ArmourMSOE (MissingSynchronousOutEvent): Missing event → context is expected to generate a synchronous out-event via requires interface

  • ArmourMAOE (MissingAsynchronousOutEvent): Missing event → after a timeout period the armour can supplement the missing asynchronous out-event

  • ArmourREIR (RangeErrorInRequiresReply): Reply value not allowed by port → the reply of a requires interface event could have a range error (a mis-mapping between two subints)

  • ArmourIBVIRR (Illegal Boolean value in Requires reply): Reply value not allowed by port → a reply value from a required interface can contain a boolean value that is not allowed

Might be expected but not possible Armour cases

Due to the semantics of the Dezyne Modeling Language some situations are syntactically or semantically impossible

  • Range error in function parameter in/out-event ⇒ events cannot have control parameters

  • Missing in-event ⇒ occurrence of an in-event cannot be enforced

  • Reply value conflicts in out-events ⇒ out-events can only return void

Individual Armour cases

We will now discuss all possible armour cases individually but only in the simplistic variant where the error is logged and subsequently ignored. The complex variant, with the error handling procedure, is also available in Dezyne code but not discussed in this tutorial.

ArmourIBVIRR (IllegalBooleanValueInRequiresReply)

A reply value from a required interface can contain a boolean value that is not allowed. The system diagram shows the armour at the requires port of the Dezyne component:

ArmourIBVIRR

We only deal with one in-event returning a boolean result value. The Strict interface specifies that only a boolean value of 'true' can be replied.

interface IStrict
{
  in bool ia();

  behaviour
  {
    on ia: reply (true);
  }
}

The Robust interface allows both boolean reply values of 'true' and 'false'.

interface IRobust
{
  in bool ia();

  behaviour
  {
    on ia: reply (true);
    on ia: reply (false);
  }
}

In the armour the result from the requires interface is captured in a local bool b. If it is false we log it as an error. In all cases we simply return the boolean value 'true' to the provides interface.

component ArmourIBVIRR // IStrict to IRobust
{
  provides IStrict pStrict;
  requires IRobust rRobust;
  requires injected ILogger iLog;

  behaviour {
    on pStrict.ia(): {
    	bool b = rRobust.ia();
    	if (!b) iLog.Log($"Reply value false from ia not allowed by port"$);
    	reply(true);
    } // armour ignore (false) case
  }
}

The full armour example code including the client and overall system component is here:

Basic example: ArmourIBVIRR

Example with error handling: ArmourIBVIRRError

ArmourIIPRB (IllegalInProvidesReturnsBool)

A provided interface may have an illegal in-event with a bool return type. The system diagram shows the armour at the provides port of the Dezyne component:

ArmourIIPRB

We only deal with one bool in-event and one void out-event. The Strict interface specifies that the in-event is illegal.

interface IStrict
{
  in bool ia();
  out void oa();

  behaviour
  {
    on ia: illegal;
    on inevitable: oa;
  }
}

The Robust interface allows both an in-event and an out-event'. In the case of the in-event it always replies 'false'.

interface IRobust
{
  in bool ia();
  out void oa();

  behaviour
  {
    on ia: {reply(false);}
    on inevitable: oa;
  }
}

In the armour the occurrance of an illegal in-event is logged and 'false' is replied. An out-event from the requires port is simply passed to the provides port.

component ArmourIIPRB // IStrict to IRobust
{
  provides IRobust pRobust;
  requires IStrict rStrict;
  requires injected ILogger iLog;

  behaviour {
    on pRobust.ia(): {reply(false); iLog.Log($"In-event ia is illegal in port"$);} // armour illegal ia
    on rStrict.oa(): pRobust.oa();
  }
}

The full armour example code including the client and overall system component is here:

Basic example: ArmourIIPRB

Example with error handling: ArmourIIPRBError

ArmourIIPRE (IllegalInProvidesReturnsEnum)

A provided interface may have an illegal in-event with a myEnum return type. The system diagram shows the armour at the provides port of the Dezyne component:

ArmourIIPRE

We only deal with one in-event returning an enumerated and one void out-event. The Strict interface specifies that the in-event is illegal.

interface IStrict
{
  in myEnum ia();
  out void oa();

  behaviour
  {
    on ia: illegal;
    on inevitable: oa;
  }
}

The Robust interface allows both an in-event and an out-event'. In the case of the in-event it always replies 'No'.

interface IRobust
{
  in myEnum ia();
  out void oa();

  behaviour
  {
    on ia: {reply(myEnum.No);}
    on inevitable: oa;
  }
}

In the armour the occurrance of an illegal in-event is logged and 'No' is replied. An out-event from the requires port is simply passed to the provides port.

component ArmourIIPRE // IStrict to IRobust
{
  provides IRobust pRobust;
  requires IStrict rStrict;
  requires injected ILogger iLog;

  behaviour {
    on pRobust.ia(): {reply(myEnum.No); iLog.Log($"In-event ia is illegal in port"$);} // armour illegal ia
    on rStrict.oa(): pRobust.oa();
  }
}

The full armour example code including the client and overall system component is here:

Basic example: ArmourIIPRE

Example with error handling: ArmourIIPREError

ArmourIIPRV (IllegalInProvidesReturnsVoid)

A provided interface may have an illegal in-event with a void return type. The system diagram shows the armour at the provides port of the Dezyne component:

ArmourIIPRV

We only deal with one void in-event and one void out-event. The Strict interface specifies that the in-event is illegal.

interface IStrict
{
  in void ia();
  out void oa();

  behaviour
  {
    on ia: illegal;
    on inevitable: oa;
  }
}

The Robust interface allows both an in-event and an out-event'. In the case of the in-event there is no associated action.

interface IRobust
{
  in void ia();
  out void oa();

  behaviour
  {
    on ia: {}
    on inevitable: oa;
  }
}

In the armour the occurrance of an illegal in-event is logged. An out-event from the requires port is simply passed to the provides port.

component ArmourIIPRV // IStrict to IRobust
{
  provides IRobust pRobust;
  requires IStrict rStrict;
  requires injected ILogger iLog;

  behaviour {
    on pRobust.ia(): {iLog.Log($"Input event ia is illegal in port"$);} // armour illegal ia
    on rStrict.oa(): pRobust.oa();
  }
}

The full armour example code including the client and overall system component is here:

Basic example: ArmourIIPRV

Example with error handling: ArmourIIPRVError

ArmourISOE (IllegalSynchronousOutEvent)

The context is expected to not generate a synchronous out-event via the requires port but may still do that. The system diagram shows the armour at the requires port of the Dezyne component:

ArmourISOE

We only deal with one void in-event and one void out-event. The Strict interface specifies that the in-event does not lead to a synchronous out-event.

interface IStrict
{
  in void ia();
  out void oa();

  behaviour
  {
    on ia: {}
    on inevitable: oa;
  }
}

The Robust interface allows that in-event either results in a synchronous out-event or no out-event at all.

interface IRobust
{
  in void ia();
  out void oa();

  behaviour
  {
    on ia: {}
    on ia: oa;
    on inevitable: oa;
  }
}

In the armour we use the async keyword to discriminate between out-events that are triggered by an out-event from a requires port from a synchronous out-event. On the receival of an in-event we set a bool and put a request in the async queue. If the async acknowledge triggers and we have not had an out-event from the requires port in between we know the behaviour is according to the strict interface. If we receive an out-event from the requires port in the context of the provides in-event (we know by inspecting the boolean value) then we know it is an error and we deal with it. Otherwise we pass the out-event as normal allowed behaviour.

component ArmourISOE {
	provides IStrict pStrict;
	requires IRobust rRobust;
	requires injected ILogger iLog;

	behaviour {
		requires dzn.async p;

		bool requested = false;
		on pStrict.ia(): {
			rRobust.ia();
			if (!requested) {p.req(); requested = true;}
		}
		on rRobust.oa(): {
			if (!requested) pStrict.oa();
			else {
				requested = false; p.clr();
				iLog.Log($"Native comp does sync out-event oa where async oa was expected"$);
			}
		}
		on p.ack(): requested = false;
    }
}

The full armour example code including the client and overall system component is here:

Basic example: ArmourISOE

Example with error handling: ArmourISOEError

ArmourMAOE (MissingAsynchronousOutEvent)

The native component is expected to generate an out-event asynchronously via the requires port but may not do that. The system diagram shows the armour at the requires port of the Dezyne component:

ArmourMAOE

We only deal with one void in-event and one void out-event. The Strict interface specifies that an in-event must lead to an asynchronous out-event. As a consequence a next in-event is only allowed after such an asynchronous out-event has happened.

interface IStrict
{
  in void ia();
  out void oa();

  behaviour
  {
  	bool ia_called = false;

    [!ia_called] on ia: {ia_called = true;}
    [ia_called] {
    	on ia: illegal;
    	on inevitable: {oa; ia_called = false;}
    }
  }
}

The Robust interface allows any occurrance of in-events and asynchronous out-events. We do allow to use multiple in-events without asynchronous out-events in between but the Dezyne component on top (the armour) will not issue multiple in-events.

interface IRobust
{
  in void ia();
  out void oa();

  behaviour
  {
    on ia: {}
    on optional: oa;
  }
}

In the strict sense we can never determine that an out-event is not coming anymore but a practical solution is to use a timeout period. After an in-event we start waiting for the asynchronous out-event from the requires port but we only wait for a given timeout period. If the timeout occurs we consider it an error; we log it and generate the missing out-event. If the out-event occurs within the deadline we pass it on and reset the armour top wait for a next in-event.

component ArmourMAOE {
	provides IStrict pStrict;
	requires IRobust rRobust;
	requires ITimer it;
	requires injected ILogger iLog;

	behaviour {
		bool waiting_for_oa = false;

		on it.timeout(): {
			iLog.Log($"timeout on expected oa"$);
			pStrict.oa(); waiting_for_oa = false;
		}
		[waiting_for_oa]
			on rRobust.oa(): {pStrict.oa(); it.cancel(); waiting_for_oa = false;}
		[!waiting_for_oa]{
			on pStrict.ia(): {rRobust.ia(); it.start(); waiting_for_oa = true;}
			on rRobust.oa(): {}
		}
    }
}

The full armour example code including the client and overall system component is here:

Basic example: ArmourMAOE

Example with error handling: ArmourMAOEError

ArmourMSOE (MissingSynchronousOutEvent)

The context is expected to generate out-event via requires interface but may not do that. The system diagram shows the armour at the requires port of the Dezyne component:

ArmourMSOE

We only deal with one void in-event and one void out-event. The Strict interface specifies that an in-event must lead to a synchronous out-event.

interface IStrict
{
  in void ia();
  out void oa();

  behaviour
  {
    on ia: oa;
  }
}

The Robust interface allows that an in-event either or not sends a synchronous out-event.

interface IRobust
{
  in void ia();
  out void oa();

  behaviour
  {
    on ia: oa;
    on ia: {}
  }
}

In the armour we use a combination of async and blocking. We need blocking to make sure all the lower level handling can be done semi-asynchronously and still we can reply in a synchronous way. The in-event is passed to the requires port and we raise an async request. If the async ackowledges we know all the processing in the context of the original in-event has completed and hence the required synchronous out-event is missing; we log the error, and create such an out-event in the armour. If the requires port receives an out-event this is happening in the context of the the original in-event (since the async acknowledge did not fire yet). Hence this is a synchronous reply and everything is fine. We cancel the async to avoid the error trigger.

component ArmourMSOE {
	provides IStrict pStrict;
	requires IRobust rRobust;
	requires injected ILogger iLog;

	behaviour {
		requires dzn.async p;
		bool xxxx = false;

		on pStrict.ia(): blocking {rRobust.ia(); p.req();}
		on rRobust.oa(): {pStrict.reply(); pStrict.oa(); p.clr();}
		on p.ack(): {pStrict.reply(); pStrict.oa(); iLog.Log($"Native comp does not send sync out-event oa"$);}
    }
}

The full armour example code including the client and overall system component is here:

Basic example: ArmourMSOE

Example with error handling: ArmourMSOEError

ArmourOENABP (OutEventNotAllowedByPort)

The required interface is not allowed to send an out-event but may still do that. The system diagram shows the armour at the requires port of the Dezyne component:

ArmourOENABP

We only deal with one void in-event and one void out-event. The Strict interface specifies that an in-event must not lead to any out-event.

interface IStrict
{
  in void ia();
  out void oa(); // nb not part of completeness check

  behaviour
  {
    on ia: {}
  }
}

The Robust interface allows optional out-events.

interface IRobust
{
  in void ia();
  out void oa();

  behaviour
  {
    on ia: {}
    on optional: oa;
  }
}

In the armour an in-event at the provides port is passed to the requires port. If an out-event is received from the requires port it is logged as an error and suppressed.

component ArmourOENABP // IStrict to IRobust
{
  provides IStrict pStrict;
  requires IRobust rRobust;
  requires injected ILogger iLog;

  behaviour {
    on pStrict.ia(): rRobust.ia();
    on rRobust.oa(): {iLog.Log($"Out-event oa is not allowed by port"$);} // armour potential oa
  }
}

The full armour example code including the client and overall system component is here:

Basic example: ArmourOENABP

Example with error handling: ArmourOENABPError

ArmourREIR (RangeErrorInRequiresReply)

The reply of a requires interface event could have a range error (a mis-mapping between two subints). The system diagram shows the armour at the requires port of the Dezyne component:

ArmourREIR

We only deal with one in-event areturning an integer value. We defined 2 integer ranges. The Strict interface use the most restricted one so we only allow a very limited set of reply values.

interface IStrict
{
  in SubCount ia();

  behaviour
  {
  	SubCount c=0;
    on ia: reply(0);
    on ia: reply(1);
    on ia: reply(2);
  }
}

The Robust interface allows the more relaxed set of reply values. In the model code we do not have to describe all possible reply values as long as we at least define one good case and one bad case that the verifer can investigate.

interface IRobust
{
  in AllCount ia();

  behaviour
  {
    on ia: reply (-1);	// -1 triggers an error
    on ia: reply (0);	// 0 is ok behaviour
  }
}

In the armour an in-event at the provides port is passed to the requires port. If the reply value from the requires port is outside the strict range it is logged as an error and either the lower or upper boundary of the restricted range is returned.

component ArmourREIR // IStrict to IRobust
{
  provides IStrict pStrict;
  requires IRobust rRobust;
  requires injected ILogger iLog;

  behaviour {
	AllCount c = 0;

    on pStrict.ia(): {
    	c = rRobust.ia();
    	if (c<0) {
    		iLog.Log($"Reply value from ia outside range (too small)"$);
    		reply(0);
    	}
    	else if (c>2) {
    		iLog.Log($"Reply value from ia outside range (too large)"$);
    		reply (2);
    	}
    	else reply(c+0);
    } // armour on boundary values
  }
}

The full armour example code including the client and overall system component is here:

Basic example: ArmourREIR

Example with error handling: ArmourREIRError

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.