Simulation + Uncertainty = Model Checking

Methods based on numerical simulation are today intensively used for finding the correct values of input parameters of a numerical system. However, in presence of uncertainties or disturbances of the inputs, simulation methods cannot guarantee that the system always continue to behave satisfactorily. We present an alternative approach based on “model checking” that guarantees the robustness of the system in presence of uncertainty. We also explain how the model checking approach can be used to synthesise a feedback law in the case where one of the inputs is controllable.