Tuple-based models in the observation framework

In this paper, we elaborate on modelling tuple-based coordination media in terms of observable sources providing coordination as a service. Only the medium's part directly affecting its observable behaviour is explicitly represented, while its inner activity is represented only as a source for proactive behaviour, thus abstracting away from its details. As an example of this methodology, we formalise JavaSpaces' time passing and leasing mechanisms, which are both modelled in terms of the medium's inner activity. Then, the formalisation of tuple centres is also shown that emphasises the ability of our approach to deal with the explicit representation of complex coordination services.