EPSRC Project `Data and Processes'

Project Team

Principal Investigator

Dr Markus Roggenbach

Team members

Mr Andy Gimblett Tool support for CSP-CASL, MPhil, part time
To be appointed, PhD, full time
To be appointed, MPhil, full time

Former team member

Mr Lim Beng Chuan: Hardware in the Loop testing for ep2 (MSc project)

Research Partners

Academic Partners

Prof Magne Haveraaen, Bergen University, Norway
Dr Yoshi Isobe, National Institute of Advanced Industrial Science and Technology (AIST), Japan
Dr Till Mossakowski, Bremen University, Germany
Prof Holger Schlingloff, Humboldt-University Berlin and Fraunhofer Institut FIRST, Germany
Besides the EPSRC funding of this cooperation, there is a Socrates Erasmus exchange programme in place that includes post-grad student mobility as well as teaching staff mobility.

Industrial Partners

Zühlke Engineering AG, Zurich, Switzerland
c.a.r.u.s., Hamburg, Germany

The project 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. We 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:

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.
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.
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.
To set up a testing approach that relates the formal specifications in CSP-CASL with real world systems such as an ep2 terminal.
To graduate an MPhil and a PhD candidate.

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

Relevant Publications

M.Roggenbach: CSP-CASL - A New Integration of Process Algebra and Algebraic Specification.
To appear in TCS.
A.Gimblett, M.Roggenbach, H.Schlingloff: Towards a Formal Specification of an Electronic Payment System in CSP-CASL.
In J.L.Fiadeiro, P.Mosses, F.Orejas (eds): Recent Trends in Algebraic Development Techniques, 17th International Workshop, WADT 2004, Barcelona, Spain, March 27-30, 2004, Revised Selected Papers, LNCS 3423, pp. 61-78, Springer 2005.
Y.Isobe, M.Roggenbach: A generic theorem prover of CSP refinement.
In: Proceedings of TACAS 2005, LNCS 3440, Springer 2005.
Y.Isobe, M.Roggenbach, S.Gruner: Extending CSP-Prover by deadlock-analysis: Towards the verification of systolic arrays .
FOSE'05, Japanese Lecture Notes Series, 2005.
C.Lüth, M.Roggenbach, L.Schröder: CCC - The CASL Consistency Checker.
In J.L.Fiadeiro, P.Mosses, F.Orejas (eds): Recent Trends in Algebraic Development Techniques, 17th International Workshop, WADT 2004, Barcelona, Spain, March 27-30, 2004, Revised Selected Papers, LNCS 3423, pp. 94-105 Springer 2005.
P.Mosses (ed) : CASL Reference Manual , LNCS 2960 (IFIP Series), Springer, 2004.
A.W.Roscoe: The Theorie and Practice of Concurrency , Prentice Hall, 1998.
The ep2 Project

Relevant Tools

Research in Algebraic Specification and Processes in Swansea

Mr J Biddle , Mr Gimblett , Dr N A Harman , Mr W Harwood , Mr K Johnson , Prof F G Moller , Prof P Mosses , Dr M Roggenbach , and Prof J Tucker form an active research group on Data and Processes in Swansea that runs the (currently event based)

Swansea Algebraic Specification Seminar

The Swansea computer science department also hosts relevant conferences such as

These activities take place within a strong group on Logic and Algebraic Methods for Design of Software and Hardware. An additional research seminar is devoted to

Proofs, Complexity and Verification

Invited speakers in the regular

Computer Science Colloquia

provide a broader view on Computer Science.

Regular visitors who hold honrary academic positions in the deparment include

Prof J Bergstra, Universities Amsterdam and Utrecht, Netherlands,
Dr K Stevensen, QinetiQ, UK, and
Prof J Zucker, McMaster University, Canada.