Abstract
Partial order reduction limits the state explosion problem that arises in model checking by limiting the exploration of redundant interleavings. A state space search algorithm based on this principle may ignore some interleavings by delaying the execution of some actions provided that an equivalent interleaving is explored. However, if one does not choose postponed actions carefully, some of these may be infinitely delayed. This pathological situation is commonly referred to as the ignoring problem. The prevention of this phenomenon is not mandatory if one wants to verify if the system halts but it must be resolved for more elaborate properties like, for example, safety or liveness properties. We present in this work some solutions to this problem. In order to assess the quality of our propositions, we included them in our model checker Helena. We report the result of some experiments which show that our algorithms yield better reductions than state of the art algorithms like those implemented in the Spin tool.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Bao, T., Jones, M.: Time-efficient model checking with magnetic disk. In: Tools and Algorithms for the Construction and Analysis of Systems. LNCS, vol. 3440, pp. 526–540. Springer, Berlin (2005)
Basten, T., Bosnacki, D.: Enhancing partial-order reduction via process clustering. In: Automated Software Engineering, pp. 245–253. IEEE Computer Society, USA (2001)
Bosnacki, D., Holzmann G.J.: Improving spin’s partial-order reduction for breadth-first search. In: SPIN, Model Checking of Software. LNCS, vol. 3639, pp. 91–105. Springer, Berlin (2005)
Bosnacki D., Leue, S., Lluch-Lafuente, A.: Partial-order reduction for general state exploring algorithms. In: SPIN, Model Checking of Software. LNCS, vol. 3925, pp. 271–287. Springer, Berlin (2006)
Brim L., Cerná I., Moravec P., Simsa J.: Distributed partial order reduction of state spaces. Electr. Notes Theor. Comput. Sci. 128(3), 63–74 (2005)
Clarke, E.M., Emerson, E.A., Jha, S., Sistla, A.P.: Symmetry reductions in model checking. In: Computer Aided Verification. LNCS, vol. 1427, pp. 147–158. Springer, Berlin (1998)
Clarke E.M., Grumberg O., Peled D.: Model Checking. The MIT Press, Cambridge (1999)
Courcoubetis, C., Vardi, M.Y., Wolper, P., Yannakakis, M.: Memory efficient algorithms for the verification of temporal properties. In: Computer Aided Verification. LNCS, vol. 531, pp. 233–242. Springer, Berlin (1990)
Dill, D.L., Stern, U.: Using magnetic disk instead of main memory in the Murϕ Verifier. In: Computer Aided Verification. LNCS, vol. 1427, pp. 172–183. Springer, Berlin (1998)
Edelkamp S., Leue S., Lluch-Lafuente A.: Directed explicit-state model checking in the validation of communication protocols. Softw. Tools Technol. Transf. 5(2–3), 247–267 (2004)
Evangelista, S.: High level petri nets analysis with Helena. In: Applications and Theory of Petri Nets. LNCS, vol. 3536, pp. 455–464. Springer, Berlin (2005)
Evangelista, S., Kaiser, C., Pradat-Peyre, J.-F., Rousseau, P.: Quasar: a new tool for analysing concurrent programs. In: Reliable Software Technologies. LNCS, vol. 2655, pp. 168–181. Springer, Berlin (2003)
Evangelista, S., Pradat-Peyre, J.-F.: Memory efficient state space storage in explicit software model checking. In: SPIN, Model Checking of Software. LNCS, vol. 3639, pp. 43–57. Springer, Berlin (2005)
Flanagan C., Godefroid P.: Dynamic partial-order reduction for model checking software. In: Principles of Programming Languages, pp. 110–121. ACM, New York (2005)
Garavel, H., Mateescu, R., Smarandache, I.M.: Parallel state space construction for model-checking. In SPIN, Model Checking of Software. LNCS, vol. 2057, pp. 217–234. Springer, Berlin (2001)
Godefroid, P.: Partial-order methods for the verification of concurrent systems—an approach to the state-explosion problem. LNCS, vol. 1032. Springer, Berlin (1996)
Holzmann, G.J.: State compression in spin: recursive indexing and compression training runs. In: SPIN, Model Checking of Software (1997)
Holzmann G.J.: The model checker SPIN. IEEE Trans. Softw. Eng. 23(5), 279–295 (1997)
Norris Ip C., Dill D.L.: Better verification through symmetry. Formal Methods Syst. Des. 9(1/2), 41–75 (1996)
Kaiser, C., Pradat-Peyre, J.-F.:Chameneos, a concurrency game for Java, Ada and others. In: Computer Systems and Applications, p. 8 (2003)
Kurshan, R.P., Levin, V., Minea, M., Peled, D., Yenigun, H.: Static partial order reduction. In: Tools and Algorithms for the Construction and Analysis of Systems. LNCS, vol. 1384, pp. 345–357. Springer, Berlin (1998)
Lerda F., Sisto R. Distributed-memory model checking with SPIN. In: SPIN, Model Checking of Software. LNCS, vol. 1680, pp. 22–39. Springer, Berlin (1999)
Moravec P., Simsa J.: Relaxed cycle condition improves partial order reduction. In: Mathematical and Engineering Methods in Computer Science, pp. 152–159 (2006)
Nalumasu R., Gopalakrishnan G.: An efficient partial order reduction algorithm with an alternative proviso implementation. Formal Methods Syst. Des. 20(3), 231–247 (2000)
Pelánek, R.: BEEM: Benchmarks for explicit model checkers. In: SPIN, Model Checking of Software. LNCS, vol. 4595, pp. 263–267. Springer, Berlin (2007)
Peled, D.: All from one, one for all: on model checking using representatives. In: Computer Aided Verification. LNCS, vol. 697, pp. 409–423. Springer, Berlin (1993)
Peled, D.: Combining partial order reductions with on-the-fly model-checking. In: Computer Aided Verification. LNCS, vol. 818, pp. 377–390. Springer, Berlin (1994)
Stern U., Dill, D.L. (1997) Parallelizing the Murphi verifier. In Computer Aided Verification. LNCS, vol. 1254, pp. 256–278. Springer, Berlin (1997)
Tarjan R.E.: Depth-first search and linear graph algorithms. SIAM J. Comput. 1(2), 146–160 (1972)
Valmari, A.: Stubborn sets for reduced state space generation. In: Applications and Theory of Petri Nets. LNCS, vol. 483, pp. 491–515. Springer, Berlin (1989)
Valmari A.: A stubborn attack on state explosion. Formal Methods Syst. Des. 1(4), 297–322 (1992)
Valmari, A.: The state explosion problem. In: Lectures on Petri Nets I: Basic Models. LNCS, vol. 1491, pp. 429–528. Springer, Berlin (1998)
Varpaaniemi, K.: Efficient detection of deadlock in petri nets. Master’s thesis, Helsinki University of Technology, Department of Computer Science and Engineering, Digital Systems Laboratory (1993)
Varpaaniemi, K.: On stubborn sets in the verification of linear time temporal properties. In: Applications and Theory of Petri Nets. LNCS, vol. 1420, pp. 124–143. Springer, Berlin (1998)
Author information
Authors and Affiliations
Corresponding author
Additional information
S. Evangelista was supported by the Danish Research Council for Technology and Production.
Rights and permissions
About this article
Cite this article
Evangelista, S., Pajault, C. Solving the ignoring problem for partial order reduction. Int J Softw Tools Technol Transfer 12, 155–170 (2010). https://doi.org/10.1007/s10009-010-0137-y
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10009-010-0137-y