By the same authors

Mobile CSP

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

Published copy (DOI)

Author(s)

Department/unit(s)

Publication details

Title of host publicationFormal Methods: Foundations and Applications
DatePublished - 2016
Pages39-55
Number of pages17
PublisherSpringer Verlag
EditorsMárcio Cornélio, Bill Roscoe
Original languageEnglish
ISBN (Electronic)978-3-319-29473-5
ISBN (Print)978-3-319-29472-8

Publication series

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

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

Discover related content

Find related publications, people, projects, datasets and more using interactive charts.

View graph of relations