University of Freiburg | Faculty of Applied Sciences | Institute for Computer Science | Computer Networks and Telematics
The tele Research Group
   
Home         Teaching         Research        Tools         Openings        Publications
     
     
     

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.

Articles

  • Formalization and Validation of the General Inter-ORB Protocol (GIOP) Using Promela and SPIN


    M.     Kamel, S. Leue


    Accepted for publication in:


    Software Tools for Technology Transfer, October 1999.


    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.

    Keywords:

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

    Related Links:

  • GIOP Promela model as a tarfile

  • The Promela/SPIN homepage

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

    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)