A formal model of concurrency for distributed object-oriented systems

It is widely accepted that object-oriented constructions can be used as a pertinent basis for the support of distributed systems consisting of concurrently executing objects that communicate and interoperate among them. In this context, distributed object systems are represented from a process-oriented perspective which uses the process as the basic modelling structure. This point of view allows us to model concurrent objects as a collection of interacting processes, each of them describing a pattern of behaviour. We aim to provide a formal foundation for object-oriented constructions. To do so, we present a formal model of concurrent objects based on a well-defined process theory, the π-calculus, which offers a very effective mechanism of specification and verification. The election of the π-calculus is justified by some of its features, e.g., mobility and higher-order constructions, for they will be essential to the description of some object behaviour and constructions