Data processing: structural design – modeling – simulation – and em – Simulating electronic device or electrical system – Event-driven
Reexamination Certificate
1996-12-09
2001-01-23
Teska, Kevin J. (Department: 2763)
Data processing: structural design, modeling, simulation, and em
Simulating electronic device or electrical system
Event-driven
C703S022000, C714S039000
Reexamination Certificate
active
06178394
ABSTRACT:
TECHNICAL FIELD
This invention relates to the verification of communication protocols used in concurrent systems.
BACKGROUND OF THE INVENTION
Prior art verification of protocols used in concurrent systems required a model, such as a finite state machine or an extended finite state machine, to be developed for each communicating element in the concurrent system. The verification of the protocol between the various communicating elements was then performed on the model. However, verification could not be performed using the actual code, for example C code or C++ code, which implemented the element and described entirely its behavior when the element was actually operating. This is disadvantageous because a) it is time consuming to develop the model and b) the verification is only as good as the accuracy of the model.
SUMMARY OF THE INVENTION
In accordance with the principles of the invention, the verification of the protocol between the various communicating elements of a concurrent system may be performed directly using the actual code that implements the element when it is actually operating. This is achieved by combining stateless search techniques with partial order methods, namely, persistent set and sleep set methods. In particular, the code of each element of a system is exercised by a scheduler in such a way that global states of the system are visited according to a stateless search, which is a search that does not use an explicit representation of the global states. A global state is a state in which the next operation to be executed by every element of the system is a visible operation. The set of visible operations includes at least those operations related to communication between the elements. The global states are visited using an intelligent state space exploration technique so that only a selected subset of all the global states are visited while ensuring that those global states that are not visited need not be visited to verify the existence or absence of selected problems that might exist in the protocol. Such selected properties can include the existence of 1) deadlocks, 2) assertion violations, 3) divergences, and 4) livelocks. Advantageously, complex protocols in systems having many elements may be efficiently verified, while using prior art comprehensive search techniques could not verify even a simplistic toy protocol within a reasonable amount of time.
REFERENCES:
patent: 4754400 (1988-06-01), Wakahara et al.
patent: 5163016 (1992-11-01), Har'El et al.
patent: 5615137 (1997-03-01), Holzmann et al.
patent: 5768498 (1998-06-01), Boigelot et al.
Godefroid, P. et al., “A Partial Approach to Model Checking,” Proc. of 6th Annual IEEE Symp. on Logic in Computer Science, Jul. 1991, pp. 406-415.
Partial-Order Methods for the Verification of Concurrent Systems—An Approach to the State-Explosion Problem, vol. 1032 of Lecture Notes in Computer Science, Springer-Verlag (Jan. 1996).
Using Partial Orders to Improve Automatic Verification Methods, published in Proc. 2nd Workshop on Computer Aided Verification, vol. 531 of Lecture Notes in Computer Science, p. 176-185, Rutgers, Springer-Verlag (Jun. 1990).
Using Partial Orders for the Efficient Verification of Deadlock Freedom and Safety Properties, published in Formal Methods in System Design, 2(2):149-164 (Apr. 1993).
Choi Kyle J.
Lucent Technologies - Inc.
Rosenthal Eugene J.
Teska Kevin J.
LandOfFree
Protocol checking for concurrent systems does not yet have a rating. At this time, there are no reviews or comments for this patent.
If you have personal experience with Protocol checking for concurrent systems, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Protocol checking for concurrent systems will most certainly appreciate the feedback.
Profile ID: LFUS-PAI-O-2443601