Identification of missing properties in model checking
US7120568B1 · kind B1 · utility
6Cited by
2References
32Claims
0Family size
Assignee
Inventors
Key dates
| Filing date | Jun 27, 2000 |
| Grant date | Oct 10, 2006 |
| Priority date | — |
| Expiry date | Aug 11, 2023 |
Classification
- Technology area (CPC G)Physics
- CPC primaryG06F30/3323
- WIPO fieldComputer technology
- WIPO sectorElectrical engineering
Abstract
A method for verification includes providing an implementation model, which defines model states of a target system and model transitions between the model states, and providing a specification of the target system, including properties that the system is expected to obey. A tableau is created from the specification, the tableau defining tableau states with tableau transitions between the tableau states in accordance with the properties. The tableau transitions are compared to the model transitions to determine whether a discrepancy exists therebetween.
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.