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.


  • 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. (PDF)
  • Moataz Kamel and Stefan Leue: Validation of Remote Object Invocation and Object Migration in CORBA GIOP using Promela/Spin, Actes/Proceedings Spin\'98, Ecole Nationale Superieure des Telecommunications, Paris, France, 1998.

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


Distributed Systems, CORBA, General Inter-ORB Protocol (GIOP), Middleware, Protocol Specification and Validation, Model Checking, Promela, Spin, Temporal Logic, Specification Patterns.