Patent Document ID: 20120203534
Application ID: 13023900
Patent Flag: 0

Claim One:
1. 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: a) transform the OSM into First Statemate Model (FSM) such that the set of initial configurations of the FSM is a super set of the set of all stable configurations of the OSM; b) determine maximum length of the super step of the FSM; c) 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; d) check the reachability of states, or any other such property, of the OSM in the SSM by using bounded model checker (BMC); and e) send the result to the output means.