Counter-Example Guided Abstraction Refinement Based Test Case Generation From Simulink/Stateflow Models

A method for verifying reachability of a transition path between states with respect to Simulink/Stateflow® models, the method comprising the steps of:

• (a) generating a concrete simulation model as a transition system by a processor;
• (b) generating an abstract model by the processor;
• (c) generating an abstract path by the processor that is a sequence of transition steps from a start state to a target state;
• (d) checking a validity of the abstract path by the processor utilizing the concrete simulation model;
• (e) outputting a result to a user by an output device that identifies the abstract path as a reachable result;
• otherwise proceeding to step (f);
• (f) partitioning a respective state of the transition step that was invalid in the abstract path by the processor;
• (g) recomputing a next abstract model by the processor based on partitioned start state in step (f);
• (h) generating an next abstract path by the processor;
• (i) determining whether the next abstract path is valid in the concrete model by the processor;
• (j) outputting a result to the user by the output device that identifies whether the recomputed abstract path is a valid result for testing the concrete model in a vehicle system;
• otherwise proceeding to step (f).