Swansea University
Computer Science

EPSRC Project EP/D037212/1

Objectives

This research proposal is concerned with the integration of processes and data. To develop distributed computer applications such as flight booking systems, web services, electronic payment systems, it is essential to precisely specify the interaction of their different components. Process algebras such as CSP, CCS, ACP, or the pi-calculus do this for the concurrent aspects, but lack the possibility of modelling data. Algebraic specification languages such as ACT ONE, ACT TWO, the Larch specification language, or CASL can model data but do not support concurrency. Previous approaches to integrate processes and data, such as LOTOS, E-LOTOS, or CSP-M restrict data to initial or concrete data types, which has the shortcoming that data needs to be fixed the moment the modelling is done. The speciality of this proposal is that it considers also loosely specified, abstract data types. This allows one to stepwise develop both processes and data - an approach regularly taken also in industrial settings.

As a framework for our proposal the specification language CSP-CASL has been chosen, which I designed within the international CoFI initiative. I already applied CSP-CASL in an industrial case study, where main parts of ep2, a new international standard for electronic payment systems, were to be formalised. However, while this and other studies indicate that CSP-CASL solves the basic integration problem, further research on semantic foundations, on tool support and especially on testing is required in order to turn a language like CSP-CASL into a practically applicable formalism. Toward this aim our investigation has the following objectives:

  1. To make structuring operations available for building up complex specifications in a compositional way and to investigate how this can lead to modular reasoning on hierarchically organised specifications.
  2. To define and investigate formal refinement notions that are capable of mirroring typical informal refinement relations as are present, e.g., in the natural language description of the ep2 system.
  3. To provide tool support for analysing CSP-CASL specifications, e.g., to prove deadlock freedom, as well as for verifying the formal refinement relations between them. Here we aim especially for a novel combination of theorem proving and model checking.
  4. To set up a testing approach that relates the formal specifications in CSP-CASL with real world systems such as an ep2 terminal.
  5. To graduate an MPhil and a PhD candidate.

For points 1 to 4, the ep2 system will be used to demonstrate and evaluate the results of our investigation of processes and data.