Model checking refers to proving properties of the models without simulation or execution. For example, by enumerating all possible event sequences accepted by a state machine, the dead states (the states that the model never goes to) are discovered and deleted. Another example is by building a reachability graph of a PetriNet model, it can be easily proved whether or not the model allows deadlock (a state of which the model, once enters it, can never go out).
Model checking of DCharts is not easy, mostly because models in DCharts contain too much information about the execution detail. Usually, a model has to be abstracted and the irrelevant information in it must be removed before checking can be performed. This could be done by means of transforming the model into model(s) of other formalisms, such as DEVS and PetriNets. Because of its difficulty, model checking is not discussed in this thesis.
Another approach to find out properties of models and demonstrate their correctness is model verification. It is done by simulating or executing the models multiple times. A tool that analyzes the gathered output trace tells whether the models are running correctly or not. It may also analyze the performance of the models and discover possible bottle-necks in them.