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

@inproceedings{ClarkeModelCheckingInTheLoopACC08, abstract = {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.}, author = {Lerda, F. and Kapinski, J. and Maka, H. and Clarke, E. M. and Krogh, B. H.}, citeulike-article-id = {5936690}, citeulike-linkout-0 = {http://dx.doi.org/10.1109/ACC.2008.4586906}, citeulike-linkout-1 = {http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=4586906}, day = {05}, doi = {10.1109/ACC.2008.4586906}, journal = {American Control Conference, 2008}, keywords = {control, cps, model\_checking, vav}, month = {August}, pages = {2734--2740}, posted-at = {2009-10-13 15:27:00}, priority = {2}, title = {Model checking in-the-loop: Finding counterexamples by systematic simulation}, url = {http://dx.doi.org/10.1109/ACC.2008.4586906}, year = {2008} }

TY - CONF ID - ClarkeModelCheckingInTheLoopACC08 L3 - citeulike-article-id:5936690 N2 - 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. JF - American Control Conference, 2008 EP - 2740 TI - Model checking in-the-loop: Finding counterexamples by systematic simulation SP - 2734 KW - control KW - cps KW - model_checking KW - vav AU - Lerda, F AU - Kapinski, J AU - Maka, H AU - Clarke, EM AU - Krogh, BH PY - 2008/08/05/ UR - http://dx.doi.org/10.1109/ACC.2008.4586906 ER -