Abstract
The state space explosion problem is central to automatic verification algorithms. One of the successful techniques to abate this problem is called ‘partial order reduction’. It is based on the observation that in many cases the specification of concurrent programs does not depend on the order in which concurrently executed events are interleaved. In this paper we present a new version of partial order reduction that allows all of the reduction to be set up at the time of compiling the system description. Normally, partial order reduction requires developing specialized verification algorithms, which in the course of a state space search, select a subset of the possible transitions from each reached global state. In our approach, the set of atomic transitions obtained from the system description after our special compilation, already generates a smaller number of choices from each state. Thus, rather than conducting a modified search of the state space generated by the original state transition relation, our approach involves an ordinary search of the reachable state space generated by a modified state transition relation. Among the advantages of this technique over other versions of the reduction is that it can be directly implemented using existing verification tools, as it requires no change of the verification engine: the entire reduction mechanism is set up at compile time. One major application is the use of this reduction technique together with symbolic model checking and localization reduction, obtaining a combined reduction. We discuss an implementation and experimental results for SDL programs translated into Cospan notation by applying our reduction techniques. This is part of a hardware-software co-verification project.
Chapter PDF
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
R. Alur, R.K. Brayton, T.A. Henzinger, S. Qadeer, and S.K. Rajamani. Partial order reduction in symbolic state space exploration. In Proceedings of the Conference on Computer Aided Verification (CAV'97), Haifa, Israel, June 1997.
E. Bounimova, V. Levin, O. Bagbugoglu, and K. Inan. A verification engine for SDL specification of communication protocols. In S. Bilgen, U. Çağlayan, and C. Ersoy, editors, Proceedings of the First Symposium on Computer Networks, pages 16–25, Istanbul, Turkey, May 1996.
C.T. Chou and D. Peled. Formal verification of a partial-order reduction technique for model checking. In Proceedings of the Second International Workshop on Tools and Algorithms for the Construction and Analysis of Systems, pages 241–257, Passau, Germany, 1996. Springer-Verlag. Volume 1055 of Lecture Notes in Computer Science.
D.L. Dill. Trace Theory for Automatic Hierarchical Verification of Speed-Independent Circuits. MIT Press, 1989.
D. Dolev, M. Klave, and M. Rodeh. An O(nlogn) unidirectional distributed algorithm for extrema finding in a circle. Journal of Algorithms, 3:245–260, 1982.
P. Godefroid and D. Pirottin. Refining dependencies improves partial-order verification methods. In Proc. 5th Conference on Computer Aided Verification, volume 697 of Lecture Notes in Computer Science, pages 438–449, Elounda, June 1993. Springer-Verlag.
R. H. Hardin, Z. Har'El, and R. P. Kurshan. COSPAN. In Proc. CAV'96, volume 1102, pages 423–427. LNCS, 1996.
G.J. Holzmann. Design and Validation of Computer Protocols. Prentice-Hall, 1992.
G.J. Holzmann and D. Peled. An improvement in formal verification. In Formal Description Techniques 1994, pages 197–211, Bern, Switzerland, 1994. Chapman&Hall.
R. Kurshan. Computer-Aided Verification of Coordinating Processes. Princeton University Press, 1994.
L. Lamport. What good is temporal logic. In IFIP Congress, pages 657–668. North Holland, 1983. in Computer Science 115.
D. Peled. Combining partial order reductions with on-the-fly model checking. Formal Methods in System Design, 8:39–64, 1996.
Functional Specification and Description Language (SDL), CCITT Blue Book, Recommendation 2.100. Geneva, 1992.
A. Valmari. A stubborn attack on state explosion. In Proc. 2nd Workshop on Computer Aided Verification, volume 531 of Lecture Notes in Computer Science, pages 156–165, Rutgers, June 1990. Springer-Verlag.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kurshan, R., Levin, V., Minea, M., Peled, D., Yenigün, H. (1998). Static partial order reduction. In: Steffen, B. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 1998. Lecture Notes in Computer Science, vol 1384. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0054182
Download citation
DOI: https://doi.org/10.1007/BFb0054182
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64356-2
Online ISBN: 978-3-540-69753-4
eBook Packages: Springer Book Archive