Intended audience and prerequisites
As this tutorial will build upon the basic features of Dezyne, it is assumed that you are familiar with the Dezyne syntax and the use of Dezyne verification and simulation tools. It is helpful if you have some knowledge on the Dezyne runtime, which can be found in the previous tutorial.
This tutorial will consist of two parts: first we will disclose some information on how simulation and verification by Dezyne works and what the effects are of using ‘external’. The second part of the tutorial will focus on designing a solution for the problems that can be found with ‘external’.
The nature of ‘external’ requires you to be able to think in terms of threads and sequencing of events across multiple threads. You will be assisted in this during the tutorial, but it helps if you are familiar with the concepts.
This tutorial will build further upon the Alarm System models and native implementation from the previous tutorials. With ‘external’, we will be able to discover interesting real-world behavior in the Alarm System that can lead to illegality in its components.