CoCasl
CoCasl at work – modelling process algebra. CoCasl, a recently developed coalgebraic extension of the algebraic specification language Casl, 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 [R. Milner, Communication and concurrency. New York etc.: Prentice Hall (1989; Zbl 0683.68008)] and CSP [C. A. R. Hoare, Communicating sequential processes. Englewood Cliffs, New Jersey etc.: Prentice-Hall International (1985; Zbl 0637.68007)], within such an algebraic-coalgebraic 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 structural 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. CoCasl hence becomes a meta-framework for studying the semantics and proof theory of reactive systems.
Keywords for this software
References in zbMATH (referenced in 26 articles , 1 standard article )
Showing results 1 to 20 of 26.
Sorted by year (- Leivant, Daniel M.: Global semantic typing for inductive and coinductive computing (2014)
- Sannella, Donald; Tarlecki, Andrzej: Foundations of algebraic specification and formal software development. (2012)
- Schröder, Lutz; Pattinson, Dirk: Modular algorithms for heterogeneous modal logics via multi-sorted coalgebra (2011)
- Sokolova, Ana: Probabilistic systems coalgebraically: a survey (2011)
- Aiguier, Marc; Longuet, Delphine: Some general results about proof normalization (2010)
- Lucanu, Dorel; Rosu, Grigore; Grigoras, Gheorghe: Regular strategies as proof tactics for CIRC. (2008)
- Schröder, Lutz: Expressivity of coalgebraic modal logic: the limits and beyond (2008)
- Schröder, Lutz: Bootstrapping inductive and coinductive types in HasCASL (2008)
- Fiadeiro, José Luiz (ed.); Schobbens, Pierre-Yves (ed.): Recent trends in algebraic development techniques. 18th international workshop, WADT 2006, La Roche en Ardenne, Belgium, June 1--3, 2006. Revised selected papers. (2007)
- Longuet, Delphine; Aiguier, Marc: Specification-based testing for CoCasl’s modal specifications (2007)
- Padawitz, Peter: Expander2: Program verification between interaction and automation. (2007)
- Schröder, Lutz: Bootstrapping types and cotypes in HasCasl (2007)
- Schröder, Lutz; Mossakowski, Till: Coalgebraic modal logic in CoCasl (2007)
- Hausmann, Daniel; Mossakowski, Till; Schröder, Lutz: A coalgebraic approach to the semantics of the ambient calculus (2006)
- Mossakowski, Till; Schröder, Lutz; Roggenbach, Markus; Reichel, Horst: Algebraic-coalgebraic specification in CoCASL (2006)
- Roggenbach, Markus: CSP-CASL -- a new integration of process algebra and algebraic specification (2006)
- Cerioli, Maura (ed.): Fundamental approaches to software engineering. 8th international conference, FASE 2005, held as part of the joint European conferences on theory and practice of software, ETAPS 2005, Edinburgh, UK, April 4--8, 2005. Proceedings. (2005)
- Hausmann, Daniel; Mossakowski, Till; Schröder, Lutz: Towards a coalgebraic semantics of the ambient calculus (2005)
- Hausmann, Daniel; Mossakowski, Till; Schröder, Lutz: Iterative circular coinduction for CoCasl in Isabelle/HOL (2005)
- Roşu, Grigore: Behavioral abstraction is hiding information (2004)