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 foreign 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.