Advertisement

Practical Partial Order Reduction for CSP

  • Thomas Gibson-RobinsonEmail author
  • Henri Hansen
  • A. W. Roscoe
  • Xu Wang
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9058)

Abstract

FDR is an explicit-state refinement checker for the process algebra CSP and, as such, is vulnerable to the state-explosion problem. In this paper, we show how a form of partial-order reduction, an automatic state reduction mechanism, can be utilised to soundly reduce the number of states that must be visited. In particular, we develop a compositional method for partial-order reduction that takes advantage of FDR’s internal, compositional, process representation. Further, we develop novel methods of preserving the traces of a process which allow partial-order reduction to be applied to arbitrary FDR refinement checks. We also provide details on how to efficiently implement the algorithms required for partial-order reduction.

Keywords

Dependency Graph Visible Action Label Transition System Communicate Sequential Process Disable Action 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall (1985)Google Scholar
  2. 2.
    Roscoe, A.: The Theory and Practice of Concurrency. Prentice Hall (1997)Google Scholar
  3. 3.
    Roscoe, A.: Understanding Concurrent Systems (2010)Google Scholar
  4. 4.
    Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.W.: FDR3 — A modern refinement checker for CSP. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 187–201. Springer, Heidelberg (2014) Google Scholar
  5. 5.
    University of Oxford, Failures-Divergence Refinement–FDR 3 User Manual (2014). https://www.cs.ox.ac.uk/projects/fdr/manual/
  6. 6.
    Valmari, A.: Stubborn sets for reduced state space generation. In: Rozenberg, G. (ed.) Advances in Petri Nets 1990. LNCS, vol. 483, pp. 491–515. Springer, Heidelberg (1991) Google Scholar
  7. 7.
    Peled, D.: All from one, one for all: on model checking using representatives. In: Courcoubetis, C. (ed.) Computer Aided Verification (CAV). LNCS, vol. 697, pp. 409–423. Springer, Heidelberg (1993) Google Scholar
  8. 8.
    Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem (1996)Google Scholar
  9. 9.
    Hansen, H., Wang, X.: Compositional analysis for weak stubborn sets. In: Application of Concurrency to System Design (ACSD) (2011)Google Scholar
  10. 10.
    Valmari, A.: Stubborn set methods for process algebras. In: Proceedings of the DIMACS Workshop on Partial Order Methods in Verification (1997)Google Scholar
  11. 11.
    Goldsmith, M., Moffat, N., Roscoe, A.W., Whitworth, T., Zakiuddin, I.: Watchdog transformations for property-oriented model-checking. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 600–616. Springer, Heidelberg (2003) Google Scholar
  12. 12.
    Valmari, A., Hansen, H.: Can stubborn sets be optimal?. Fundamenta Informaticae 113(3) (2011)Google Scholar
  13. 13.
    Varpaaniemi, K.: On the Stubborn Set Method in Reduced State Space Generation. PhD thesis, Helsinki University of Technology (1998)Google Scholar
  14. 14.
    Laarman, A., Pater, E., van de Pol, J., Weber, M.: Guard-based partial-order reduction. In: Bartocci, E., Ramakrishnan, C.R. (eds.) SPIN 2013. LNCS, vol. 7976, pp. 227–245. Springer, Heidelberg (2013) Google Scholar
  15. 15.
    Evangelista, S., Pajault, C.: Solving the ignoring problem for partial order reduction. International Journal on Software Tools for Technology Transfer 12(2) (2010)Google Scholar
  16. 16.
    Godefroid, P., Wolper, P.: Using partial orders for the efficient verification of deadlock freedom and safety properties. In: Larsen, K.G., Skou, A. (eds.) CAV 1991. LNCS, vol. 575, pp. 332–342. Springer, Heidelberg (1992) Google Scholar
  17. 17.
    Varpaaniemi, K.: Minimizing the number of successor states in the stubborn set method. Fundamenta Informaticae 51(1) (2002)Google Scholar
  18. 18.
    Valmari, A.: State space generation: Efficiency and practicality. PhD thesis, Tampere University of Technology (1988)Google Scholar
  19. 19.
    Roscoe, A.W., Gardiner, P., Goldsmith, M., Hulance, J., Jackson, D., Scattergood, J.: Hierarchical compression for model-checking CSP or how to check 10\(^{20}\) dining philosophers for deadlock. In: Brinksma, E., Steffen, B., Cleaveland, W.R., Larsen, K.G., Margaria, T. (eds.) TACAS 1995. LNCS, vol. 1019, pp. 133–152. Springer, Heidelberg (1995) Google Scholar
  20. 20.
    Boulgakov, A., Gibson-Robinson, T., Roscoe, A.W.: Computing maximal bisimulations. In: Merz, S., Pang, J. (eds.) ICFEM 2014. LNCS, vol. 8829, pp. 11–26. Springer, Heidelberg (2014) Google Scholar
  21. 21.
    Roscoe, A.W., Hopkins, D.: SVA, a tool for analysing shared-variable programs. In: AVoCS (2007)Google Scholar
  22. 22.
    Gibson-Robinson, T., Roscoe, A.W.: FDR into the cloud. In Communicating Process Architectures (2014)Google Scholar

Copyright information

© Springer International Publishing Switzerland 2015

Authors and Affiliations

  • Thomas Gibson-Robinson
    • 1
    Email author
  • Henri Hansen
    • 2
  • A. W. Roscoe
    • 1
  • Xu Wang
    • 1
    • 2
  1. 1.Department of Computer ScienceUniversity of OxfordOxfordUK
  2. 2.Department of MathematicsTampere University of TechnologyTampereFinland

Personalised recommendations