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, where possible.
Publications
-
M. Kamel and S.Leue: Formalization and Validation of the General Inter-ORB Protocol (GIOP) using Promela and Spin,
Volume 2, Pages 394-409, International Journal on Software Tools for Technology Transfer, 2000.
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.
Download: [PDF] [PS]
GIOP Promela
- Modified GIOP Promela model as a zip-file
Note: we have replaced the variables named "pid" in the original model with variables named "prid" to accommodate changes in the SPIN parser. These are the only changes made. It is recommended to use this collection of the GIOP Promela files. - Original GIOP Promela model as tarfile
Note: these models use a variable named "pid" which the current SPIN parser does not allow.
Related Links
- The Promela/SPIN homepage
- Promela Models / Promela Database (maintained by Alberto Lluch Lafuente)
- 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)
Keywords
Distributed Systems, CORBA, General Inter-ORB Protocol (GIOP), Middleware, Protocol Specification and Validation, Model Checking, Promela, Spin, Temporal Logic, Specification Patterns.