Formal Modeling and Validation of Distributed, Object-Oriented Systems

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. (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

• 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.