Foundations of Communication-Centred Programming: Calculi, Logic & Types

By Hugo-Andrés López-Acosta,
IT University of Copenhagen,
2012

Abstract

Service and process-oriented systems are relatively new technologies that promise effective business processes and flexible and adaptable enterprise IT systems. The key factor in service systems is the ability to decompose a business process into a distributed system, where each participant implements parts of the functions in a business process, and interactions between participants are performed via message passing. In recent years, service- and process-oriented applications have rapidly become the norm for distributed enterprises and they have led to a number of new programming languages and standards, collectively referred to as communication-centred programming. Despite their adoption, these languages and standards for communication-centred programming are still young and unstable, and not grounded on a solid theoretical foundation.

There are at least two significant dimensions when describing communication- centred programs: First, the global/local views used to describe interactions, and second, the imperative/declarative specifications styles used. With respect to views: a global view considers the system as a whole, describing specifications as sequences of message exchanges among participants, and a local view describes the system as a concurrent composition of processes, implementing each participant in the system. While the global view is what is usually provided as specification, the local view is a necessary step towards a distributed implementation. On specification styles: If processes are defined imperatively, then the control flow is defined explicitly (e.g.: as a flow graph of interactions/commands). In a declarative approach processes are described as a collection of conditions (e.g.: logical formulae) they should fulfil in order to be considered correct. Until now, research in these two dimensions have evolved rather independently from each other.

This dissertation collects works devoted to foundational studies in communication-centred programming. Specifically, the dissertation revolves around process calculi as the main analytical tool for service-oriented systems. Process calculi are formal languages conceived for the description and analysis of concurrent systems, providing a rigorous framework where distributed systems can be accurately analysed, by means of reasoning techniques to verify essential properties of a system. By means of process calculi, we provide formal relations between global and local views, and declarative/imperative specifications. This is achieved by extending previous works on the area with additional information in model specifications, like timing constraints and compensable behaviour. Finally, we provide process specifications with reasoning techniques (specification logics, type systems, simulation techniques) that allow one to verify the behaviour of a service specification with respect to trustworthy properties in the system.

FULL TEXT