Formal specification of CORBA services: experience and lessons learned

ABSTRACT

CORBA is now established as one of the main contenders in object-oriented middleware. Beyond the definition of this standard for distributed object systems, the Object Management Group (OMG) has specified several object services (Common Object Services, COS) that should foster the interoperability of distributed applications. Based on experiment, the goal of this paper is to show that the OMG's style of specification of the CORBA services is not suited to guarantee that implementers will produce interoperable and substitutable implementations. To illustrate our point, we give an account of an experiment based upon the formal specification of one COS, namely the CORBA Event Service. This formal specification highlights several ambiguities and under-specifications in the OMG document. We then test several commercial and public domain implementations of the CORBA Event Service, in order to assess how the implementers have dealt with these under-specifications. We show that the choices made by the implementers lead to incompatible implementations. We finally suggest a solution to overcome the problem of specification of object services, which satisfies the views of both implementers and users. Specifically, we suggest that the specification of such services be made using a formal description technique, and that implementers be provided with test cases derived from the formal specification.

REFERENCES

• 1: Barbey, Stephane, Buchs, Didier and Peraire, Cecile. "Overview and Theory for Unit Testing of Object-Oriented Software." Tagungsband "Qualit~tsmanagement Der Objektorientierten Software-Entwicklung", Basel, Switzerland. (1996) 73-112.
• 2: Stéphane Barbey , Didier Buchs , Cécile Péraire, A Theory of Specification-Based Testing for Object-Oriented Software, Proceedings of the Second European Dependable Computing Conference on Dependable Computing, p.303-320, October 02-04, 1996
• 3: Bastide, Remi. "Objets Cooperatifs : Un Formalisme Pour La Modelisation Des Systemes Concurrents." Ph.D. thesis, Universite Toulouse III (1992).
• 4: Rémi Bastide , Ousmane Sy , David Navarre , Philippe Palanque, A formal specification of the CORBA event service, Fourth International Conference on Formal methods for open object-based distributed systems IV, p.371-395, September 2000, Stanford, California, United States
• 5: Rémi Bastide , Ousmane Sy , Philippe A. Palanque, Formal Specification and Prototyping of CORBA Systems, Proceedings of the 13th European Conference on Object-Oriented Programming, p.474-494, June 14-18, 1999
• 6: Rémi Bastide , Ousmane Sy , Philippe Palanque, Formal Support for the Engineering of CORBA-based Distributed Object Systems, Proceedings of the International Symposium on Distributed Objects and Applications, p.264, September 05-07, 1999
• 7: Diagne, Alioune. "Une Approche Multi-Formalismes De Specification De Systemes Repartis: Transformation De Composants Modulaires En Reseaux De Petri." Universite Paris 6 (1997).
• 8: Diagne, Alioune, and Estraillier, Pascal. "Formal Specification and Design of Distributed Systems." IFIP TC6/WG6.1 First International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS'96), Paris, France. Elie Najm, and Jean-Bernard Stefani. Chapman & Hall, UK (1997)
• 9: EisenHauer, Greg, Bodhi Mukherjee, and Chris Codella. On the Implementation of CORBA Event Channels IBM T.J. Watson Research Center (1997).
• 10: Mauro Gaspari , Gianluigi Zavattaro, Process Algebraic Specification of the New Asynchronous CORBA Messaging Service, Proceedings of the 13th European Conference on Object-Oriented Programming, p.495-518, June 14-18, 1999
• 11: Marie-Claude Gaudel, Testing Can Be Formal, Too, Proceedings of the 6th International Joint Conference CAAP/FASE on Theory and Practice of Software Development, p.82-96, May 22-26, 1995
• 12: David Harel , Eran Gery, Executable Object Modeling with Statecharts, Computer, v.30 n.7, p.31-42, July 1997 [doi>10.1109/2.596624]
• 13: Timothy H. Harrison , David L. Levine , Douglas C. Schmidt, The design and performance of a real-time CORBA event service, Proceedings of the 12th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.184-200, October 05-09, 1997, Atlanta, Georgia, United States
• 14: James, P. R., and Gaudel, Marie-Claude. "Testing Algebraic Data Types and Processes: a Unifying Theory." Formal Aspects of Computing 10, no. Special issue. Best papers of FMICS98 (1999) 436-51.
• 15: William Harvey , Haim Kilov, Object-Oriented Behavioral Specifications, Kluwer Academic Publishers, Norwell, MA, 1996
• 16: Jan Kleindienst , František Plášil , Petr Tůma, Lessons learned from implementing the CORBA persistent object service, Proceedings of the 11th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, p.150-167, October 06-10, 1996, San Jose, California, United States
• 17: Charles Lakos , Søren Christensen, A General Systematic Approach to Arc Extensions for Coloured Petri Nets, Proceedings of the 15th International Conference on Application and Theory of Petri Nets, p.338-357, June 20-24, 1994
• 18: Barbara H. Liskov , Jeannette M. Wing, A behavioral notion of subtyping, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.6, p.1811-1841, Nov. 1994 [doi>10.1145/197320.197383]
• 19: Object Management Group. The Common Object Request Broker: Architecture and Specification. CORBA IIOP 2.2 /98-02-01, Framingham, MA (1998).
• 20: ____. Common Object Services Specification /98-07-05, Framingham, MA (1998).
• 21: ____. Notification Service. Orbos/, Framingham, MA (1998).
• 22: Pickin, S, Sanchez, C., Yelmo, J.-C., Gil, J.-J. and Rodriguez, E. "Introducing Formal Notations in the Development of Object-Based Distributed Systems." IFIP TC6/WG6.1 First International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS'96), Paris, France. Chapman & Hall, UK (1997)
• 23: Prinz, Andreas. "Describing Behaviour in Interfaces.", Paris, France. Elie Najm, and Jean-Bernard Stefani. Chapman & Hall, UK (1997)
• 24: Puntigam, Franz. "Types for Active Objects Based on Trace Semantics." Formal Methods for Open Object-Based Distributed Systems. Elie Najm, and Jean-Bernard Stefani, editors. Chapman & Hall (1997) 4-19.
• 25: Rational Software Corporation. UML Semantics. 1.1 ed.1997.
• 26: Schmidt, Douglas C., and Vinoski, Steve. "The OMG Events Service." SIGS C++ Report 9, no. 2 (1997)
• 27: Schmidt, Douglas C., and Vinoski, Steve. "Overcoming Drawbacks in the OMG Events Service." SIGS C++ Report 9, no. 6 (1997)
• 28: Christophe Sibertin-Blanc, Cooperative Nets, Proceedings of the 15th International Conference on Application and Theory of Petri Nets, p.471-490, June 20-24, 1994
• 29: Wil M. P. van der Aalst , Twan Basten, Life-Cycle Inheritance: A Petri-Net-Based Approach, Proceedings of the 18th International Conference on Application and Theory of Petri Nets, p.62-81, June 23-27, 1997

INDEX TERMS

Primary Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.5 Object-oriented Programming

          Nouns: CORBA

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.2 Design Tools and Techniques
          Subjects: Petri nets

General Terms:
Design, Measurement, Performance, Standardization, Theory

Keywords:
CORBA, behavioral specification, distributed systems, high-level Petri nets