The following animation demonstrates the power of exhaustive verification to ensure the quality of the  software used in a complex embedded system.

The control panel of the embedded system has a number of buttons . Each has a small light indicator showing whether the button is enabled, i.e. pressing it will have some effect. The operator is guided by marking the enabled buttons as green  , otherwise they are red . The left and right side of the control panel are used to control two different parts of the application. Each part will from time to time enter a critical state indicated by the long (green) bar  at the top becoming red. The system can still operate as long as only one part is in the critical state, however, it must never happen that both parts enter the critical state simultaneously.

You should imagine that you are testing the embedded system. Below is an interactive version of the software which you can operate by clicking the buttons with the mouse. Try to see if you can find a sequence of steps that will make both parts  enter their critical state indicated by the two bars becoming red simultaneously. WARNING, this is not easy.

The next diagram illustrates testing by simulation. The inputs (pushing enabled buttons) are supplied automatically. In this example, there are only 2-4 possible inputs at any point of the computation, so the next input is chosen randomly. You may watch this simulation for as long as you wish. Should it enter a critical state for both parts, the simulation will stop.

After having tried the interactive version yourself and watching the simulation for a long time you might conclude that this is a working design, where it is not possible to enter the critical state for both parts simultaneously.

But there is an error, so it possible to push enabled buttons in such a sequence that the design will enter a state where both bars are red simultaneously. Try to go back to the interactive version and see if you can find it.

Any success? Maybe you did not try hard enough?

If you do not believe that such a sequence exists take a look at the third version and try clicking the mouse anywhere in the diagram.
 

This illustrates a computation where both bars are red simultaneously, so the software does have an error that is very hard to find by simulation or interactive debugging. However, model checking tools such as those described on the home page of this project will find the sequence  leading to the error in a matter of seconds. Please contact us if you want to know more.