Model checking with layered localization reduction
US6957404B2 · kind B2 · utility
12Cited by
4References
40Claims
0Family size
Assignee
Inventors
Key dates
| Filing date | Dec 20, 2002 |
| Grant date | Oct 18, 2005 |
| Priority date | — |
| Expiry date | Jun 12, 2023 |
Classification
- Technology area (CPC G)Physics
- CPC primaryG06F30/3323
- WIPO fieldComputer technology
- WIPO sectorElectrical engineering
Abstract
A method for verifying a property of a complete model of a system under study includes abstracting at least some of the variables from the model so as to produce an abstract model of the system. Beginning with an initial state in a state space of the abstract model, an abstract path is found through the state space of the abstract model in accordance with the transition relation to a target state defined by the property. A subset of the abstracted variables is restored to the abstract model so as to produce an intermediate model of the system, and the property on the complete model is verified based on the intermediate model.
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.