TY - GEN
T1 - Mobile CSP
AU - Woodcock, J. C. P.
AU - Cavalcanti, A. L. C.
AU - Wellings, A. J.
PY - 2016
Y1 - 2016
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84958033523&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-29473-5_3
DO - 10.1007/978-3-319-29473-5_3
M3 - Conference contribution
SN - 978-3-319-29472-8
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 39
EP - 55
BT - Formal Methods: Foundations and Applications
A2 - Cornélio, Márcio
A2 - Roscoe, Bill
PB - Springer
T2 - 18th Brazilian Symposium on Formal Methods: Foundations and Applications, SBMF 2015
Y2 - 21 September 2015 through 22 September 2015
ER -