Modeling a matrix for formal verification
US8489367B2 · kind B2 · utility
1Cited by
3References
14Claims
0Family size
Assignee
Inventors
Key dates
| Filing date | Sep 30, 2009 |
| Grant date | Jul 16, 2013 |
| Priority date | — |
| Expiry date | Mar 23, 2032 |
Classification
- Technology area (CPC G)Physics
- CPC primaryG06F11/3608
- WIPO fieldComputer technology
- WIPO sectorElectrical engineering
Abstract
A reference model may be defined to refer to a matrix of a target computerized system. The reference model may comprise a reference index and a reference matrix. The reference index may have a non-deterministic value enabling the reference matrix to refer to the matrix using a fewer number of cells. The disclosed subject matter may enable a more efficient model checking process of a computerized device by using a reference model that is relatively easy to define or maintain or by using a reference model that is configured to be more efficient for model checking as it uses non-determinism.
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.