COORDINATION IN THE IMPUNITY FRAMEWORK

Our main interest in this paper is to investigate how we can combine d ifferent systems and languages via a shared tuple space. The languages themselves can be for example standard imperative languages. Hence we study a framework, in which we can have both the possibility for comm unication via a shared tuple space, and more standard imperative progr amming constructs. The ImpUNITY framework is an extension of the UNITY framework. It contains several program structuring mechanisms and put s special emphasis on compositional refinement of both specifications and programs. It has an associated temporal logic, formal refinement n otions, and program transformation rules. In this paper we extend this framework further: we show how coordination in the farm of a shared t uple space between communicating ImpUNITY programs is modelled and use d during formal program specification and refinement. We exemplify our formalism by a larger case study on a phone system where communicatio n in the system is partly taken care of via a tuple space. Additionall y, we bring structure in the tuple space and the state spaces of the l ocal programs, by allowing parts of them to be hidden and making it po ssible to restrict the access rights of different components to the tu ple space. (C) 1998 Elsevier Science B.V. All rights reserved.