Verification allows the user to formally check if a given specification is satisifed.

By verification, we mean the process of ascertaining whether a system fulfils a given specification or not. When verifying we do not (usually) distinguish between (a model of) the controlled process and (a model of) the controller. Rather, the closed-loop system is taken as a whole and questions such as "can this happen?" are asked. Hopefully, the verification tool answers "no" (assuming it is an undesired property), but in the cases that the answer is "yes", typically some indication of what causes the problem is given. Naturally, this information can be used to change the closed-loop system (that is, the controller) so that the undesired behavior is avoided. From a control engineering perspective, this seems a backward way of working, though. Since we generate the controller from the specification and the process model, using a procedure that is mathematically proven to give a correct result, we know that none of the non-specified behavior will be exhibited. The specification is guaranteed not to be broken. Obviously, this holds only if the process model and specification is correct, which may seem as an argument in favor of verification. However, the same problem turns up there. It is the models that are verified, not reality. If the verification models are incorrect, then no guarantees can be given about the real system.

One verification aspect that may be useful even from a control engineering perspective is the verification of the specification. Given the specification we assume that it specifies the entire desired and allowed behavior. However, mistakes may have been made. Asking and answering questions about the specification can thus be very useful.

It should be noted that synthesis is generally a more complex problem than verification, especially considering the specification. For synthesis, the entire desired and allowed behavior must be expressed, whereas separate characteristics can often be verified separately. It is very hard to give a complete specification, particularly for a system under development.

Traditionally, verification has treated timing aspects, which lie outside the logical correctness that our synthesis guarantees. This is very important, in particular for time critical (embedded) systems, a very important class of systems where formal methods are practically imperative. For logical systems, timing aspects can be treated separately and will always restrict the logically correct solution.

An area close to verification is simulation. When simulating, the models are exposed to different types of inputs and disturbances and their outputs are (computer) generated. The simulation models can often be made more complex and thus closer to reality than the models used for synthesis. Thus, simulation can reveal "incorrectness" in the controller (say) due to the synthesis model not capturing enough of the relevant details. Note though that simulation can never prove the absence of errors, only the presence