@ARTICLE{ iet:/content/journals/10.1049/iet-cps.2017.0007, author = {Meng Li}, affiliation = { Department of Electrical and Computer Engineering, Iowa State University, Ames, IA 50010, USA }, author = {Ratnesh Kumar}, affiliation = { Department of Electrical and Computer Engineering, Iowa State University, Ames, IA 50010, USA }, keywords = {commercial model-based development tool;requirements-satisfaction;reachability resolution;thermal control unit;hybrid automaton refinement;edge representation;discrete-time hybrid systems;cyberphysical system;automated test generation;bounded counter;Simulink/Stateflow;defect-detection;}, language = {English}, abstract = {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.}, title = {Reachability resolution for discrete-time hybrid systems with application to automated test generation for Simulink/Stateflow}, journal = {IET Cyber-Physical Systems: Theory & Applications}, issue = {1}, volume = {2}, year = {2017}, month = {April}, pages = {28-41(13)}, publisher ={Institution of Engineering and Technology}, copyright = {This is an open access article published by the IET under the Creative Commons Attribution-NonCommercial-NoDerivs License (http://creativecommons.org/licenses/by-nc-nd/3.0/)}, url = {https://digital-library.theiet.org/;jsessionid=1bnc1k7tudl5j.x-iet-live-01content/journals/10.1049/iet-cps.2017.0007} }