A Formalization of OMG Naming Service Specification


The Transactions of the Korea Information Processing Society (1994 ~ 2000), Vol. 5, No. 2, pp. 458-474, Feb. 1998
10.3745/KIPSTE.1998.5.2.458,   PDF Download:

Abstract

To realize the OMG's ultimate goal - a wide reuse and interoperability of software systems, it is necessary to formally specify the software components. Without a formal behavioral interface specification of the components, it is difficult ot determine conformance to the standard and satisfaction of user's requirements. In this paper, we formalize the OMG Naming Service Spercification using the formal specification languages Z and Larch. Firstly is defined in Z a mathematical model for OMG naming service modules are formalized using Larch-style Behavioral Interface Specification Language (BISL) for CORBA IDL, called Larch/CORBA-IDL. Our work establishes a foundation for applying formal methods to standard specification, and shows its benefits, in particular, of behavioral interface specification. It also demonstrates that multiple formalism can be adapted to specify the standards, and Larch is ideally suited to specify the behavioral semantics for objects in distributed systems.


Statistics
Show / Hide Statistics

Statistics (Cumulative Counts from September 1st, 2017)
Multiple requests among the same browser session are counted as one view.
If you mouse over a chart, the values of data points will be shown.


Cite this article
[IEEE Style]
K. M. Hee, "A Formalization of OMG Naming Service Specification," The Transactions of the Korea Information Processing Society (1994 ~ 2000), vol. 5, no. 2, pp. 458-474, 1998. DOI: 10.3745/KIPSTE.1998.5.2.458.

[ACM Style]
Kim Mi Hee. 1998. A Formalization of OMG Naming Service Specification. The Transactions of the Korea Information Processing Society (1994 ~ 2000), 5, 2, (1998), 458-474. DOI: 10.3745/KIPSTE.1998.5.2.458.