Coordination in the ImpUNITY framework

Our main interest in this paper is to investigate how we can combine different systems and languages via a shared tuple space. The languages themselves can be for example standard im perative languages. Hence we study a framework, in which we can have both the possibility for communication via a shared tuple space, and more standard imperative programming con structs. The ImpUNITY framework is an extension of the UNITY framework. It contains several program structuring mechanisms and puts special emphasis on compositional refinement of both specifications and programs. It has an associated temporal logic, formal refinement notions, and program transformation rules. In this paper we extend this framework further: we show how coordination in the form of a shared tuple space between communicating ImpUNITY programs is modelled and used during formal program specification and refinement. We exemplify our formalism by a larger case study on a phone system where communication in the system is partly taken care of via a tuple space. Additionally, we bring structure in the tuple space and the state spaces of the local programs, by allowing parts of them to be hidden and making it possible to restrict the access rights of different components to the tuple space.