Abstract:
The General Inter-Orb Protocol (GIOP) is a key component of the Common Object Request Broker Architecture (CORBA) specification. We present the formal modeling and validation of the GIOP protocol using the Promela language, Linear Time Temporal Logic (LTL) and the Spin model checker. We validate the Promela model using ten high-level requirements which we elicit from the informal CORBA specification. These requirements are then formalized in LTL and the Spin model checker is used to determine their validity. During the validation process we discovered a few problems in GIOP: a potential transport-layer interface deadlock and problems with the server migration protocol. We also describe how property specification patterns helped us in formalizing the high-level requirements that we have elicited.
Keywords:
Distributed Systems, CORBA, General Inter-ORB Protocol (GIOP), Middleware, Protocol Specification and Validation, Model Checking, Promela, Spin, Temporal Logic, Specification Patterns
Related Links:
- GIOP Promela model as a tarfile
- The Promela/SPIN homepage
- Temporal Logic Specification Patterns
- CORBA GIOP 2.3 specification - Chapter 15: General Inter-ORB Protocol
- SunSoft: Inter-ORB Engine (Version 1.4, 1997, contains GIOP implementation code)
(A preliminary version of this paper appeared as Technical Report CWC03,
Centre for Wireless Communication, University of Waterloo, Waterloo, Ontario,
Canada, November 18, 1998: 
PostScript-File (19 p.))