Mobile CSP

J. C. P. Woodcock*, A. L. C. Cavalcanti, A. J. Wellings

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contribution


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 π-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.

Original languageEnglish
Title of host publicationFormal Methods: Foundations and Applications
Subtitle of host publication18th Brazilian Symposium, SBMF 2015, Belo Horizonte, Brazil, September 21-22, 2015, Revised Selected Papers
EditorsMárcio Cornélio, Bill Roscoe
Number of pages17
ISBN (Electronic)978-3-319-29473-5
ISBN (Print)978-3-319-29472-8
Publication statusPublished - 2016
Event18th Brazilian Symposium on Formal Methods: Foundations and Applications, SBMF 2015 - Belo Horizonte, Brazil
Duration: 21 Sept 201522 Sept 2015

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference18th Brazilian Symposium on Formal Methods: Foundations and Applications, SBMF 2015
CityBelo Horizonte

Cite this