Model checking, model verification and debugging are the three methods to improve the correctness of a model or to find out potential errors in it.
Model checking checks the correctness of a model by means of formal property proving. This checking does not depend on individual experiments. The properties, such as reachable states and acceptable event lists, are always true for the model. Model verification checks the correctness of a model by means of multiple simulations. The common properties of those simulations are summarized and are regarded as properties of the model. For example, the states that are not entered in all those simulations are considered unreachable states of the model. However, this conclusion may not be correct because of the non-exhaustive sampling of all possible behaviors. In fact, to achieve 100% certainty for a single property, an infinite number of simulations are usually required. Those simulations exhaust all possible traces of the model simulation. This is, of course, impossible. As a result, model verification is less formal than model checking. Debugging is the least formal in this comparison, since it is responsible for only one simulation or one group of simulations. When an error occurs in a simulation, the debugger usually looks inside the faulty part of the model to locate the error. When a design error is discovered, the debugger tries to fix it without affecting the other parts. However, this is usually impossible, and the result of this modification becomes unpredictable.
This chapter mainly discusses model verification, as it is the most well-studied approach. Our paper on consistency checking [40] contains a general discussion and an example of model verification with SVM. Formal model checking of DCharts is interesting and useful for many applications. It will be studied in the future. Debugging of DCharts models in the SVM simulator has been discussed in the previous chapter.