Skip to main content
SpringerLink
Log in

Process Algebra and Model Checking

  • Chapter
  • First Online:
Handbook of Model Checking

Abstract

Process algebras such as CCS, CSP and ACP are abstract notations for describing concurrent systems that interact via (usually) handshake-based communication. They lead to natural concepts of process state and are therefore natural candidates for model checking. We survey the area of process algebra and model checking, focusing on these three process algebras. We first introduce the syntax and semantics of these process algebras, before looking at the algorithmic basis for their model checking, which includes ideas such as bisimulation and refinement as well as the logics used to describe system-correctness properties. Finally, we introduce the process-alebra-based model-checking tools FDR, CWB and XMC, illustrating their utility by a number of case studies.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abdel-Rohman, M., Leipholz, H.H.E.: Structural control by pole assignment method. Eng. Mech. 104(5), 1157–1175 (1978)

    Google Scholar 

  2. Agrawal, A.K., Fujino, Y., Bhartia, B.K.: Instability due to time delay and its compensation in active control of structures. Earthq. Eng. Struct. Dyn. 22(3), 211–224 (1993)

    Article  Google Scholar 

  3. Armstrong, P., Goldsmith, M.H., Lowe, G., Ouaknine, J., Palikareva, H., Roscoe, A.W., Worrell, J.: Recent developments in FDR. In: Madhusudan, P., Seshia, S. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 7358, pp. 699–704. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  4. Armstrong, P., Lowe, G., Ouaknine, J., Roscoe, A.W.: Model checking timed CSP. In: Voronkov, A., Korovina, M. (eds.) HOWARD-60. A Festschrift on the Occasion of Howard Barringer’s 60th Birthday, pp. 13–33. EasyChair, Manchester (2014)

    Google Scholar 

  5. Baeten, J.C.M., Bergstra, J.A.: Real time process algebra. Form. Asp. Comput. 3(2), 142–188 (1991)

    Article  Google Scholar 

  6. Baeten, J.C.M., Bergstra, J.A., Smolka, S.A.: Axiomatizing probabilistic processes: ACP with generative probabilities. Inf. Comput. 121(2), 234–255 (1995)

    Article  MathSciNet  Google Scholar 

  7. Baeten, J.C.M., Weijland, W.P.: Process Algebra. Cambridge Tracts in Computer Science, vol. 18. Cambridge University Press, Cambridge (1990)

    MATH  Google Scholar 

  8. Basu, S., Smolka, S.A.: Model checking the Java metalocking algorithm. ACM Trans. Softw. Eng. Methodol. 16(3) (2007)

    Article  Google Scholar 

  9. Bergstra, J.A., Klop, J.W.: Algebra of communicating processes with abstraction. Theor. Comput. Sci. 37, 77–121 (1985)

    Article  MathSciNet  Google Scholar 

  10. Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.): Handbook of Process Algebra. Elsevier, Amsterdam (2001)

    MATH  Google Scholar 

  11. Blom, S., van de Pol, J., Weber, M.: LTSmin: distributed and symbolic reachability. In: Touili, T., Cook, B., Jackson, P. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 6174, pp. 354–359. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  12. Brookes, S.D., Hoare, C.A.R., Roscoe, A.W.: A theory of communicating sequential processes. J. ACM 31(3), 560–599 (1984)

    Article  MathSciNet  Google Scholar 

  13. Brookes, S.D., Roscoe, A.W.: An improved failures model for communicating processes. In: Brookes, S.D., Roscoe, A.W., Winskel, G. (eds.) Proceedings of the Pittsburgh Seminar on Concurrency. LNCS, vol. 197, pp. 281–305. Springer, Heidelberg (1985)

    Chapter  Google Scholar 

  14. Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Kozen, D. (ed.) Proceedings of the Workshop on Logic of Programs, Yorktown Heights. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1981)

    Chapter  Google Scholar 

  15. Cleaveland, R.: On automatically explaining bisimulation inequivalence. In: Clarke, E.M., Kurshan, R.P. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 531, pp. 364–372. Springer, Heidelberg (1991)

    Chapter  Google Scholar 

  16. Cleaveland, R., Hennessy, M.C.B.: Testing equivalence as a bisimulation equivalence. In: Sifakis, J. (ed.) Automatic Verification Methods for Finite State Systems. LNCS, vol. 407, pp. 11–23. Springer, Heidelberg (1989)

    Chapter  Google Scholar 

  17. Cleaveland, R., Hennessy, M.C.B.: Testing equivalence as a bisimulation equivalence. Form. Asp. Comput. 5(1), 1–20 (1993)

    Article  Google Scholar 

  18. Cleaveland, R., Lewis, P.M., Smolka, S.A., Sokolsky, O.: The Concurrency Factory: a development environment for concurrent systems. In: Alur, R., Henzinger, T.A. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 1102, pp. 398–401. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

  19. Cleaveland, R., Parrow, J., Steffen, B.U.: The Concurrency Workbench: a semantics-based tool for the verification of finite-state systems. Tech. Rep. ECS-LFCS-89-83, Department of Computer Science, University of Edinburgh (1989)

    Google Scholar 

  20. Cleaveland, R., Parrow, J., Steffen, B.U.: A semantics-based tool for the verification of finite-state systems. In: Proceedings of the Ninth IFIP Symposium on Protocol Specification, Testing and Verification. North-Holland, Amsterdam (1989)

    Google Scholar 

  21. Cleaveland, R., Parrow, J., Steffen, B.U.: The Concurrency Workbench: a semantics-based tool for the verification of concurrent systems. ACM Trans. Program. Lang. Syst. 15(1), 36–72 (1993)

    Article  Google Scholar 

  22. Cleaveland, R., Sims, S.: Generic tools for verifying concurrent systems. Sci. Comput. Program. 42(1), 39–47 (2002)

    Article  Google Scholar 

  23. Colouris, G., Dollimore, J., Kindberg, T.: Distributed Systems, Concepts and Design. Addison-Wesley, Reading (1994)

    Google Scholar 

  24. Creese, S.J., Roscoe, A.W.: TTP: a case study in combining induction and data independence. Tech. Rep. PRG-TR-1-99, Oxford University Computing Laboratory (1999)

    Google Scholar 

  25. Creese, S.J., Roscoe, A.W.: Verifying an infinite family of inductions simultaneously using data independence and FDR. In: Wu, J., Chanson, S.T., Gao, Q. (eds.) Proceedings of FORTE/PSTV’99, pp. 437–452. Springer, Heidelberg (1999)

    MATH  Google Scholar 

  26. Creese, S.J., Roscoe, A.W.: Data independent induction over stuctured networks. In: Arabnia, H.R. (ed.) Proceedings of PDPTA 2000. CSREA (2000)

    Google Scholar 

  27. Dams, D., Grumberg, O.: Abstraction and abstraction refinement. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking. Springer, Heidelberg (2018)

    Google Scholar 

  28. Du, X., McDonnell, K.T., Nanos, E., Ramakrishna, Y.S., Smolka, S.A.: Software design, specification, and verification: lessons learned from the Rether Case Study. In: Johnson, M. (ed.) Proceedings of the Sixth Internationaal Conference on Algebraic Methodology and Software Technology (AMAST). LNCS, vol. 1349, pp. 185–198. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  29. Elseaidy, W.M., Cleaveland, R., Baugh, J.W. Jr.: Modeling and verifying active structural control systems. Sci. Comput. Program. 29(1–2), 99–122 (1997)

    Article  Google Scholar 

  30. Emerson, E.A., Lei, C.L.: Efficient model checking in fragments of the propositional mu-calculus. In: Symp. on Logic in Computer Science (LICS), pp. 267–278. IEEE, Piscataway (1986)

    Google Scholar 

  31. Garcia-Molina, H.: Elections in a distributed computing system. IEEE Trans. Comput. 31(1), 48–59 (1982)

    Article  Google Scholar 

  32. Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.W.: FDR3: a modern refinement checker for CSP. In: Abraham, E., Mavelund, K. (eds.) Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 8413, pp. 187–201 (2014)

    Google Scholar 

  33. Gibson-Robinson, T., Roscoe, A.W.: FDR into the cloud. In: Welch, P.H., et al. (eds.) Proceedings of Communicating Process Architectures (CPA). Open Channel Publishing (2014)

    Google Scholar 

  34. Glabbeek, R.J.V., Weijland, W.P.: Branching time and abstraction in bisimulation semantics. J. ACM 43(3), 555–600 (1996)

    Article  MathSciNet  Google Scholar 

  35. Groote, J.F., Mousavi, M.R.: Modeling and Analysis of Communicating Systems. MIT Press, Cambridge (2014)

    MATH  Google Scholar 

  36. Hansson, H., Jonsson, B.: A calculus for communicating systems with time and probabilities. In: Proceedings 11th Real-Time Systems Symposium (RTSS), pp. 278–287. IEEE, Piscataway (1990)

    Google Scholar 

  37. Hennessy, M.C.B., Milner, R.: Algebraic laws for nondeterminism and concurrency. J. ACM 32(1), 137–161 (1985)

    Article  MathSciNet  Google Scholar 

  38. Henzinger, M.R., Henzinger, T.A., Kopke, P.W.: Computing simulations on finite and infinite graphs. In: 36th Annual Symposium on Foundations of Computer Science, pp. 453–462. IEEE, Piscataway (1995)

    MATH  Google Scholar 

  39. Henzinger, T.A., Manna, Z., Pnueli, A.: What good are digital clocks? In: International Colloquium on Automata, Languages and Programming (ICALP). LNCS, vol. 623, pp. 545–558. Springer, Heidelberg (1992)

    Chapter  Google Scholar 

  40. Hoare, C.A.R.: Communicating sequential processes. Commun. ACM 21(8), 666–677 (1978)

    Article  Google Scholar 

  41. Hoare, C.A.R.: A model for communicating sequential processes, tech. monograph PRG-22, Programming Research Group, Oxford University Computing Laboratory (1981)

    Google Scholar 

  42. Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall, New York (1985)

    MATH  Google Scholar 

  43. Holzmann, G.J.: Designing executable abstractions. In: Proceedings of the Second Workshop on Formal Methods in Software Practice (FMSP), pp. 103–108. ACM, New York (1998)

    Chapter  Google Scholar 

  44. Hopcroft, P.J., Broadfoot, G.: Combining the box structure development method and CSP for software development. Electron. Notes Theor. Comput. Sci. 128(6), 127–144 (2005)

    Article  Google Scholar 

  45. Hunt, H.B., Rosenkrantz, D.J., Szymanski, T.G.: On the equivalence, containment, and covering problems for the regular and context-free languages. J. Comput. Syst. Sci. 12(2), 222–268 (1976)

    Article  MathSciNet  Google Scholar 

  46. Hwong, Y.L., Keiren, J.J.A., Kusters, V.J.J., Leemans, S., Willemse, T.A.C.: Formalising and analysing the control software of the Compact Muon Solenoid experiment at the Large Hadron Collider. Sci. Comput. Program. 78(12), 2435–2452 (2013)

    Article  Google Scholar 

  47. Kanellakis, P.C., Smolka, S.A.: CCS expressions, finite state processes, and three problems of equivalence. Inf. Comput. 86(1), 43–68 (1990)

    Article  MathSciNet  Google Scholar 

  48. Kozen, D.: Results on the propositional \(\mu\)-calculus. Theor. Comput. Sci. 27(3), 333–354 (1983)

    Article  MathSciNet  Google Scholar 

  49. Lawrence, J.: Practical application of CSP and FDR in software design. In: Abdallah, A.E., Jones, C.B., Sanders, J.W. (eds.) Communicating Sequential Processes. The First 25 Years. LNCS, vol. 3525, pp. 151–175. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  50. Lazic, R.S.: A semantic study of data independence with applications to model checking. Ph.D. thesis, University of Oxford (1999)

    Google Scholar 

  51. Limited, I.: Occam Programming Manual. Prentice Hall, New York (1984)

    Google Scholar 

  52. Liu, Y., Sun, J., Dong, J.S.: PAT 3: an extensible architecture for building multi-domain model checkers. In: Proceedings of the 22nd International IEEE Symposium on Software Reliability Engineering (ISSRE), pp. 190–199. IEEE, Piscataway (2011)

    Google Scholar 

  53. Lowe, G.: Probabilistic and prioritized models of timed CSP. Theor. Comput. Sci. 138(2), 315–352 (1995)

    Article  MathSciNet  Google Scholar 

  54. Lowe, G.: Breaking and fixing the Needham-Schroeder public-key protocol using FDR. In: Intl. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). LNCS, vol. 1055, pp. 147–166. Springer, Heidelberg (1996)

    Google Scholar 

  55. Lowe, G.: Casper: a compiler for the analysis of security protocols. In: Proceedings of the 10th Computer Security Foundations Workshop (CSFW), pp. 18–30. IEEE, Piscataway (1997)

    Chapter  Google Scholar 

  56. Lu, S., Smolka, S.: Model checking the secure electronic transaction (SET) protocol. In: Proceedings of the 7th International Symposium on Modeling, Analysis and Simulation of Computer and Telecommunication Systems (MASCOTS), pp. 358–364. IEEE, Piscataway (1999)

    Google Scholar 

  57. Luttik, B.: What is algebraic in process theory? In: Proceedings of the Workshop “Essays on Algebraic Process Calculi” (APC 25). Electronic Notes in Theoretical Computer Science, vol. 162, pp. 227–231 (2006)

    Google Scholar 

  58. Milner, R.: A Calculus of Communicating Systems. LNCS, vol. 92. Springer, Heidelberg (1980)

    MATH  Google Scholar 

  59. Milner, R.: Communication and Concurrency. International Series in Computer Science. Prentice Hall, New York (1989)

    MATH  Google Scholar 

  60. Milner, R., Parrow, J., Walker, D.J.: A calculus of mobile processes. Inf. Comput. 100(1), 1–40 (1992)

    Article  MathSciNet  Google Scholar 

  61. Ouaknine, J.: Discrete analysis of continuous behaviour in real-time concurrent systems. Ph.D. thesis, University of Oxford (2000)

    Google Scholar 

  62. Ouaknine, J., Palikareva, H., Roscoe, A.W., Worrell, J.: Static livelock analysis in CSP. In: Katoen, J.P., König, B. (eds.) Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol. 6901, pp. 389–403. Springer, Heidelberg (2011)

    Google Scholar 

  63. Paige, R., Tarjan, R.E.: Three partition refinement algorithms. SIAM J. Comput. 16(6), 973–989 (1987)

    Article  MathSciNet  Google Scholar 

  64. Palikareva, H., Ouaknine, J., Roscoe, A.W.: SAT-solving in CSP trace refinement. Sci. Comput. Program. 77(10), 1178–1197 (2012)

    Article  Google Scholar 

  65. Peleska, J.: Applied formal methods—from CSP to executable hybrid specifications. In: Abdallah, A.E., Jones, C.B., Sanders, J.W. (eds.) Communicating Sequential Processes. The First 25 Years. LNCS, vol. 3525, pp. 293–320. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  66. Ploeger, B.: Analysis of ACS using mCRL2. Tech. Rep. CS–09–11, Technische Universiteit Eindhoven (2009)

    Google Scholar 

  67. Plotkin, G.: A structural approach to operational semantics. Tech. Rep. DAIMI FN-19, Computer Science Department, Aarhus University (1981)

    Google Scholar 

  68. Ramakrishna, Y.S., Smolka, S.A.: Partial-order reduction in the weak modal mu-calculus. In: Mazurkiewicz, A., Winkowski, J. (eds.) Intl. Conf. on Concurrency Theory (CONCUR). LNCS, vol. 1243, pp. 5–24. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  69. Ramakrishnan, C.R., Ramakrishnan, I.V., Smolka, S.A., et al.: XMC: a logic-programming-based verification toolset. In: Emerson, E.A., Sistla, A.P. (eds.) Intl. Conf. on Computer-Aided Verification (CAV). LNCS, vol. 1855, pp. 576–580. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  70. Reed, G.M., Roscoe, A.W.: A timed model for communicating sequential processes. Theor. Comput. Sci. 58(1–3), 249–261 (1988)

    Article  MathSciNet  Google Scholar 

  71. Roscoe, A.W.: Unbounded non-determinism in CSP. J. Log. Comput. 3(2), 131–172 (1993)

    Article  Google Scholar 

  72. Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice Hall, New York (1997)

    Google Scholar 

  73. Roscoe, A.W.: Seeing beyond divergence. In: Abdallah, A.E., Jones, C.B., Sanders, J.W. (eds.) Communicating Sequential Processes. The First 25 Years. LNCS, vol. 3525, pp. 15–35. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  74. Roscoe, A.W.: CSP is expressive enough for \(\pi\). In: Jones, C.B., Roscoe, A.W., Wood, K.R. (eds.) Reflections on the Work of C.A.R. Hoare, pp. 371–404. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  75. Roscoe, A.W.: Understanding Concurrent Systems. Springer, Heidelberg (2010)

    Book  Google Scholar 

  76. Roscoe, A.W., Hopcroft, P.J.: Slow abstraction through priority. In: Liu, Z., Woodcock, J., Zhu, H. (eds.) Theories of Programming and Formal Methods. LNCS, vol. 8051, pp. 326–345. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  77. Roscoe, A.W., Huang, J.: Checking noninterference in timed CSP. Form. Asp. Comput. 25(1), 3–35 (2013)

    Article  MathSciNet  Google Scholar 

  78. Roscoe, A.W., Wu, Z.: Verifying statemate statecharts using CSP and FDR. In: Liu, Z., He, J. (eds.) Proceedings of Formal Methods and Software Engineering (FMSE). LNCS, vol. 4260, pp. 324–341. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  79. Sangiorgi, D., Walker, D.J.: The pi-Calculus: A Theory of Mobile Processes. Cambridge University Press, Cambridge (2003)

    MATH  Google Scholar 

  80. Scattergood, J.: The semantics and implementation of machine-readable CSP. Ph.D. thesis, University of Oxford (1998)

    Google Scholar 

  81. Schneider, S.A.: Concurrent and Real-Time Systems. Wiley, New York (2000)

    Google Scholar 

  82. Soong, T.T.: Active Structural Control. Longman, New York (1990)

    Google Scholar 

  83. Steffen, B.: Characteristic formulae. In: Ausiello, G., Dezani-Ciancaglini, M., Rocca, S.R.D. (eds.) Proceedings of the International Colloquium on Automata, Languages and Programming (ICALP). LNCS, vol. 372, pp. 723–732. Springer, Heidelberg (1989)

    Chapter  Google Scholar 

  84. Walker, D.J.: Bisimulation and divergence in CCS. In: Symp. on Logic in Computer Science (LICS), pp. 186–192. IEEE, Piscataway (1988)

    Google Scholar 

  85. Welch, P.H., Barnes, F.R.M.: Communicating mobile processes. In: Abdallah, A.E., Jones, C.B., Sanders, J.W. (eds.) Communicating Sequential Processes. The First 25 Years. LNCS, vol. 3525, pp. 175–210. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  86. Yang, J.N., Akbarpour, A., Ghaemmaghami, P.: New control algorithms for structural control. Eng. Mech. 113(9), 1369–1386 (1987)

    Article  Google Scholar 

  87. Yantchev, J.T.: ARC—a tool for efficient refinement and equivalence checking for CSP. In: IEEE Second Int. Conf. on Algorithms and Architectures for Parallel Processing (ICAPP), pp. 68–75. IEEE, Piscataway (1996)

    Google Scholar 

  88. Yi, W.: CCS + time = an interleaving model for real-time systems. In: Albert, J.L., Monien, B., Rodríguez-Artalejo, M. (eds.) International Colloquium on Automata, Languages and Programming (ICALP). LNCS, vol. 510, pp. 217–228. Springer, Heidelberg (1991)

    Chapter  Google Scholar 

  89. Zakiuddin, M.I., Moffat, N., O’Halloran, C.M., Ryan, P.Y.A.: Chasing events to certify a critical system. Tech. rep., UK Defence Evaluation and Research Agency (1998)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Maryland, College Park, College Park, MD, USA

    Rance Cleaveland

  2. University of Oxford, Oxford, UK

    A. W. Roscoe

  3. Stony Brook University, Stony Brook, NY, USA

    Scott A. Smolka

Authors
  1. Rance Cleaveland
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. A. W. Roscoe
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Scott A. Smolka
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to A. W. Roscoe .

Editor information

Editors and Affiliations

  1. FORE Systems University Professor of Computer Science, Carnegie Mellon University, Pittsburgh, Pennsylvania, USA

    Edmund M. Clarke

  2. Institute of Science and Technology Austria (IST), Klosterneuburg, Austria

    Thomas A. Henzinger

  3. Arbeitsbereich Formal Methods in Systems Engineering, Technische Universität Wien, Wien, Austria

    Helmut Veith

  4. Institut f. Angewandte Informationsverarbeitung und Kommunikationstechnologie (IAIK), Technische Universität Graz, Graz, Austria

    Roderick Bloem

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG, part of Springer Nature

About this chapter

Check for updates. Verify currency and authenticity via CrossMark

Cite this chapter

Cleaveland, R., Roscoe, A.W., Smolka, S.A. (2018). Process Algebra and Model Checking. In: Clarke, E., Henzinger, T., Veith, H., Bloem, R. (eds) Handbook of Model Checking. Springer, Cham. https://doi.org/10.1007/978-3-319-10575-8_32

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-10575-8_32

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-10574-1

  • Online ISBN: 978-3-319-10575-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation