Open AccessReachability resolution for discrete‐time hybrid systems with application to automated test generation for Simulink/Stateflow
Author(s) -
Li Meng,
Kumar Ratnesh
Publication year - 2017
Publication title -
iet cyber‐physical systems: theory and applications
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.308
H-Index - 7
ISSN - 2398-3396
DOI - 10.1049/iet-cps.2017.0007
Subject(s) - stateflow , reachability , computer science , hybrid automaton , automaton , timed automaton , test case , computation , code generation , model checking , algorithm , theoretical computer science , programming language , regression analysis , computer security , machine learning , key (lock) , matlab
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.