This compendium presents articles on case studies in the modeling of
distributed, object-oriented systems, using various modeling languages
and tools. We also make the source code for the presented models available,
M. Kamel, S. Leue
Accepted for publication in:
Software Tools for Technology Transfer, October 1999.
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.
Distributed Systems, CORBA, General Inter-ORB Protocol (GIOP), Middleware, Protocol Specification and Validation, Model Checking, Promela, Spin, Temporal Logic, Specification Patterns
SunSoft: Inter-ORB Engine (Version 1.4, 1997, contains GIOP implementation code)
Download: PostScript version
(A preliminary version of this paper appeared as Technical Report CWC03, Centre for Wireless Communication, University of Waterloo, Waterloo, Ontario, Canada, November 18, 1998)