Model checking in-the-loop: Finding counterexamples by systematic simulation

Model checkers for program verification have enjoyed considerable success in recent years. In the control systems domain, however, they suffer from an inability to account for the physical environment. For control systems, simulation is the most widely used approach for validating system designs. We present a new technique for finding counterexamples that uses a software model checker to perform a systematic simulation of the software implementation of a controller coupled with a continuous plant. Instead of performing a large set of independent simulations, our approach uses the model checking notion of state-space exploration by piecing together numerical simulations of the plant and transitions of the controller. Our implementation of this technique uses an explicit-state source-code model checker to analyze the software and the MATLAB/Simulink environment to model and simulate the plant. We present an illustrative example involving a supervisory controller for an unmanned aerial vehicle (UAV). We show that our technique is able to detect an error in the controller design.