Patent Document ID: 20150154096
Application ID: 14093112
Patent Flag: 0

Claim One:
1. A method of verifying a system that can be described as a finite state transition system, said system comprising control logic for controlling manipulation of data, said method comprising the steps of: generating a model of said system, said model comprising an initial state function defining at least one initial state, a transition function defining how said system moves between consecutive states and a property function defining a property that should be met for an allowable state, said initial state function, transition function and property function each comprising at least one of data, operations and predicates; generating an abstracted model by approximating at least some of said data, operations and predicates with uninterpreted terms, uninterpreted functions and uninterpreted predicates respectively, to generate an abstracted initial state function defining at least one abstracted initial state, abstracted transition function and abstracted property function within said abstracted model; performing a reachability analysis on said abstracted model to determine whether when starting from said at least one abstracted initial state, said system can reach an unallowable abstracted state by following said abstracted transition function; and if said system cannot reach an unallowable abstracted state, said system is verified as correct; and if said system can reach an unallowable abstracted state, unabstracting a trace of said transitions from said at least one abstracted initial state to said unallowable abstracted state and determining using said model whether steps of said unabstracted trace are feasible; and if steps of said unabstracted trace are not feasible, refining said abstracted model to preclude any infeasible steps and repeating said reachability analysis on said refined abstracted model; and if steps of said unabstracted trace are feasible, generating an error.