| Typing the Behavior of Corba Objects | Objectives | Description |
Spanish-Portuguese Joint Research Programme E15/02, 2002-2003, between
The project aims at a proposal for typing the behavior of CORBA objects. The results will be presented in international conferences and published in scientific journals. We will also design, and perhaps begin to implement, a tool to check the conformance of programs with respect to the new specification of CORBA objects.
Our source are type systems which support the specification and verification of complex interactions between agents in a concurrent system. Examples of such interactions are network communication protocols, client-server protocols, and the correct use of high-level data structures implemented by objects. The target is CORBA, one of the major distributed object platforms. Proposed by the OMG, the Object Management Architecture attempts to define, at a high level of description, the various facilities required for distributed object-oriented computing.
Commercial object and component platforms (such as CORBA, DCOM, or EJB) provide the basic infrastructure for making objects interoperate based on object interfaces. They allow to sort out most of the ``plumbing'' issues when putting heterogeneous components together to build applications, but all parties are starting to recognize that this kind of signature interoperability is not sufficient for ensuring the correct development of component-based applications in open systems. Current IDLs present some limitations when tried to be used in open and independently extensible systems.
We will use "session types", which allow the specification of the dynamic behavior of objects. Sessions are partial protocol specifications, in which we only pay attention to the behavioral interface that a component presents to another one. This allows modular specification of the behavior of the components, providing more than just signature information, and permits precise definitions of compatibility and substitutability tests, and at a lower computational cost than other semantic checks (and hence of practical utility).