Verification and correctness of service-oriented systems

Service-oriented computing (SOC) is the paradigm that underlies the infrastructure on which the Digital Economy is being built. It offers the ability for businesses and organisations to operate on a globalised, platform-independent market of services, and for individuals to interact with businesses and organisations in a flexible and seamless way that responds to individual needs.

The specific research that we propose to develop addresses fundamental questions raised by SOC on the computational theory and the methods and techniques that are needed to make this infrastructure reliable. Although research has been funded on global ubiquitous computing in general, and Web services in particular, only very little effort has been directed to two of the distinguishing aspects of SOC as a computational paradigm: the asynchronous nature of the interactions that SOC presupposes (the large majority of models that have been proposed are based on synchronous communication, which prevents the kind of loose coupling that is required for open-world software), and the fact that the configurations of the systems that operate on global computers (like the Internet) are intrinsically dynamic, thus defeating the traditional engineering methods that rely on design-time integration of software applications.

An outcome of the collaborative work to be undertaken during the visit is the formulation of a research plan, and grant proposals through which it could be funded, which would advance the state of the art in verification, correctness and realisability of service-oriented systems in areas that are critical for industry: on the one hand, the support for light coupling through asynchronous communication -- synchronous models are easier to work with but not realistic when it comes to open-world software; on the other hand, the dynamicity of the configurations of the applications that run on global computers -- for example, the OSGi (www.osgi.org) has been pushing for the adoption of service platforms and technology that enable components to dynamically discover each other for collaboration, minimise coupling, and change the composition dynamically.

Given the track record of NASA Ames in developing groundbreaking research with impact in both academia and industry worldwide, especially in the domain of safety and mission-critical systems, the research that is spawned by this visit will be of interest to companies and research groups operating in these areas. One of the objectives of the visit is indeed share case-studies, models or experimental data from different kinds of systems, especially to investigate the applicability of our techniques to classes of systems that we have not yet approached and are relevant for the UK industry, including manufacturing, transport and health.

The research plan and grant proposals that the visit will generate will establish the specific pathways that can lead to the expected impact.