Abstract
The main problem being faced in finite-state model checking is the state space explosion problem. For coping with it, many advanced methods for reducing state spaces have been proposed. One of the most successful methods (especially when dealing with software systems) is the so-called partial-order reduction. In the paper, we examine how this method can be used in the context of object-oriented Petri nets, which bring in features like dynamic instantiation, late binding, garbage collection, etc.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Brat, G., Havelund, K., Park, S., Visser, W.: Java PathFinder – A Second Generation of a Java Model Checker. In: Workshop on Advances in Verification (2000)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. The MIT Press, Cambridge (2000)
Češka, M., Janoušek, V., Vojnar, T.: PNtalk – A Computerized Tool for Object- Oriented Petri Nets Modelling. In: Moreno-Díaz, R., Pichler, F. (eds.) EUROCAST 1997. LNCS, vol. 1333. Springer, Heidelberg (1997)
Češka, M., Janoušek, V., Vojnar, T.: Generating and Using State Spaces of Object-Oriented Petri Nets. International Journal of Computer Systems Science and Engineering 16(3), 183–193 (2001)
Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems – An Approach to the State-Explosion Problem. PhD thesis, University of Liege, Computer Science Department (1994)
Holzmann, G.J., Peled, D.: An Improvement in Formal Verification. In: Proc. of 7th FORTE International Conference on Formal Description Techniques, IFIP Conference Proceedings. Chapman & Hall, Boca Raton (1994)
Holzmann, G.J., Peled, D., Yannakakis, M.: On Nested Depth First Search. In: Proc. of the 2nd Spin Workshop. American Mathematical Society (1996)
Janoušek, V.: Modelling Objects by Petri Nets. PhD. thesis, Brno University of Technology, Brno, CZ (1998)
Kristensen, L.M., Valmari, A.: Finding Stubborn Sets of Coloured Petri Nets Without Unfolding. In: Desel, J., Silva, M. (eds.) ICATPN 1998. LNCS, vol. 1420, p. 104. Springer, Heidelberg (1998)
Lluch-Lafuente, A., Edelkamp, L., Leue, S.: Partial Order Reduction in Directed Model Checking. Technical report (2001)
Valmari, A.: The State Explosion Problem. In: Reisig, W., Rozenberg, G. (eds.) APN 1998. LNCS, vol. 1491. Springer, Heidelberg (1998)
Vojnar, T.: Towards Formal Analysis and Verification over State Spaces of Object- Oriented Petri Nets. PhD. thesis, Brno University of Technology, Brno, CZ (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Češka, M., Haša, L., Vojnar, T. (2003). Partial-Order Reduction in Model Checking Object-Oriented Petri Nets. In: Moreno-Díaz, R., Pichler, F. (eds) Computer Aided Systems Theory - EUROCAST 2003. EUROCAST 2003. Lecture Notes in Computer Science, vol 2809. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45210-2_25
Download citation
DOI: https://doi.org/10.1007/978-3-540-45210-2_25
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-20221-9
Online ISBN: 978-3-540-45210-2
eBook Packages: Springer Book Archive