Verifying ODP trader function by using Event B
Hafid Belhaj · 2010
In order to support interoperability in open distributed systems, an information service is needed that can provide dynamic knowledge about available service providers. Such a service is Trading function, identified by Basic Reference Model of Open Distributed Processing (RM ODP). RM ODP is a joint effort of ISO and ITU−T. Within the standardization of RM ODP, Trading function is developed as a component standard. The use of formal methods in the design process of ODP systems is explicitly required. Currently there are no formal specifications of ODP concepts which are widely accepted. One interesting question concerns the suitability of event B for their use in ODP. In this paper, the use of event B for verifying ODP is investigated and evaluated. The ODP trader is chosen as case of study because it appears as a first main application of ODP.