| 摘要 |
The present invention provides a system and method for detecting unreachable states in a large commercial Statemate Statechart model. A system for checking the reachability of any given state in a Statemate Model, the said system comprises: an input means for receiving an Original Statemate Model (OSM), output means for displaying the result to a user, and a processor, wherein the processor is capable of executing the programmed instructions to: transform the OSM into First Statemate Model (FSM) by using translator; transform the OSM into Second Statemate Model (SSM) based on the determined length of the super step such that the set of all initial configurations of the SSM is a superset of all the stable configurations of the OSM by using translator; check the reachability of states of the OSM in the SSM by using bounded model checker (BMC); and send the result to the output means.
|
