Model checking of liveness property in a phase abstracted model
US8627273B2 · kind B2 · utility
Assignee
Inventors
Key dates
| Filing date | Jul 22, 2009 |
| Grant date | Jan 7, 2014 |
| Priority date | — |
| Expiry date | Mar 26, 2032 |
Classification
- Technology area (CPC G)Physics
- CPC primaryG06F30/3323
- WIPO fieldComputer technology
- WIPO sectorElectrical engineering
Abstract
Phase abstraction may be utilized to increase efficiency of model checking techniques. A liveness property may be checked in respect to a phase abstracted model by modifying the liveness property in accordance with the phase abstracted model. A fairness property may be modified to ensure that the fairness property is held by the model checker. A counter-example produced by a model checker is modified to be in accordance to an original model. The counter-example comprises a repetitive behavior. The counter-example may be modified to shorten the repetitive behavior or to apply the repetitive behavior in an earlier cycle of the counter-example.
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.