A principled exploration of coordination models

Coordination is a style of interaction in which information exchange among independent system components is accomplished by means of high-level constructs designed to enhance the degree of decoupling among participants. A decoupled mode of computation is particularly important in the design of mobile systems which emerge dynamically through the composition of independently developed components meeting under unpredictable circumstances and thrust into achieving purposeful cooperative behaviors. This paper examines a range of coordination models tailored for use in mobile computing and shows that the constructs they provide are reducible to simple schema definitions in Mobile UNITY. Intellectually, this exercise contributes to achieving a better operational-level understanding of the relation among several important classes of models of mobility. Pragmatically, this work demonstrates the immediate applicability of Mobile UNITY to the formal specification of coordination constructs supporting mobile computing. Moreover, the resulting schemas are shown to be helpful in reducing the complexity of the formal verification effort.