Efficient production of disjoint multiple traces
US7146301B2 · kind B2 · utility
Assignee
Inventors
Key dates
| Filing date | Jan 11, 2002 |
| Grant date | Dec 5, 2006 |
| Priority date | — |
| Expiry date | Jun 4, 2024 |
Classification
- Technology area (CPC G)Physics
- CPC primaryG06F30/3323
- WIPO fieldComputer technology
- WIPO sectorElectrical engineering
Abstract
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.
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.