In this chapter, we will discuss a scenario of the Alarm System’s behavior where a delay in communication between two components results in a race condition that ultimately leads to illegal behavior. With this in mind, we will examine the Dezyne verification process and why standard verification does not find the race condition we discovered.

With this information, you should be able to understand when to use ‘external’ and what problems it can solve, as well as the impact of using ‘external’ in your Dezyne models.

What can go wrong?

For the example in this chapter, a snapshot containing Dezyne models and C++ source code is available on Github.

Consider the following situation:



In the above sequence diagram, a valid password has been entered on the IController interface. his resulted in the Controller moving to the Armed state, turning on the Sensor as well.

At this point the Sensor was triggered, resulting in the starting of the Timer as well as the Controller transitioning to the Alarming state. The corresponding Watch window with this sequence of events is included to the right and it confirms that the Controller is in the Alarming state and that the Timer is Running.

Say we were to perform another passwordEntered event, with a valid password. The following sequence will occur:



So far so good, right? The Dezyne model encounters no illegal behavior and the Watch window tells us that the Controller has moved back to the Armed state, ITimer is Idle again and the Sensor is Sensing.

An important remark to make at this point is that the passwordEntered event from iController led to a series of events that took an arbitrary amount of time, x. This is important to keep in mind for the next paragraph.

How does this translate to runtime execution?

In order to fully understand what can happen, it’s important to replay the above scenario in real-world context where time does matter. Recall that the code generated from the System required a thread-safe-shell to guarantee the single-thread-active property of the application (see this article). This was done by using a dzn::pump to schedule events on a First In, First Out (FIFO) basis for a private thread to handle.

After the first valid passwordEntered event, the Controller is Armed. If Armed, the triggered event from the Sensor leads to the Controller starting the timer. Let’s call this point t = 0. The timer is configured to timeout after 30 seconds as specified in the behavior, so the timeout event will be scheduled by the native Timer thread at t = 30.

Earlier it was noted that the execution time of the second passwordEntered event is x. Say a valid password is entered just before t = 30. It is now a possibility that during the execution x, t = 30 occurs which results in a timeout event being scheduled. However, after x, the Controller is in the Armed state. If you look at the behavior of the Controller component in the Armed state, a timeout event cannot be handled and as such is implicitly illegal:

[state.Armed] {
  on iController.passwordEntered(pw): {
    bool valid = iPWManager.verifyPassword(pw);
    if(valid) {
      state = State.Unarmed;
  on iSensor.triggered(): {
    state = State.Alarming;

Why does verification not catch this?

So now that we have considered a sequence of events in context of runtime behavior, we have found a trace that leads to a race condition triggering illegal behavior. Why doesn’t Dezyne show us this illegal behavior? If you verify the Controller component, it passes every test just fine. If you simulate the Controller component, you will not be able to send a timeout event during the handling of the passwordEntered event.

The reason behind this is that Dezyne verification does not account for the time it takes to execute a sequence of events. During verification, it is assumed that the execution of events occurs instantaneously. If events occur instantaneously, there can be no concurrency of events- there is no timespan in which multiple processes are active. As such,there is no time period x in the verification during which the timeout event can be scheduled. We have found a discrepancy between the behavior verified by Dezyne and the behavior of the generated code in a real-world environment: concurrency.

The absence of concurrency in the verified scenario means that only synchronous traces of events are considered. However, the scenario we found relies on asynchronous behavior of one of the native components. This asynchronous behavior can only come from a component that runs on its own execution thread. Using the ‘external’ keyword, you can indicate that the implementing component is active outside of the Dezyne private thread and therefore, extra behaviors must be considered by the Dezyne verification and simulation tools.

What does ‘external’ do and when should you use it?

The ‘external’ keyword is a modifier for requires interfaces of a component. Marking an interface as ‘external’ will increase its set of possible event sequences in the verification and simulation tools of Dezyne. More specifically, indicating that a requires interface is ‘external’ tells Dezyne that it should account for delays that can occur in communication through the interface. If the interface is stateful, this means that the two components on either end of the interface can get out of sync regarding the state of the protocol they use to communicate.

In the example with ITimer in the previous chapter, the Controller considers the state of Timer is Running when the cancel event is sent. However, the Timer has already timed out and has queued the timeout event accordingly. This is a textbook example of two components, Controller and Timer, being out of sync in regard to their perceived state of the protocol they use to communicate (ITimer). The result is that an unsuspecting Controller still receives a timeout it must handle even though the Controller is under the assumption that the Timer had been canceled.

If you modify the ITimer port of the Controller to requires external ITimer iTimer; and verify the Controller, you will actually find the illegal assert:


So, when should you use ‘external’? Right now, it might seem tempting to make every required port that sends out events ‘external’. However, its usage is not always warranted and as such you might be doing a lot of work for no benefit at all. The general rule of thumb:

Mark as ‘external’ any requires interface containing out-events that is delegated to the boundary of a system. Take note that the ‘external’ marking must be done in a behavior component, not a system component.

If a requires interface with out-events is implemented in a Dezyne component contained in the same system, the scheduling of said out-events will be done on the private Dezyne thread during runtime. The semantics enforced by the included Dezyne runtime simply prevent the component from scheduling any out-events while another component is executing its behaviour. Therefore, no race conditions between state and asynchronous events within the generated Dezyne framework can exist.

For more information on the Dezyne runtime semantics, please refer to this article.

With proper inclusion of ‘external’ for components implemented outside of Dezyne, verification and simulation will once again consider the full scope of the possible behaviours of your application. As you saw in the previous sequence view, though, you have some work to do in the Controller component so that it can function correctly with an ‘external’ ITimer port. In the next chapter, we will explore some changes you can make to the implementation of a component to allow for ‘external’ behaviour.