A temporal logic approach in the design of communication mechanism for functionally distributed systems

This work has been developed on the basis of a previous experience made inside a project for a functionally distributed system (Cnet), in which an inter-node communication mechanism was defined in terms of Ada(TM) packages. This paper gives a more general framework for the definition of properties of the communication schemes, showing that a temporal logic approach to the definition of the properties can be used as an aid to the design of the communication mechanisms, and as a unifying tool for describing its integration in a high level language.