Patent ID: 9098620
Filing Date: 2015-08-04
Classification: G06F

Abstract:
1. A method for verifying a system comprising: receiving a state space graph modeling a finite state space of the system, each node of the state space graph corresponding to a state of the system, and each edge of the graph corresponding to a transition between a pair of nodes; generating an abstract graph abstractly representing the state space graph from the state space graph; performing a parallel reachability analysis directly on the state space graph by traversing the finite state space graph as received in parallel using a structured duplicate detection technique based on the abstract graph; determining invalid behaviors or states of the system based on the performing of the parallel reachability analysis using the structured duplicate detection technique; and proving the correctness of the system if no invalid behaviors or states are found, wherein the state space graph models a plurality of processes, each represented by a finite-state automaton, wherein each state in the state space graph includes a current state for each of the plurality of processes and transitions for the current state, wherein the generating includes, for each state of the state space graph, mapping the state to an abstract state of the abstract graph, the abstract state including the one or more current states of the state corresponding to a subset of the plurality of processes, and wherein the transitions are used to determine predecessor and successor relations and only automata of processes of the subset are used to generate the abstract graph.