Static partial order reduction

Details Static partial order reduction Static partial order reduction

1998-10-14

2001-09-25

Teska, Kevin J. (Department: 2123)

Data processing: structural design, modeling, simulation, and em

Simulating electronic device or electrical system

C703S002000

Reexamination Certificate

active

06295515

ABSTRACT:

BACKGROUND
This invention relates to system specification reduction methods.
One common method for dealing with the intrinsically intractable computational complexity of model-checking asynchronous systems is partial order reduction. This reduction technique exploits the common practice of modeling concurrent events in asynchronous systems as an interleaving of the events in all possible execution orders. An important observation about such systems is that often the properties one needs to check do not distinguish among these different orders. The reduction algorithm produces a state graph which contains only a subset of the states and transitions of the original system, but which contains enough information about the modeled system so that it is possible to apply model-checking algorithms to it instead of the full state graph. The verified property is guaranteed to be true in the reduced model if and only if it is true in the original model.
Since partial order reduction is naturally defined for asynchronous systems, it has thus far been applied mainly to the verification of software. Traditional partial order reduction algorithms use an explicit state representation, and a depth-first search. In contrast, other techniques for model checking, most notably symbolic model checking based on binary decision diagrams (BDDs), have proved most effective for synchronous systems, in particular for verifying hardware.
Previous implementations of partial order reduction algorithms in pre-existing state space search engines required considerable changes in the search mechanism. See, for example, P. Godefroid and D. Pirottin, “Refining Dependencies Improves Partial Order Verification Methods,”
Proc.
5
th
Conference on Computer Aided Verification, vol.
697
of Lecture Notes in Computer Science,
pp. 438-449, Elounda, June 1993, Springer-Verlag, and G. J. Holzmann and D. Peled “An Improvement in Formal Verification,”
Formal Description Techniques
1994, pp. 197-211, Bern Switzerland, 1994, Chapman & Hall. The alternative was to construct a special tool for performing the search, for example, as described by A. Valmari in “A Stubborn Attack on State Explosion,”
Proc.
2
nd
Workshop on Computer Aided Verification, vol.
531
of Lecture notes in Computer Science,
pp. 156-165, Rutgers, June, 1009, Springer-Verlag. [14]. In the Holtzman and Peled article, a reduction that is based on doing a large part of the calculations at compile time is described. However, some changes are still made to the search engine, controlling the backtracking mechanism in the depth-first search performed in the SPIN model checker, which is described by G. J. Holzmann in
Design and Validation of Computer Protocols,
Prentice Hall, 1992.
D. Peled described a simplified “ample sets” search method in “Combining Partial Order Reductions With on-the-fly Model Checking,”
Formal Methods In System Design,
8:39-64, 1996. This approach basically contemplates translating the specification into an internal code and then verifying the code with a model-checking tool that includes partial order reduction. The ample sets are the sets of transitions of the reduced graph that still describes the system. Since the notions of “ample sets” are employed in the instant disclosure, this article is hereby incorporated by reference. Closely related to this article is U.S. Pat. No. 5,615,137, issued to Holzmann and Peled on Mar. 25, 1997, and it, too, is hereby incorporated by reference.
In this prior art approach, a generator for the reduced model is created by appending a set of rules to the generator of the original model which, at least in part, are applied in the course of the model checking.
It is an object of this invention to create a set of rules that are applied as a transformation of the original model, and completely independently of the model checking or verification.
It is another object of this invention to create a generator that statically produces a reduced state graph.
It is another object of this invention to create a process that efficiently verifies the design of systems that include both software and hardware, and is well adapted to symbolic model checking.
It is still another object of this invention to create a process that is independent of the type of search employed, and is applicable to a depth-first search approach or a breadth-first search approach without a change.
It is yet another object of this invention to create a process that is compatible with existing model checking tools without requiring a change to their search engines.
SUMMARY
These and other objects are achieved with a process that implements a static partial order reduction. Specifically, the process of this invention creates a modified state graph generator of a multi-process system that is checked by appending to the generator a number of rules that serve to substantially reduce the generated state graph. Moreover, the appended rules condition the generator to realize a substantially reduced state graph in a manner that allows any desired state searching tactic (breadth first, depth first, etc.) to be employed when states and transitions are considered in the course of verification. This permits use of existing model checking tools without needing to modify them. The static partial order reduction is made possible by realizing that a prior art condition that at least one state along each cycle of the reduced state graph must be fully expanded can be guaranteed by considering the individual processes that make up the system and identifying certain transitions in those processes.


REFERENCES:
patent: 5163016 (1992-11-01), Har'El et al.
patent: 5615137 (1997-03-01), Holzmann et al.
patent: 5740084 (1998-04-01), Hardin et al.
patent: 5901073 (1999-05-01), Kurshan et al.
Gerth et al.; “A partial order approach to branching time logic model checking”, IEEE Proc. Theory of Comp. & Systems; pp. 130-139, Jan. 1995.*
Saha et al.: A fast protocol conversion technique using reduction of state transition graphs; IEEE Conf. Comp. and Comm.; pp. 628-635, 1992.*
Clarke et al.; Computer aided verification; IEEE Spectrum; pp. 61-67, 1996.*
Macii et al.; Formal verification of digital systems by automatic reduction of data paths; IEEE Trans. CAD of IC; pp. 1136-1156, 1997.*
Peled, D, “Partial Order Reduction: Model Checking Using Representatives”, Mathematical Foundations of Computer Science 1996, 21st Int'l. Symposium, MFCS '96, Proceedings, Mathematical Foundations of Computer Science 1996, Cracow, Poland, Sep. 2-6, 1996.
Godefroid, P., et al., “Using Partial-Order Methods in the Formal Validation of Industrial Concurrent Programs”, IEEE Trans. on Software Engineering, vol. 22, No. 7, Jul. 1996.
Alur, R., et al. “Partial-Order Reduction in Symbolic State Space Exploration”, Computer Aided Verification., 9th Int'l Conf., CAV'97. Proceedings, Computer Aided Verification, 9th Int'l Conf., CAV'97. Proceedings, Haifa, Israel, Jun. 22-25, 1997.

Affiliated with

Also associated with

Rating

Static partial order reduction does not yet have a rating. At this time, there are no reviews or comments for this patent.

If you have personal experience with Static partial order reduction, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Static partial order reduction will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFUS-PAI-O-2490895