Treaty of Windsor Anglo-Portuguese Joint Research Programme, 2008-2009, between

• Imperial College London, Department of Computing, Nobuko Yoshida
• Queen Mary University of London, Department of Computer Science, Kohei Honda
• University of Lisbon, Department of Informatics, Vasco T. Vasconcelos and Francisco Martins

The growth of web services as an approach to the design and implementation of distributed software systems has led to a number of challenges associated with the development of safe, secure and robust distributed communication-centric applications. Our central aim, addressing these challenges, is to develop the language designs and the type theory for communication-centric software based on the mathematical theories of the mobile processes. Specifically, our objectives are to develop communication-based computational models and their type systems which can validate safety of complex communication protocols between business processes; and to apply the foundation theory to design the key components for web service description languages, focussing on static type checking and advanced protocol validations such as deadlock freedom. This proposal stems from independent but closely related research carried out by the partners in past ten years. The UK partners are working as the official members of W3C Web Services Choreography Description Language Working Group. The time has come to extend our theory, contribute the standardisation and apply it to a real web-description language. This project will build the theories of communication-based systems and transfer them to the arena of web services, in order to provide a foundation for software development techniques to support successful web service programming.

Our first aim is to develop a new computational model and its typing system based on the theory of session types which the partners have initiated, and have been actively studied by the partners and other researchers over the world, not limited in mobile processes but also other computational models and the programming languages. In particular, session types are used as a typing system for WS-CDL. As the first step, we investigate a new session typing system for mobile processes, based on asynchronous communication, to gain the efficiency of message passing. This will overcome the shortcoming of the previous works where consecutive messages are inefficiently blocked due to synchronous nature of communication. We then transfer the established theory to an industrial standardisation language (WS-CDL), where we design key components of an integrated verification environment for web service development and a theoretical framework for a correct implementation of business protocols. In particular, the asynchronous typing system is integrated into WS-CDL and its implementation written in an object-oriented language. Finally we extend to our base type theory to handle more advanced safety properties such as deadlock-freedom and livelock-freedom based on the type theory of the mobile processes.