Formalization of discovery and communication mechanisms of Tuple Space based Mobile Middleware for underlying unreliable infrastructure

Tuple Space based Mobile Middleware (TSMM), with tuple space as its coordination medium, provides decoupled coordination of different agents of its supported applications over mobile, dynamic and unreliable networks, like Infrastructure Basic Service Set (iBSS). TSMM includes its own discovery and communication mechanisms to achieve robustness and flexibility in such networks. This paper suggests an approach for formalizing these discovery and communication mechanisms of TSMM, in order to appropriately analyze robustness and flexibility of TSMM in presence of underlying unreliability. Formalization is carried out using Mobile UNITY.