Compositional modelling and reasoning in an institution for processes and data

Liam O'Reilly; Till Mossakowski; Markus Roggenbach

In: Till Mossakowski; Hans-Jörg Kreowski (Hrsg.). Recent Trends in Algebraic Development Techniques. International Workshop on Algebraic Development Techniques (WADT-10), 20th, July 1-4, Etelsen, Germany, Pages 251-269, Lecture Notes in Computer Science (LNCS), Vol. 7137, Springer, 2012.


The language CspCASL combines specifications of data and processes. We give an institution based semantics to CspCASL that allows us to re-use the institution independent structuring mechanisms of CASL. Furthermore, we extend CspCASL with a notion of refinement that reconciles the differing philosophies behind the refinement notions for CSP and CASL. We develop a compositional proof calculus for refinement along the CASL structuring mechanisms, and demonstrate that compositional proof techniques along parallel process composition from the context of CSP lifts to structured CspCASL specifications.

Deutsches Forschungszentrum für Künstliche Intelligenz
German Research Center for Artificial Intelligence