In this section, 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?|
|• How does this translate to runtime execution?|
|• Why does verification not catch this?|
|• What does ‘external' do and when should you use it?|