A Formal Specification and Verification of CORBA Standards


The Transactions of the Korea Information Processing Society (1994 ~ 2000), Vol. 5, No. 12, pp. 3127-3137, Dec. 1998
10.3745/KIPSTE.1998.5.12.3127,   PDF Download:

Abstract

The CORBA standard specification is peculiar in that, in addition to the usual description of architecture and functionality of distributed systems, it also specifies in CORBA IDL(Interface Definition Language) the precise application interfaces to be provided by implementation modules to conform to the standard. However, it is necessary to formally specify the behavioral semantics of the interfaces and to formally verify and reason about their properties. A formal specification and verification will ensure the correctness of CORBA specification, and thus will increase our confidence on the standard. We propose a formal specification and verification method for CORBA standard specification. We first specify CORBA standard modules in Larch/CORBA IDL (LCB). a Larch behavioral interface specification language tailored to CORBA IDL. The LCB specifications are translated into LSL(Larch Shared Language), an algebraic specification language, based on the formal semantics of LCB. an actual mathematical verification is accomplished in terms of LSL using its proof logic and support tools. We also provide the semantic foundation of our method and apply it to the CORBA naming service apecification to show its effectiveness and efficiency.


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 Formal Specification and Verification of CORBA Standards," The Transactions of the Korea Information Processing Society (1994 ~ 2000), vol. 5, no. 12, pp. 3127-3137, 1998. DOI: 10.3745/KIPSTE.1998.5.12.3127.

[ACM Style]
Kim Mi Hee. 1998. A Formal Specification and Verification of CORBA Standards. The Transactions of the Korea Information Processing Society (1994 ~ 2000), 5, 12, (1998), 3127-3137. DOI: 10.3745/KIPSTE.1998.5.12.3127.