Enabling Online Fault Prediction in Adaptive Control: A Model Checker and Controller Co-Designed CPS Solution

By combining cyber subsystem of model checker with physical subsystem of control, online model checking of control systems can serve as a runtime fault prediction method to increase control systems safety. Online model checking of adaptive control systems, however, incurs more challenging time costs, due to the uncertainty caused by unknown control system parameter values. In this paper, we first propose a safety-oriented adaptive controller (SOAC) to replace the classic adaptive controller. This cuts online model checking time cost from <tex xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">$\Omega(Jd^{n+p-1})$</tex> to <tex xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">$O(Jd^{n-1})$</tex>, where <tex xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">$J$</tex> and <tex xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">$d$</tex> are scalable configuration parameters, raising which refines numerical computation granularity; <tex xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">$n$</tex> is the dimension of the physical state; and <tex xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">$p+1$</tex> is the dimension of control system parameters with unknown values. We further propose a specialized model checker for SOAC, and prove under mild conditions, the proposed model checker can further cut model checking time cost to <tex xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">$O(J)$</tex>.