Intertwined global optimization based reachability analysis

Abstract

This paper proposes a semi-formal reachability analysis technique based on global optimization for hybrid systems. In order to model the hybrid system dynamics with parameter and noise disturbance, a system of stochastic recurrence equations formalism is proposed. Then, a reachability analysis approach is adopted to compute the reachable sets under an interval of initial conditions and in light of system parameters variability. The novelty of our approach is in approximating the reachable bounds in an intertwined forward/backward manner. The backward corrections refine the obtained reachable bounds in the forward scheme and so reduce the high reachability over-bounding due to the wrapping effect. Finally, a Monte Carlo hypothesis testing based technique is performed on the resultant reachable bounds to uncover the hybrid system failure with regard to a certain specification. These failures are quantified in terms of parametric yield rate which reflects the sensitivity of the hybrid system to variations in its parameters. We demonstrate the effectiveness of our proposed verification methodology by applying it on a mixed analog and digital electronics building block commonly used in communications systems.