Anglo-Portuguese Joint Research Programme, Treaty of Windsor B29/05, 2005-2006, between
The goal of the project is to develop of a framework to specify and statically verify multiparty communication protocols. Software systems consist in collections of components assembled together, although possibly written by different people and in different programming languages. These systems may even be distributed and relying in a communication infrastructure to interoperate. The integration of these components poses difficult problems. The protocol that the components should followed on their interaction must be rigorously specified, and formally verified, not only dynamically, but more important, statically. Specifically, we aim at the development of type systems which support the specification and verification of complex interactions between agents in a concurrent and distributed system. Examples of such interactions are network communication protocols, client-server protocols, and the correct use of high-level data structures implemented by objects.
We have been using "session types" to specify the dynamic behaviour of objects. Sessions are partial protocol specifications, in which we only pay attention to the behavioural interface that a component presents to another one. This allows modular specification of the behaviour of components, which we studied in the context of a foundational calculus like the pi-calculus, and in the context of a functional language. We have also studied precise definitions of compatibility and substitutability tests, and at a lower computational cost than other semantic checks (and hence of practical utility). A possible application area are Web Services, wich aim at interoperability between applications available on the web. To define such business interactions, one needs a formal description of the message exchange protocols used by business processes in their interactions. Session types may provide a useful static analyses tool. Our goal now is twofold: (1) To develop further the framework of session type, extending them from dyadic to multiparty interactions. (2) To equip our experimental concurrent functional language with object-oriented constructs, a fundamental technology to programmers.
Anglo-Portuguese Joint Research Programme, Treaty of Windsor B29/02. Project Typed Programming Languages for Communicating Object Systems.