CSP-CASL - A new Integration of Process Algebra and Algebraic Specification

Markus Roggenbach


CSP-CASL is a combination of the process algebra CSP and the algebraic specification language CASL following the paradigm `integrating a formalism for the concurrent aspects with algebraic specification of the static datatypes'. Its novel aspects are:

1. A process algebra is combined with the concept of loose specifications on the algebraic side. Thus, CSP-CASL is able to deal with data refinement/abstraction by restricting/extending the model class. Furthermore, CSP-CASL can express communication patterns depending on abstract data requirements.
2. CSP-CASL has a two-step semantics. This gives rise to a notion of refinement which can be decomposed in terms of the respective refinements in CASL and CSP.
3. Choosing a denotational semantics for CSP enables theorem proving for CSP.

The last two points aim for the reuse of HOL-CSP and HOL-CASL as components for theorem proving support of CSP-CASL refinement.

A CSP-CASL specification consists of a data part, which is essentially a structured CASL specification, and a process part, which consists of a (recursive) CSP process, where CASL terms are used to describe communications. As usual, the concept of communication via channels is added as `syntactic sugar': an optional channel part allows declaring (typed) channels. These declarations are translated into CASL datatypes, which provide the extra syntax needed for the CSP operations like sending or receiving data on a channel.

The above described structure of a CSP-CASL specification is reflected by its two-step semantics: The first step determines a class of models for the data part by the standard CASL semantics. The second fixes one of the obtained models, additionally fixes one of the denotational semantics of CSP and gives a meaning to the process part. Here, all CASL terms, sorts, ... occuring in the process part are interpreted according to the fixed model of the data part. The second step is generic in the various denotational CSP semantics. The semantics of a whole CSP-CASL specification is the family of all these interpretations.

A crucial point of the CSP-CASL semantics is how to define the communication alphabet for the CSP semantics relative to a given CASL model. While a CASL model provides a carrier set for each sort, the CSP semantics expects all communications to be collected in one set. As a first approximation CSP-CASL takes the disjoint sum of all carrier sets as communication alphabet. Preserving the typing leads to identical process behavior for isomorphic CASL models. To model CASL subsorting, an equivalence relation is defined on this disjoint sum. The technical problem here is that CASL equations fail to be transitive at the syntactical level. Finally, to deal with partiality a (typed) communication `undefined' is added: thus, definedness of communications is not treated as an external `well-formedness' condition but can be proven within CSP-CASL.

The integration of CSP and CASL also provides interesting insights into both languages. Following the guideline that all kind of data arising in a CSP-CASL specification should be describable within CASL, CSP's replicated operators like
||_{i=1}^n P(i)

are out of scope: CASL does not provide dependent types. In order to obtain `full CSP' in CSP-CASL, a CASL extension would be necessary. Another point is that loose CASL specifications naturally lead to infinite carrier sets. Thus, CSP hiding might give rise to a non-wellformed CSP-CASL specification as the choosen underlying CSP semantics such as the failures/divergences model deals only with finitely nondeterministic CSP.
Tuesday 11th February 2003, 14:00
Robert Recorde Room
Department of Computer Science