Authors:
 Liam O'Reilly (1), Yoshinao Isobe (2), Markus Roggenbach (1)

Affiliations:
 (1) University of Wales Swansea, United Kingdom
 (2) AIST, Tsukuba, Japan

Title:
Integrating Theorem Proving for Processes and Data - A
State-of-the-art Report of an ongoing PhD Project

Abstract:
Distributed applications such as flight booking systems, web services,
electronic payment systems, require parallel processing of data.
Consequently, such systems have concurrent aspects (e.g.
deadlock-freedom) as well as data aspects (e.g. functional
correctness). Often, these aspects depend on each other.

In [1], we designed the language CSP-CASL, which is tailored to the
specification of distributed systems. There, we identified four basic
integration problems, illustrated them by prototypical examples, and
showed that CSP-CASL can cope with them. Here, we develop theorem
proving support for CSP-CASL by translating CSP-CASL specifications
into the input language of the already established tool
CSP-Prover. Part of this translation is carried out by the tool HETS.

At the current state of our project, we focus on the prototypical
examples stated in [1]. As simple as they are, they capture the very
nature of the integration problem between processes and data. It turns
out that a systematic analysis of these specifications leads to a set
of automatically provable theorems. With these theorems available,
reasoning about CSP-CASL specifications becomes as easy as
reasoning with CSP-Prover alone.

[1] M.Roggenbach: CSP-CASL - A New Integration of Process Algebra and
Algebraic Specification, TCS, Volume 354, 2006.