In: WG6.1 4th International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS 2000): IFIP TC6, pages 371-396. September 2000.
Abstract: CORBA is a standard proposed by the Object Management Group (OMG) that promotes interoperability between distributed object systems. Following the standardization of this object-oriented middleware, the OMG has specified a set of Common Object Services (COS) that are meant to serve as the building blocks of distributed CORBA applications. The COS are specified using CORBA Interface Definition Language (IDL) that describes the syntactic aspects of services supported by remote objects. However, CORBA-IDL does not support specification of the behaviour of objects in an abstract and formal way, and behavioural specification is mostly provided in plain English. To overcome this problem, we have proposed a formal description technique (Cooperative Objects) based on high-level Petri nets, and developed a software support environment. The goal of this paper is to demonstrate that our approach is suited to the formal specification of typical CORBA COS, and presents a Cooper! ative Object model of the CORBA event service, a COS that provides asynchronous, one-to-many communication between objects. The advantages of dealing with a tool-supported, executable formal notation are detailed, as well as the results that can be obtained through Petri net analysis techniques.
Keywords: Distributed systems, behavioural specification, CORBA, high-level Petri nets.