Skip to main content
SpringerLink
Log in

Mobile CSP

  • Conference paper
  • First Online:
Book cover Formal Methods: Foundations and Applications (SBMF 2015)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 9526))

Included in the following conference series:

Abstract

We describe an extension of imperative CSP with primitives to declare new event names and to exchange them by message passing between processes. We give examples in Mobile CSP to motivate the language design, and describe its semantic domain, based on the standard failures-divergences model for CSP, but also recording a dynamic event alphabet. The traces component is identical to the separation logic semantics of Hoare & O’Hearn. Our novel contribution is a semantics for mobile channels in CSP, described in Unifying Theories of Programming, that supports: compositionality with other language paradigms; channel faults, nondeterminism, deadlock, and livelock; multi-way synchronisation; and many-to-many channels. We compare and contrast our semantics with other approaches, including the \(\pi \)-calculus, and consider implementation issues. As well as modelling reconfigurable systems, our extension to CSP provides semantics for techniques such as dynamic class-loading and the full use of dynamic dispatching and delegation.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 34.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 44.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Bjørndalen, J., et al.: PyCSP - CSP for Python. In: McEwan, A., et al. (eds.) CPA, pp. 229–248 (2007)

    Google Scholar 

  2. Buschmann, F.: Pattern-Oriented Software Architecture. Wiley, New York (1996)

    Google Scholar 

  3. Sherif, A., Woodcock, J., Butterfield, A.: Slotted-Circus. In: Davies, J., Gibbons, J. (eds.) IFM 2007. LNCS, vol. 4591, pp. 75–97. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  4. Woodcock, J., Cavalcanti, A.: A tutorial introduction to CSP in unifying theories of programming. In: Cavalcanti, A., Sampaio, A., Woodcock, J. (eds.) PSSE 2004. LNCS, vol. 3167, pp. 220–268. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  5. Cavalcanti, A.: Unifying classes and processes. SoSyM 4(3), 277–296 (2005)

    MathSciNet  Google Scholar 

  6. Cavalcanti, A., et al.: Safety-critical Java in Circus. In: Wellings, A., et al. (eds.) JTRES, pp. 20–29 (2011)

    Google Scholar 

  7. Woodcock, J., Cavalcanti, A., Wellings, A.: The safety-critical Java memory model: a formal account. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 246–261. Springer, Heidelberg (2011)

    Google Scholar 

  8. Cavalcanti, A., et al.: The safety-critical Java memory model formalised. Formal Asp. Comput. 25(1), 37–57 (2013)

    Article  MathSciNet  MATH  Google Scholar 

  9. Cavalcanti, A., et al.: Safety-critical Java programs from Circus models. Real-Time Syst. 49(5), 614–667 (2013)

    Article  MATH  Google Scholar 

  10. Fischer, C.: Combining object-Z and CSP. In: Wolisz, A., et al. (eds.) Formale Beschreibungstechniken für verteilte Systeme. GMD-Studien, vol. 315, pp. 119–128 (1997)

    Google Scholar 

  11. Hoare, C.A.R.: Communicating Sequential Processes. Prentice Hall, Upper Saddle River (1985)

    MATH  Google Scholar 

  12. Hoare, C.A.R., He, J.: Unifying Theories of Programming. Prentice Hall, Englewood Cliffs (1998)

    Google Scholar 

  13. Hoare, T., O’Hearn, P.W.: Separation logic semantics for communicating processes. ENTCS 212, 3–25 (2008)

    Google Scholar 

  14. ISO: ISO, IEC, 2012 Information technology - Prog. languages - Ada, 8652 (2012)

    Google Scholar 

  15. Karsai, G.: Unification or integration? the challenge of semantics in heterogeneous modeling languages. In: Combemale, B., et al. (eds.) The Globalization of Modeling Languages, pp. 2–6 (2014)

    Google Scholar 

  16. Li, X., Jifeng, H., Liu, Z.: rCOS: refinement of component and object systems. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2004. LNCS, vol. 3657, pp. 183–221. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  17. Meyer, B.: Object-Oriented Software Construction. Prentice Hall, Upper Saddle River (1997)

    MATH  Google Scholar 

  18. Milner, R., et al.: A calculus of mobile processes. Inf. Comput. 100, 41–77 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  19. FDR3 model checker. www.cs.ox.ac.uk/projects/fdr/

  20. Odersky, M.: Programming in Scala. Mountain View, California (2008)

    Google Scholar 

  21. Oliveira, M., et al.: A denotational semantics for Circus. Electr. Notes Theor. Comput. Sci. 187, 107–123 (2007)

    Article  Google Scholar 

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

    Google Scholar 

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

    Chapter  Google Scholar 

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

    Book  MATH  Google Scholar 

  25. RTCA. Object-oriented technology and related techniques supplement to DO-178C [ED-12C] and DO-178A. Technical report DO-332/ED-217, [ED-109A] (2011)

    Google Scholar 

  26. Schneider, S., Treharne, H.: Communicating B machines. In: Bert, D., Bowen, J.P., C. Henson, M., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol. 2272, p. 416. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  27. Sherif, A., et al.: A process algebraic framework for specification and validation of real-time systems. Formal Asp. Comput. 22(2), 153–191 (2010)

    Article  MATH  Google Scholar 

  28. Smyth, N.: Communicating Sequential Processes in Ptolemy II. Tech. Memo. UCB/ERL M98/70, Electronics Research Laboratory, Berkeley, December 1998

    Google Scholar 

  29. Sun, J., et al.: Model checking CSP revisited: introducing a process analysis toolkit. In: Margaria, T.T., et al. (eds.) ISoLA, pp. 307–322. Springer, Heidelberg (2008)

    Google Scholar 

  30. Tang, X., et al.: Towards mobile processes in unifying theories. In: SEFM, pp. 44–53(2004)

    Google Scholar 

  31. Tang, X., Woodcock, J.: Travelling processes. In: Kozen, D. (ed.) MPC 2004. LNCS, vol. 3125, pp. 381–399. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  32. \({\sf inmos.}\) occam Programming Manual. Prentice Hall (1984)

    Google Scholar 

  33. Schneider, S., Treharne, H.: How to drive a B machine. In: Bowen, J.P., Dunne, S., Galloway, A., King, S. (eds.) B 2000, ZUM 2000, and ZB 2000. LNCS, vol. 1878, p. 188. Springer, Heidelberg (2000)

    Google Scholar 

  34. Vajar, B., et al.: Mobile CSP\(\parallel \)B. In: ECEASST 23 (2009)

    Google Scholar 

  35. Welch, P.H., et al.: The JCSP (CSP for Java) Home Page (1999)

    Google Scholar 

  36. Welch, P.H.: Mobile barriers for \(\sf occam\)-\(\pi \), et al.: semantics, implementation and application. In: Broenink, J.F., et al. (eds.) CPA, pp. 289–316 (2005)

    Google Scholar 

  37. Woodcock, J.: Engineering \(\sf UToPiA\). In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 22–41. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

  38. Woodcock, J., et al.: A concurrent language for refinement. In: Butterfield, A., et al. (eds.) 5th Irish Workshop on Formal Methods (2001)

    Google Scholar 

  39. Woodcock, J., Cavalcanti, A.: The semantics of Circus. In: Bert, D., Bowen, J.P., C. Henson, M., Robinson, K. (eds.) B 2002 and ZB 2002. LNCS, vol. 2272, pp. 184–203. Springer, Heidelberg (2002)

    Google Scholar 

  40. Woodcock, J., Cavalcanti, A.: A tutorial introduction to designs in unifying theories of programming. In: Boiten, E.A., Derrick, J., Smith, G.P. (eds.) IFM 2004. LNCS, vol. 2999, pp. 40–66. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  41. Woodcock, J., et al.: Features of CML: A formal modelling language for systems of systems. In: ICOSE, pp. 445–450 (2012)

    Google Scholar 

  42. Zeyda, F., Cavalcanti, A., Wellings, A.: The safety-critical Java mission model: a formal account. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol. 6991, pp. 49–65. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

