Patent ID: 7990980
Filing Date: 2011-08-02
Classification: H04L

Abstract:
1. A method of modeling non-deterministic queues for efficient model checking, wherein a multitude of messages are held in a plurality of queues, said messages having n priorities, the method comprising the steps of: providing (n+1) queues, including a first queue, and n priority queues; passing, by a processor, 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; passing each of said messages from the n priority queues to a destination based on the priority of the message; and introducing one or more non-deterministic waits into one or more of the passing steps in a manner simplifying passing the messages into or out of the n priority queues, the one or more non-deterministic waits allowing passing of lower priority messages that are in the n priority queues at a given time, passing being from said n priority queues to the destination before an incoming higher priority message enters said n priority queues and allowing passing of said incoming higher priority message once in the n priority queues, said passing of said incoming higher priority message being to the destination before certain lower priority messages are passed to the destination, the certain lower priority messages being ones that were passed to the n priority queues after the given time but prior to the n priority queues receiving said incoming higher priority message.