Efficient partition refinement based reachability checking for simulinks/stateflow models

A method for verifying reachability of a transition between states with respect to design and simulation modeling, the method comprising the steps of:

• generating a concrete simulation model by a processor as a transition system;
• generating an abstract model by the processor having an abstract path that is a sequence of transition steps between a source state and a target state, the source state being an inverse of the target state;
• checking a validity of the abstract path by the processor utilizing the concrete simulation model;
• outputting a result to a user by an output device that identifies whether the abstract path is invalid in the concrete model;
• if invalid then;
• discarding the abstract path;
• generating a new abstract path by an output device;
• re-checking a validity of each new abstract path by the processor;
• if abstract path is valid in the concrete model, then determining whether the abstract path is reachable from an initial condition;
• if reachable from the initial condition, then outputting the result to the user identifying the reachable transition between the source state and the target state;
• otherwise, partitioning the source state into two additional state abstractions by the processor;
• recomputing a refined abstract model by the processor retaining all transition paths except transitions that are determinative as invalid, the refined abstract model including a sequence of non-discarded transition steps;
• rechecking validity of an abstract path associated with the refined abstract model using the concrete model;
• and
• 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.