International Business Machines Corporation

Shoham Ben-David

Anna Gringauze

Eli Dichterman

Leonid Gluhovsky

Ilan Beer

Yaron Wolfsthal

Yossi Malka

Leonid Glukhovsky

A method for checking a model includes specifying a path to be traversed through the states of a system under study, such that a specified sequence of events is to occur on the specified path between an initial state and a target set of states on the path. Beginning from the initial state, successive reachable sets of states along the specified path are computed, such that in the successive reachable sets the events occur in the specified sequence. When an intersection is not found to exist between one of the reachable sets on the specified path and the target set, a partial trace is produced along the specified path between the initial state and a termination state in which at least one of the specified events occurs.

Generation of partial traces in model checking

A method for checking a model, which defines states of a system under study and a transition relation among the states. The method includes specifying a property that applies to a target set that comprises at least one target state among the states of the system under study. Beginning from an initial set of at least one initial state among the states of the system, successive reachable sets are computed, including the states of the system that are reachable from the initial set, until an intersection is found between one of the reachable sets and the target set. A plurality of mutually-disjoint traces are then computed from the at least one target state in the intersection through the states in the reachable sets to the at least one initial state.

Efficient production of disjoint multiple traces

A method for exploring the behavior of a design model, the method including the steps of providing a design model represented as a Finite State Machine (FSM). The method further includes the step of providing a path specification of interest. The method further includes the step of exploring the behavior of the design in order to find and present a scenario in the design that meets the path specification.

Target design model behavior explorer

A method for checking a model includes computing a succession of sets of the states of the system, beginning with an initial set of one or more initial states, such that the states in each of the sets are reachable by a successive cycle of a transition relation of the system from the states in a preceding set. One or more of the sets in the succession are selected to be saved in a memory, while the sets not selected are discarded. When an intersection is found between one of the sets in the succession and a target set, a trace is computed from one of the target states in the intersection through the states in the sets in the succession, including the discarded sets, to one of the initial states, using the sets saved in the memory to reconstruct the discarded sets.

Growing community of inventors

Haifa, Israel

Shoham Ben-David