Reachability resolution for discrete-time hybrid systems with application to automated test generation for Simulink/Stateflow

摘要

Simulink/Stateflow is a popular commercial model-based development tool for many industrial domains. For safety and security concerns, verification and testing must be performed on the Simulink/Stateflow designs and the generated code. The authors present a test generation approach for Simulink/Stateflow by its reduction to reachability in a hybrid automaton, with its locations representing the computations of the Simulink/Stateflow model, and edges representing the computation-succession. A novel reachability resolution method is presented based on the refinement of the hybrid automaton such that the reachability is reduced to the reachability in the underlying graph (without the dynamics), whenever the refinement step terminates. The approach yields a technique that is effective in terms of achieving test coverage and efficient in terms of test generation time whenever the computation of each time step can be analytically solved for an arbitrary number of repetition. The approach is also applied on defect-detection and requirements-satisfaction, and illustrated through application to a bounded counter and a cyberphysical system of a thermal control unit.