Patent Document ID: 8977533
Application ID: 13023900
Patent Flag: 1

Claim One:
1. A system for checking statuses of states in a Statemate Model using bounded model checking (BMC), the system comprises: an input means for receiving an Original Statemate Model (OSM), and a processor coupled to the input means, wherein the processor is capable of executing certain programmed instructions to: transform the OSM into a First Stalemate Model (FSM), wherein the FSM comprises a set of initial FSM configurations, and wherein the set of initial FSM configurations is a super set of all stable OSM configurations; determine a maximum length of a biggest super step among the set of initial FSM configurations, wherein the maximum length is indicative of a maximum number of steps possible between any two successive stable reachable OSM configurations; transform the OSM into a Second Statemate Model (SSM) based on the maximum length of the biggest super step by initializing a) all internal events of the OSM to false, and b) rest of the variables of the OSM to non-deterministic values, wherein the SSM comprises a set of initial SSM configurations, and wherein the set of initial SSM configurations is a superset of all the stable OSM configurations; identify unreachable states of the OSM by analyzing only the set of initial configurations of the SSM by using a bounded model checker (BMC) with a bound as the maximum length of the biggest super step, wherein each of the initial super steps in the SSM are analyzed, without analyzing additional configurations of the SSM beyond the initial configuration; and send information associated with the un-reachable states to an output means.