Specifying Process Algebra in CoCASL

Author
Description
CSP Specification
CCS Specification

Author

Till Mossakowski, Markus Roggenbach, and Lutz Schröder
BISS
Department of Computer Science
University of Bremen
P.O. Box 330440
D-28334 Bremen
roba@informatik.uni-bremen.de
http://www.informatik.uni-bremen.de/~roba

Description

COCASL [6], a recently defined coalgebraic extension of the algebraic specification language CASL [1], allows for modelling systems in terms of inductive datatypes as well as of co-inductive process types. Here, we demonstrate how to specify process algebras, namely CCS [5] and CSP [4, 9], within such an algebraic-co-algebraic framework. It turns out that COCASL can deal with the fundamental concepts of process algebra in a natural way: The type system of communications, the syntax of processes and their structured operational semantics fit well in the algebraic world of CASL, while the additional coalgebraic constructs of COCASL cover the various process equivalences (bisimulation, weak bisimulation, observational congruence, and trace equivalence) and provide fully abstract semantic domains.

Among the various frameworks for the description and modelling of reactive systems, process algebra plays a prominent role. It has proven to be suitable at the level of requirement specification, for formal refinement proofs as well as for writing design specifications. Looking for the underlying concepts of process algebra, nearly all of them can be found in languages like CCS [5] and CSP [4, 9]: a type system on the communications describing which communications synchronize; synchronous as well as asynchronous communication; operational semantics; and also various notions of process equivalence like strong and weak bisimulation, observation congruence, and trace equivalence. Thus, proposing a new framework which aims at the specification of reactive systems, it is worthwhile to study if these process algebras and their semantic concepts are covered.

COCASL [6], a recently defined coalgebraic extension of the algebraic specification language CASL [1], allows for modelling systems in terms of inductive datatypes as well as of co-inductive process types. Here, the language CASL provides a many sorted first order logic with partial functions and subsorting, and also features sort generation constraints for generated and free datatypes. Furtheron, CASL allows for initial semantics in terms of a structured free construct. COCASL extends this language by a basic co-datatype construct, cogeneratedness constraints, and structured cofree specifications; moreover, coalgebraic modal logic is introduced as syntactical sugar.

The idea behind the design of COCASL is to obtain a fruitful synergy of algebraic and coalgebraic system modelling. Specifying the process algebras CCS and CSP provides an extensive case study in this language. Thus, besides being a proof of concept for COCASL, these specifications demonstrate how to integrate different system aspects within one framework. CASL as the algebraic sub-language of COCASL will deal with the syntactic aspects and the operational semantics of these process algebras, while the equivalence relations on processes like bisimulation, which have been shown to be of coalgebraic nature [2, 10, 7], will be modelled with the coalgebraic constructs provided by COCASL. The full specifications are available at [8].

References:

[1] CASL The COFI Algebraic Specification Language Summary, version 1.0.1. Documents/CASL/Summary, in [3], March 2001.

[2] Peter Aczel and Nax Mendler. A final coalgebra theorem. In Category Theory and Computer Science, number 389 in Lecture Notes in Computer Science, pages 357 365. Springer, 1989.

[3] CoFI. The Common Framework Initiative, electronic archives. Notes and documents accessible from http://www.cofi.info.

[4] Charles Antony Richard Hoare. Communicating Sequential Processes. Prentice Hall, 1985.

[5] Robin Milner. Communication and Concurrency. Prentice Hall, 1989.

[6] Till Mossakowski, Horst Reichel, Markus Roggenbach, and Lutz Schröder. Algebraic-co-algebraic specification in CoCASL. presented at WADT 02, submitted for publication.

[7] Markus Roggenbach and Mila Majster-Cederbaum. Towards a unified view of bisimulation: a comparative study. Theoretical Computer Science, 238:81 130, 2000.

[8] Markus Roggenbach, Till Mossakowski, and Lutz Schröder. Specifications of CCS and CSP in Co- CASL. available at http://www.pst.informatik.uni-muenchen.de/~baumeist/CoFI/case.html.

[9] A.W. Roscoe. The theory and practice of concurrency. Prentice Hall, 1998.

[10] J. J. M. M. Rutten. Universal coalgebra: A theory of systems. Theoretical Computer Science, 249(1):3 80, 2000.

CSP Specification

CCS Specification


On to Executable Specification of an Interpreter Part of CASL Case Studies
Hubert Baumeister
December 22, 2006