EFFICIENT PARTITION REFINEMENT BASED REACHABILITY CHECKING FOR SIMULINKS/STATEFLOW MODELS

摘要

A method for verifying reachability of a transition between states in a transition system using simulation modeling. Generating a concrete simulation model. Generating an abstract model having an abstract path that is a sequence of transition steps between a source state and a target state. Validity of the abstract path is checked. Identifying whether the abstract path is invalid in the concrete model. If invalid, then discarding the abstract path and generating a new abstract path. Re-checking a validity of each new abstract path. If abstract path is valid, then determining whether the abstract path is reachable from an initial condition. If reachable, then outputting the reachable transition to the user; otherwise, partitioning the source state into two additional state abstractions. Recomputing a refined abstract model retaining all transition paths except transitions that are determinative as invalid. Rechecking validity of an abstract path associated with the refined abstract model.