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

• Main Authors: Meng Li, Ratnesh Kumar
• Format: Article
• Language: English
• Published: Wiley 2017-03-01
• Series: IET Cyber-Physical Systems
• Subjects: reachability analysis; discrete systems; automation; program testing; control engineering computing; automata theory; reachability resolution; discrete-time hybrid systems; automated test generation; Simulink/Stateflow; commercial model-based development tool; hybrid automaton refinement; edge representation; defect-detection; requirements-satisfaction; bounded counter; cyberphysical system; thermal control unit
• Online Access: https://digital-library.theiet.org/content/journals/10.1049/iet-cps.2017.0007

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.