This paper introduces a formal specification technique for mobile systems based on input/output relations on streams. We consider networks of components communicating asynchronously via unbounded directed channels. Mobility is achieved by allowing the components to communicate channel ports. We distinguish between many-to-many and two variants of point-to-point communication. The communication paradigms are semantically under-pinned by denotational models. The models are formulated in the context of timed nondeterministic data-flow networks and presented in a step-wise fashion. The emphasis is on capturing the special kind of dynamic hiding characterizing mobile systems. We demonstrate the proposed approach in a number of small examples.
Formal Aspects of Computing (FAC), vol. 13(1), pp. 1-31, Springer Verlag, 2001.