CORBA is a standard proposed by the Object Management Group (OMG) in order to promote interoperability between distributed object systems. CORBA provides a programming-language neutral Interface Definition Language (IDL) that describes the syntactic aspects of services supported by remote objects. However, CORBA IDL does not provide any means to specify the behaviour of objects in an abstract and formal way. Behaviour specification is provided either in plain English, or directly in the programming language chosen for the implementation. We propose the use of Cooperative Objects, a dialect of object-structured high-level Petri nets, as formalism for behavioural specification of CORBA systems. We detail at the syntactic and semantic level how this formalism supports the features of the CORBA object model. We present a realistic case study to demonstrate our approach.