Verification and validation of control algorithms by coupling of interpreted Petri nets

Interpreted Petri nets (IPN) are an extension of the basic Petri net (PN) framework. They are ordinary PN with additional components to model the information flow to and from the PN. This contribution gives a general overview of the control design process. Furthermore, it shows how the different tasks in this process, especially analysis, verification and validation, can be successfully solved within the formal IPN framework.