Basic Observables for a Calculus for Global Computing

We discuss a basic process calculus useful for modelling applications over global comput-ing systems and present the associated semantic theories as determined by some basic notions of observation. The main features of the calculus are explicit distribution, remote operations, process mobility and asynchronous communication through distributed data spaces. We intro-duce some natural notions of extensional observations and study their closure under operational reductions and/or language contexts to obtain barbed congruence and may testing. For these equivalences, we provide alternative tractable characterizations as labelled bisimulation and trace equivalence. We discuss some of the induced equational laws and relate them to design choices of the calculus. In particular, we show that some of these laws do not hold any longer if the language is rendered less abstract by introducing (asynchronous and undetectable) fail-ures or by implementing remote communications via process migrations and local exchanges. In both cases, we also investigate the adaptation of the tractable characterizations of barbed congruence and may testing to the lower-level scenarios