CSP-CASL—A new integration of process algebra and algebraic specification

CSP–CASL integrates the process algebra CSP [T. Hoare, Communicating Sequential Processes, Prentice-Hall, Englewood cliffs, NJ, 1985; A.W. Roscoe, The Theory and Practice of Concurrency, Prentice-Hall, Englewood cliffs, NJ, 1998] with the algebraic specification language CASL [P.D. Mosses (Ed.), CASL Reference Manual, Lecture Notes in Computer Science, Vol. 2960, Springer, Berlin, 2004; E. Astesiano, M. Bidoit, B. Krieg-Brückner, H. Kirchner, P.D. Mosses, D. Sannella, A. Tarlecki, CASL—the common algebraic specification language, Theoret. Comput. Sci. 286 (2002) 153–196]. Its novel aspects include the combination of denotational semantics in the process part and, in particular, loose semantics for the data types covering both concepts of partiality and sub-sorting. Technically, this integration involves the development of a new so-called data-logic formulated as an institution. This data-logic serves as a link between the institution underlying CASL and the alphabet of communications necessary for the CSP semantics. Besides being generic in the various denotational CSP semantics, this construction leads also to an appropriate notion of refinement with clear relations to both data refinement in CASL and process refinement in CSP.