Abstract
In this paper, we present the denotational semantics for channel mobility in the Unifying Theories of Programming (UTP) semantics framework. The basis for the model is the UTP theory of reactive processes, precisely, the UTP semantics for Communicating Sequential Processes (CSP), which is extended to allow the mobility of channels—the set of channels that a process can use for communication (its interface), originally static or constant (set during the process's definition), is now made dynamic or variable: it can change during the process's execution. A channel is thus moved around by communicating it via other channels and then allowing the receiving process to extend its interface with the received channel. We introduce a new concept, the capability of a process, which allows separating the ownership of channels from the knowledge of their existence. Mobile processes are then defined as having a static capability and a dynamic interface. Operations of a mobile telecommunications network, e.g., handover, load balancing, are used to illustrate the semantics. We redefine CSP operators and in particular provide the first semantics for the renaming and hiding operators in the context of channel mobility.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Abrial JR (1984) The mathematical construction of a program. In: Science of computer programming, vol 4. Elsevier, pp 45–86. doi: https://doi.org/10.1016/0167-6423(84)90011-X
Bialkiewicz J-A, Peschanski F (2009) A denotational study of Mobility. In: Communicating process architectures, vol 67. IOS Press, pp 239–261. https://doi.org/10.3233/978-1-60750-065-0-239
Boreale M (1998) On the expressiveness of internal mobility in name-passing calculi. In: Theoretical computer science, vol 195. Elsevier, pp 205–226. https://doi.org/10.1016/S0304-3975(97)00220-X
Broy M, Dederichs F, Dendorfer C, Fuchs M, Gritzner TF, Weber R (1993) The design of distributed systems—an introduction to FOCUS (revised), Technical Report, University of Munich. citeseer.edu/broy93.pdf
Cavalcanti A, Woodcock J (2006) A tutorial introduction to CSP in unifying theories of programming. In: Refinement techniques in software engineering, Springer. pp 220–268. https://doi.org/10.1007/11889229_6
Ekembe Ngondi G (2016) Unifying theories of mobile channels. In: Proceedings 17th international workshop on refinement, EPTCS vol 209. pp 24–39. https://doi.org/10.4204/EPTCS.209.3
Ekembe Ngondi, G., Woodcock, J.: UTP semantics of reactive processes with continuations. Proceedings of international symposium on UTP, LNCS 10134, 114–133 (2016). https://doi.org/10.1007/978-3-319-52228-9_6
Ekembe Ngondi G (2016) Denotational semantics of mobility in unifying theories of programming (UTP), Ph.D. Thesis, University of York. http://etheses.whiterose.ac.uk/16525/7/Thesis_draft6_1.pdfetheses.whiterose.ac.uk/ek16.pdf
Giunti, M., Palamidessi, C., Valencia, F.D.: Hide and new in the Pi-Calculus. Proceedings of joint workshop on expresiveness/structure operation semantics, EPTCS 89, 65–80 (2012). https://doi.org/10.4204/EPTCS.89
Fuggetta, A., Picco, G.P., Vigna, G.: Understanding code mobility. IEEE Trans Softw Eng 24, 342–361 (1998). https://doi.org/10.1109/32.685258
Grosu R, Stolen K (1999) Stream based specification of mobile systems. In: Formal aspects of computing, vol 13. Springer, pp 1–31. https://doi.org/10.1007/PL00003937
Harwood, W., Cavalcanti, A., Woodcock, J.: A theory of pointers for the UTP. International colloquium on theoretical aspects of computing, LNCS 5160, 141–155 (2008). https://doi.org/10.1007/978-3-540-85762-4_10
Hoare, T.: Communicating sequential processes. Prentice-Hall (1985)
Hoare T, He Jifeng, (1998) Unifying theories of programming. Prentice-Hall
Hoare T, O'Hearn P (2008) Separation logic semantics for communicating processes. In: Proceedings of 1st international conference on foundations of information, computer and software ENTCS vol 212. pp 3–25, Elsevier. https://doi.org/10.1016/j.entcs.2008.04.050
McEwan A, Woodcock J (2010) Unifying theories of interrupts. In: Proceedings of international symposium on UTP, LNCS, vol 5713. Springer, pp 122–141. https://doi.org/10.1007/978-3-642-14521-6_8
Milner, R.: Communicating and mobile systems: the pi-calculus. Cambridge University Press (1999)
Roscoe, A.W.: The theory and practice of concurrency. Prentice-Hall (1998)
Roscoe AW (2010) Understanding concurrent systems, Chap. 20, §20.3. pp 497–506, Prentice-Hall. https://doi.org/10.1007/978-1-84882-258-0
Roscoe AW (2011) On the expressiveness of CSP, draft. http://www.cs.ox.ac.uk/files/1383/expressive.pdf
Roscoe AW (2010) CSP is expressive enough for Pi. In: `Reflections on the Work of C.A.R. Hoare', history of computing 2010, pp 371–404. https://doi.org/10.1007/978-1-84882-912-1_16
Sangiorgi D (1996) \(\pi \)-calculus, Internal mobility and agent-passing Calculi. In: Theoretical computer science, vol 167. Elsevier, pp 235–274. https://doi.org/10.1016/0304-3975(96)00075-8
Schneider S, Treharne H, Vajar B (2007) Introducing mobility into CSP\(||\)B. In: Automated verification of critical systems (AVoCS). http://epubs.surrey.ac.uk/7216/2/avocs07.pdfepubs.surrey.ac.uk/avocs07.pdf
Stølen K (1999) Specification of dynamic reconfiguration in the context of input/output relations. In: International conference on FMOODS, IFIPAICT, vol 10. Springer, pp 259–272. https://doi.org/10.1007/978-0-387-35562-7_20
Tang X, Woodcock J (2004) Towards mobile processes in UTP. In: Proceedings of 2nd international conference SEFM, vol 1. IEEE, pp 44–53. https://doi.org/10.1109/SEFM.2004.10045
Vajar B, Schneider S, Treharne H (2009) Mobile CSP\(||\)B. In: AVoCS, electronic communication of the EASST. https://doi.org/10.14279/tuj.eceasst.23.338
Welch PH, Barnes FRM (2004) Communicating mobile processes - introducing occam-pi. In: Communicating sequential processes: the first 25 years, symposium on the occasion of 25 years of CSP. pp 175–210. https://doi.org/10.1007/11423348_10
Welch PH, Barnes FRM (2008) A CSP model for mobile channels. In: Communicating process architectures (CPA), vol 66. IOS Press, pp 17-33. https://doi.org/10.3233/978-1-58603-907-3-17
Woodcock J, Wellings AJ, Cavalcanti A (2015) Mobile CSP. In: Brazilian symposium on formal methods, LNCS, vol 9526. Springer, pp 39–55. https://doi.org/10.1007/978-3-319-29473-5_3
Acknowledgements
The author is grateful to Prof. Jim Woodcock for his guidance in formulating a sound theory of channel mobility. My gratitude extends to anonymous reviewers for their useful comments.
Funding
Open Access funding provided by the IReL Consortium.
Author information
Authors and Affiliations
Corresponding author
Additional information
Eerke Albert Boiten
Publisher’s Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
Rights and permissions
Open Access This article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article's Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article's Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/.
About this article
Cite this article
Ekembe Ngondi, G. Denotational semantics of channel mobility in UTP-CSP. Form Asp Comp 33, 803–826 (2021). https://doi.org/10.1007/s00165-021-00546-3
Received:
Revised:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00165-021-00546-3