Abstract
FDR, initially introduced decades ago, is the de facto analyzer for Communicating Sequential Processes (CSP). Model checking techniques have been evolved rapidly since then. This paper describes Pat, i.e., a process analysis toolkit which complements FDR in several aspects. Pat is designed to analyze event-based compositional system models specified using CSP as well as shared variables and asynchronous message passing. It supports automated refinement checking, model checking of LTL extended with events, etc. In this paper, we highlight how partial order reduction is applied to improve refinement checking in Pat. Experiment results show that Pat outperforms FDR in some cases.
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
Formal Systems (Europe) Ltd. Process Behaviour Explorer (2003), http://www.fsel.com/probe_download.html
Chaki, S., Clarke, E.M., Ouaknine, J., Sharygina, N., Sinha, N.: State/Event-Based Software Model Checking. In: Boiten, E.A., Derrick, J., Smith, G.P. (eds.) IFM 2004. LNCS, vol. 2999, pp. 128–147. Springer, Heidelberg (2004)
Cimatti, A., Clarke, E.M., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, M., Sebastiani, R., Tacchella, A.: NuSMV 2: An OpenSource Tool for Symbolic Model Checking. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 359–364. Springer, Heidelberg (2002)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (2000)
Dong, J.S., Hao, P., Qin, S., Sun, J., Yi, W.: Timed Patterns: TCOZ to Timed Automata. In: Davies, J., Schulte, W., Barnett, M. (eds.) ICFEM 2004. LNCS, vol. 3308, pp. 483–498. Springer, Heidelberg (2004)
Gastin, P., Oddoux, D.: Fast LTL to Büchi Automata Translation. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 53–65. Springer, Heidelberg (2001)
Hoare, C.A.R.: Communicating Sequential Processes. International Series in Computer Science. Prentice-Hall, Englewood Cliffs (1985), www.usingcsp.com/cspbook.pdf
Holzmann, G.J.: The Model Checker SPIN. IEEE Trans. on Soft. Eng. 23(5), 279–295 (1997)
Sun, J.S.D.J., Liu, Y., Wang, H.H.: Specifying and Verifying Event-based Fairness Enhanced Systems. In: Proceedings of the 10th International Conference on Formal Engineering Methods (ICFEM 2008) (accepted, 2008)
Mahony, B., Dong, J.S.: Timed Communicating Object Z. IEEE Transactions on Software Engineering 26(2) (February 2000)
Parashkevov, A., Yantchev, J.: ARC - a Tool for Efficient Refinement and Equivalence Checking for CSP. In: Proceedings of the IEEE International Conference on Algorithms and Architectures for Parallel Processing (ICA3PP 1996), pp. 68–75 (1996)
Roscoe, A.W.: Model-checking CSP, pp. 353–378 (1994)
Roscoe, A.W.: Compiling Shared Variable Programs into CSP. In: Proceedings of PROGRESS workshop 2001 (2001)
Roscoe, A.W.: On the expressive power of CSP refinement. Formal Aspects of Computing 17(2), 93–112 (2005)
Roscoe, A.W., Gardiner, P.H.B., Goldsmith, M., Hulance, J.R., Jackson, D.M., Scattergood, J.B.: Hierarchical Compression for Model-Checking CSP or How to Check 10\(^{\mbox{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)
Roscoe, A.W., Wu, Z.Z.: Verifying Statemate Statecharts Using CSP and FDR. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 324–341. Springer, Heidelberg (2006)
Sun, J., Dong, J.S.: Design Synthesis from Interaction and State-Based Specifications. IEEE Transactions on Software Engineering 32(6), 349–364 (2006)
Valmari, A.: Stubborn Set Methods for Process Algebras. In: Proceedings of the Workshop on Parital Order Methods in Verification (PMIV 1996). DIMACS Series in Discrete Mathematics and Theoretical Computer Science, vol. 29, pp. 213–231 (1996)
Wehrheim, H.: Partial order reductions for failures refinement. Electronic Notes in Theoretical Computer Science 27 (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Sun, J., Liu, Y., Dong, J.S. (2008). Model Checking CSP Revisited: Introducing a Process Analysis Toolkit. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification and Validation. ISoLA 2008. Communications in Computer and Information Science, vol 17. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-88479-8_22
Download citation
DOI: https://doi.org/10.1007/978-3-540-88479-8_22
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-88478-1
Online ISBN: 978-3-540-88479-8
eBook Packages: Computer ScienceComputer Science (R0)