Verifying ODP trader function by using Event B
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.
Keywords: RM-ODP, Trader function, event B, RODIN
platform
Download Full-Text
