A Pi-Calculus Based Approach to Software Composition

Present-day applications are increasingly required to be flexible, or "open" in a variety of ways. By flexibility we mean that these applications have to be portable (to different hardware and software platforms), interoperable (with other applications), extendible (to new functionality), configurable (to individual users' or clients' needs), and maintainable. These kinds of flexibility are currently best supported by component-oriented software technology: components, by means of abstraction, support portability, interoperability, and maintainability. Extendibility and configurability are supported by different forms of binding technology, or "glue": application parts, or even whole applications can be created by composing software components; applications stay flexible by allowing components to be replaced or reconfigured, possibly at runtime. This thesis develops a formal language for software composition that is based on the Pi-calculus. More precisely, we present the L-calculus, a variant of the Pi-calculus in which agents communicate by passing extensible, labeled records, or so-called "forms", rather than tuples. This approach makes it much easier to model compositional abstractions than it is possible in the plain Pi-calculus, since the contents of communication are now independent of position, agents are more naturally polymorphic since communication forms can be easily extended, and environmental arguments can be passed implicitly. The L-calculus is developed in three stages: (i) we analyse whether the Pi-calculus is suitable to model composition abstractions, (ii) driven by the insights we got using the Pi-calculus, we de ne a new calculus that has better support for software composition (e.g., provides support for inherently extensible software construction), and (iii), we de ne a first-order type system with subtype polymorphism and sound record concatenation that allows us to check statically an agent system in order to prevent the occurrences of run-time errors. We conclude with defining a first Java-based composition system and Piccola, a prototype composition language based on the L-calculus. The composition system provides support for integrating arbitrary compositional abstractions using both Piccola and standard bridging technologies like RMI and CORBA. Furthermore, the composition systems maintains a composition library that provides components in a uniform way