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.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall (1985)
Roscoe, A.: The Theory and Practice of Concurrency. Prentice Hall (1997)
Roscoe, A.: Understanding Concurrent Systems (2010)
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)
University of Oxford, Failures-Divergence Refinement–FDR 3 User Manual (2014). https://www.cs.ox.ac.uk/projects/fdr/manual/
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)
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)
Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem (1996)
Hansen, H., Wang, X.: Compositional analysis for weak stubborn sets. In: Application of Concurrency to System Design (ACSD) (2011)
Valmari, A.: Stubborn set methods for process algebras. In: Proceedings of the DIMACS Workshop on Partial Order Methods in Verification (1997)
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)
Valmari, A., Hansen, H.: Can stubborn sets be optimal?. Fundamenta Informaticae 113(3) (2011)
Varpaaniemi, K.: On the Stubborn Set Method in Reduced State Space Generation. PhD thesis, Helsinki University of Technology (1998)
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)
Evangelista, S., Pajault, C.: Solving the ignoring problem for partial order reduction. International Journal on Software Tools for Technology Transfer 12(2) (2010)
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)
Varpaaniemi, K.: Minimizing the number of successor states in the stubborn set method. Fundamenta Informaticae 51(1) (2002)
Valmari, A.: State space generation: Efficiency and practicality. PhD thesis, Tampere University of Technology (1988)
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)
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)
Roscoe, A.W., Hopkins, D.: SVA, a tool for analysing shared-variable programs. In: AVoCS (2007)
Gibson-Robinson, T., Roscoe, A.W.: FDR into the cloud. In Communicating Process Architectures (2014)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Gibson-Robinson, T., Hansen, H., Roscoe, A.W., Wang, X. (2015). Practical Partial Order Reduction for CSP. In: Havelund, K., Holzmann, G., Joshi, R. (eds) NASA Formal Methods. NFM 2015. Lecture Notes in Computer Science(), vol 9058. Springer, Cham. https://doi.org/10.1007/978-3-319-17524-9_14
Download citation
DOI: https://doi.org/10.1007/978-3-319-17524-9_14
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-17523-2
Online ISBN: 978-3-319-17524-9
eBook Packages: Computer ScienceComputer Science (R0)