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

Hugo-Andrés López-Acosta, Thomas Hildebrandt (Main supervisor)

Research output: Book/ReportPh.D. thesisResearch

58 Downloads (Pure)

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 communicationcentred
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 communicationcentred 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.
Original languageEnglish
Number of pages233
Publication statusPublished - 2012
Externally publishedYes

Keywords

  • Process Calculi
  • Service-Oriented models
  • Specification logics
  • Type systems

Fingerprint

Dive into the research topics of 'Foundations of Communication-Centred Programming: Calculi, Logics & Types'. Together they form a unique fingerprint.

Cite this