Formal Modeling and Validation
of Distributed, Object-Oriented Systems
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,
Formalization and Validation of the
General Inter-ORB Protocol (GIOP) Using Promela and SPIN
M. Kamel, S. Leue
Accepted for publication
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.
CORBA, General Inter-ORB Protocol (GIOP), Middleware, Protocol Specification
and Validation, Model Checking, Promela, Spin, Temporal Logic, Specification
Promela model as a tarfile
Logic Specification Patterns
2.3 specification - Chapter
15: General Inter-ORB Protocol
Inter-ORB Engine (Version 1.4, 1997, contains GIOP implementation
(A preliminary version of this paper appeared as Technical Report
CWC03, Centre for Wireless Communication, University of Waterloo,
Waterloo, Ontario, Canada, November 18, 1998)