Short version
in 32nd International Colloquium on Automata, Languages and Programming
(ICALP '05),
Lisboa (Portugal), July 11-15, 2005.
Full version
in Information and Computation.
More technical details can be found in
Tech. Rep. 07/2004,
Dip. Informatica, Univ. di Roma "La Sapienza".
We develop the semantic theory of a foundational language for modelling applications over global computers whose interconnection structure can be explicitly manipulated. Together with process distribution, process mobility and remote asynchronous communication through distributed data repositories, the language has primitives for explicitly modelling inter-node connections and for dynamically activating and deactivating them. For the proposed language, we define natural notions of extensional observations and study their closure under operational reductions and/or language contexts to obtain barbed congruence and may testing equivalence. We then focus on barbed congruence and provide an alternative characterisation in terms of a labelled bisimulation. To test practical usability of the semantic theory, we model a system of communicating mobile devices and use the introduced proof techniques to verify one of its key properties.
@InProceedings{DGP:ICALP05,
author = {R. {De Nicola} and D. Gorla and R. Pugliese},
title = {Basic Observables for a Calculus for Global Computing},
editor = {L. Caires et al.},
booktitle = {Proc. of 32nd International Colloquium on Automata, Languages and Programming (ICALP 2005)},
series = {LNCS},
volume = {3580},
pages = {1226--1238},
year = {2005},
publisher = {Springer},
}
@article{DGP:IC07,
author = {R. {De Nicola} and D. Gorla and R. Pugliese},
title = {Basic Observables for a Calculus for Global Computing},
journal = {Information and Computation},
volume = {205},
number = {10},
pages = {1491--1525},
year = {2007},
publisher = {Elsevier},
}