{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:15:34Z","timestamp":1759637734388,"version":"3.37.3"},"reference-count":29,"publisher":"Association for Computing Machinery (ACM)","issue":"4-5","license":[{"start":{"date-parts":[[2021,8,1]],"date-time":"2021-08-01T00:00:00Z","timestamp":1627776000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,5,27]],"date-time":"2021-05-27T00:00:00Z","timestamp":1622073600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2021,8]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>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\u2014the 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<jats:italic>capability<\/jats:italic>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.<\/jats:p>","DOI":"10.1007\/s00165-021-00546-3","type":"journal-article","created":{"date-parts":[[2021,5,27]],"date-time":"2021-05-27T17:25:55Z","timestamp":1622136355000},"page":"803-826","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Denotational semantics of channel mobility in UTP-CSP"],"prefix":"10.1145","volume":"33","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8579-3366","authenticated-orcid":false,"given":"Gerard","family":"Ekembe Ngondi","sequence":"first","affiliation":[{"name":"Lero, the SFI Research Centre for Software, Trinity College Dublin, Dublin, Ireland"}]}],"member":"320","reference":[{"key":"e_1_2_1_2_1_2","doi-asserted-by":"crossref","unstructured":"Abrial JR (1984) The mathematical construction of a program. In: Science of computer programming vol 4. Elsevier pp 45\u201386. doi: https:\/\/doi.org\/10.1016\/0167-6423(84)90011-X","DOI":"10.1016\/0167-6423(84)90011-X"},{"key":"e_1_2_1_2_2_2","unstructured":"Bialkiewicz J-A Peschanski F (2009) A denotational study of Mobility. In: Communicating process architectures vol 67. IOS Press pp 239\u2013261. https:\/\/doi.org\/10.3233\/978-1-60750-065-0-239"},{"key":"e_1_2_1_2_3_2","doi-asserted-by":"crossref","unstructured":"Boreale M (1998) On the expressiveness of internal mobility in name-passing calculi. In: Theoretical computer science vol 195. Elsevier pp 205\u2013226. https:\/\/doi.org\/10.1016\/S0304-3975(97)00220-X","DOI":"10.1016\/S0304-3975(97)00220-X"},{"key":"e_1_2_1_2_4_2","unstructured":"Broy M Dederichs F Dendorfer C Fuchs M Gritzner TF Weber R (1993) The design of distributed systems\u2014an introduction to FOCUS (revised) Technical Report University of Munich. citeseer.edu\/broy93.pdf"},{"key":"e_1_2_1_2_5_2","doi-asserted-by":"crossref","unstructured":"Cavalcanti A Woodcock J (2006) A tutorial introduction to CSP in unifying theories of programming. In: Refinement techniques in software engineering Springer. pp 220\u2013268. https:\/\/doi.org\/10.1007\/11889229_6","DOI":"10.1007\/11889229_6"},{"key":"e_1_2_1_2_6_2","doi-asserted-by":"crossref","unstructured":"Ekembe Ngondi G (2016) Unifying theories of mobile channels. In: Proceedings 17th international workshop on refinement EPTCS vol 209. pp 24\u201339. https:\/\/doi.org\/10.4204\/EPTCS.209.3","DOI":"10.4204\/EPTCS.209.3"},{"key":"e_1_2_1_2_7_2","first-page":"114","article-title":"UTP semantics of reactive processes with continuations","volume":"10134","author":"Ekembe Ngondi G","year":"2016","journal-title":"Proceedings of international symposium on UTP, LNCS"},{"key":"e_1_2_1_2_8_2","unstructured":"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"},{"key":"e_1_2_1_2_9_2","first-page":"65","article-title":"Hide and new in the Pi-Calculus","volume":"89","author":"Giunti M","year":"2012","journal-title":"Proceedings of joint workshop on expresiveness\/structure operation semantics, EPTCS"},{"key":"e_1_2_1_2_10_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.685258"},{"key":"e_1_2_1_2_11_2","doi-asserted-by":"crossref","unstructured":"Grosu R Stolen K (1999) Stream based specification of mobile systems. In: Formal aspects of computing vol 13. Springer pp 1\u201331. https:\/\/doi.org\/10.1007\/PL00003937","DOI":"10.1007\/PL00003937"},{"key":"e_1_2_1_2_12_2","first-page":"141","article-title":"A theory of pointers for the UTP","volume":"5160","author":"Harwood W","year":"2008","journal-title":"International colloquium on theoretical aspects of computing, LNCS"},{"key":"e_1_2_1_2_13_2","doi-asserted-by":"publisher","DOI":"10.5555\/3921"},{"key":"e_1_2_1_2_14_2","doi-asserted-by":"crossref","unstructured":"Hoare T He Jifeng (1998) Unifying theories of programming. Prentice-Hall","DOI":"10.1007\/BFb0002714"},{"key":"e_1_2_1_2_15_2","doi-asserted-by":"crossref","unstructured":"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\u201325 Elsevier. https:\/\/doi.org\/10.1016\/j.entcs.2008.04.050","DOI":"10.1016\/j.entcs.2008.04.050"},{"key":"e_1_2_1_2_16_2","doi-asserted-by":"crossref","unstructured":"McEwan A Woodcock J (2010) Unifying theories of interrupts. In: Proceedings of international symposium on UTP LNCS vol 5713. Springer pp 122\u2013141. https:\/\/doi.org\/10.1007\/978-3-642-14521-6_8","DOI":"10.1007\/978-3-642-14521-6_8"},{"volume-title":"Communicating and mobile systems: the pi-calculus","year":"1999","author":"Milner R","key":"e_1_2_1_2_17_2"},{"volume-title":"The theory and practice of concurrency","year":"1998","author":"Roscoe AW","key":"e_1_2_1_2_18_2"},{"key":"e_1_2_1_2_19_2","doi-asserted-by":"crossref","unstructured":"Roscoe AW (2010) Understanding concurrent systems Chap. 20 \u00a720.3. pp 497\u2013506 Prentice-Hall. https:\/\/doi.org\/10.1007\/978-1-84882-258-0","DOI":"10.1007\/978-1-84882-258-0"},{"key":"e_1_2_1_2_20_2","unstructured":"Roscoe AW (2011) On the expressiveness of CSP draft. http:\/\/www.cs.ox.ac.uk\/files\/1383\/expressive.pdf"},{"key":"e_1_2_1_2_21_2","doi-asserted-by":"crossref","unstructured":"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\u2013404. https:\/\/doi.org\/10.1007\/978-1-84882-912-1_16","DOI":"10.1007\/978-1-84882-912-1_16"},{"key":"e_1_2_1_2_22_2","doi-asserted-by":"crossref","unstructured":"Sangiorgi D (1996) \u03c0-calculus Internal mobility and agent-passing Calculi. In: Theoretical computer science vol 167. Elsevier pp 235\u2013274. https:\/\/doi.org\/10.1016\/0304-3975(96)00075-8","DOI":"10.1016\/0304-3975(96)00075-8"},{"key":"e_1_2_1_2_23_2","unstructured":"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"},{"key":"e_1_2_1_2_24_2","doi-asserted-by":"crossref","unstructured":"St\u00f8len K (1999) Specification of dynamic reconfiguration in the context of input\/output relations. In: International conference on FMOODS IFIPAICT vol 10. Springer pp 259\u2013272. https:\/\/doi.org\/10.1007\/978-0-387-35562-7_20","DOI":"10.1007\/978-0-387-35562-7_20"},{"key":"e_1_2_1_2_25_2","unstructured":"Tang X Woodcock J (2004) Towards mobile processes in UTP. In: Proceedings of 2nd international conference SEFM vol 1. IEEE pp 44\u201353. https:\/\/doi.org\/10.1109\/SEFM.2004.10045"},{"key":"e_1_2_1_2_26_2","unstructured":"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"},{"key":"e_1_2_1_2_27_2","doi-asserted-by":"crossref","unstructured":"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\u2013210. https:\/\/doi.org\/10.1007\/11423348_10","DOI":"10.1007\/11423348_10"},{"key":"e_1_2_1_2_28_2","unstructured":"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"},{"key":"e_1_2_1_2_29_2","doi-asserted-by":"crossref","unstructured":"Woodcock J Wellings AJ Cavalcanti A (2015) Mobile CSP. In: Brazilian symposium on formal methods LNCS vol 9526. Springer pp 39\u201355. https:\/\/doi.org\/10.1007\/978-3-319-29473-5_3","DOI":"10.1007\/978-3-319-29473-5_3"}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-021-00546-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00165-021-00546-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00165-021-00546-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1007\/s00165-021-00546-3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,8,31]],"date-time":"2024-08-31T17:46:56Z","timestamp":1725126416000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1007\/s00165-021-00546-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,8]]},"references-count":29,"journal-issue":{"issue":"4-5","published-print":{"date-parts":[[2021,8]]}},"alternative-id":["10.1007\/s00165-021-00546-3"],"URL":"https:\/\/doi.org\/10.1007\/s00165-021-00546-3","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2021,8]]},"assertion":[{"value":"7 February 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"20 February 2021","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"14 March 2021","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"27 May 2021","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}