Author

Description

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