Constructing verification models of nonlinear Simulink systems via syntactic hybridization

In this paper, we present a methodology that facilitates the integration of formal verification techniques into model-based design. The focus is on set-based reachability analysis and on control systems that are described by hybrid dynamics and nonlinear components. Starting with a standard simulation model, e.g. in MATLAB/Simulink, we transform it into an equivalent verification model, formally a network of hybrid automata. This verification model complies with the SX format, which is a formalism used by several reachability tools. A major obstacle encountered is that highly scalable reachability algorithms and tools exist for piecewise affine (PWA) dynamical models, but not for nonlinear ones. To obtain PWA over-approximations of nonlinear dynamics, we use an abstraction method known as hybridization. Hybridization consists in partitioning the state-space into a set of domains and for each domain approximating the nonlinear dynamics by simpler ones. Nondeterministic inputs are added to account for the abstraction error. Existing hybridization procedures operate on the composed (flattened) system, so the number of partitions is exponential in the number of variables. This quickly leads to intractably large models, even for small systems. To mitigate this problem, we decompose the original dynamics and carry out the state-space partitioning and PWA approximation on the components. The number of partitions in each PWA component is at most quadratic in the abstraction error, thus largely avoiding an explosion in the number of partitions. Since the SX format can handle templates, several components may share the same abstraction. The result is a highly compact model that retains the modular structure of the original simulation model. If only a small subset of the partitions is reachable, the bottleneck of having excessively large PWA models can be avoided by composing the model on-the-fly during the reachability analysis.