Modeling non-deterministic priority queues for efficient model checking
US7990980B2 · kind B2 · utility
Assignee
Inventors
Key dates
| Filing date | Dec 27, 2007 |
| Grant date | Aug 2, 2011 |
| Priority date | — |
| Expiry date | Oct 3, 2028 |
Classification
- Technology area (CPC H)Electricity
- CPC primaryH04L49/9036
- WIPO fieldDigital communication
- WIPO sectorElectrical engineering
Abstract
A method and system are disclosed for modeling non-deterministic queues for efficient model checking. In this method and system, a multitude of messages are held in a plurality of queues, and these messages having n priorities. The method comprises the steps of providing (n+1) queues, including a first queue, and n priority queues; passing said messages from a source to the first queue; passing each of said messages from the first queue to one of said n priority queues based on the priority of the message; and passing each of said messages from the n priority queues to a destination based on the priority of the message. One or more non-deterministic waits are introduced into one or more of the passing steps to simplify passing the messages into or out of the n priority queues.
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.