Download references

Acknowledgements

This work has been supported by the EPSRC hiJaC and the EU H2020 INTO-CPS projects. Thanks to Philippa Gardiner for an application of the \(\pi \)-calculus that led to Example 2; to Peter Welch for discussions more than a decade ago on mobile channels in occam- \(\pi \) that led to the semantic model in this paper; and to three anonymous referees for prompting clarifications in the paper.

Author information

Authors and Affiliations

  1. Department of Computer Science, University of York, York, UK

    Jim Woodcock, Andy Wellings & Ana Cavalcanti

Authors
  1. Jim Woodcock
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Andy Wellings
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Ana Cavalcanti
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Jim Woodcock .

Editor information

Editors and Affiliations

  1. Universidade Federal de Pernambuco, Recife - PE, Brazil

    Márcio Cornélio

  2. University of Oxford, Oxford, United Kingdom

    Bill Roscoe

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing Switzerland

About this paper

Cite this paper

Woodcock, J., Wellings, A., Cavalcanti, A. (2016). Mobile CSP. In: Cornélio, M., Roscoe, B. (eds) Formal Methods: Foundations and Applications. SBMF 2015. Lecture Notes in Computer Science(), vol 9526. Springer, Cham. https://doi.org/10.1007/978-3-319-29473-5_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-29473-5_3

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-29472-8

  • Online ISBN: 978-3-319-29473-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation