Modelling QoS bounded parameter negotiation protocol by event-B

The Reference Model of Open Distributed Processing (RM-ODP) was a joint effort by the international standards bodies ISO and ITU-T to develop a coordinating framework for the standardization of open distributed processing (ODP). The model describes an architecture within which support of distribution, interworking, interoperability and portability can be integrated. The RM-ODP framework defines ODP concerns using five viewpoints: enterprise, information, computational, engineering, and technology, ODP functions and transparencies. The specification and implementation of QoS is increasingly important in distributed systems due to the need to address questions of performance. To ensure correct implementation of QoS requirements, statements of QoS need to be introduced early in the design process, and in terms of design we consider the use of the event-B method. The aim of this paper is to construct an event-B models of the protocol of bounded parameter negotiating QoS within the enterprise viewpoint. The purpose of our event-B models is to act as a template via which specific distributed system designs can be constructed.