Heterogeneous CASL and the heterogeneous tool set

Till Mossakowski

(Bremen)

For the specification of large software systems, heterogeneous multi-logic specifications are needed, since complex problems have different aspects that are best specified in different logics. True logic combinations (in the sense of fibring, or colimits of logical systems) work well for certain classes of logics. However, the true combination approach reaches its limits when logics involving very different features (like modalities, higher-order polymorphism, and calculi for concurrent systems) shall be combined. In such cases, a true combination of all the used logics will quickly become too complex. Hence, heterogeneous specification provide a weaker form of logic combination (corresponding to weighted colimits), where basically the logics are put side by side, but can interact via logic translations.

Using heterogeneous specifications, different approaches being developed at different sites can be related, i.e. there is a formal interoperability among languages and tools. In many cases, specialized languages and tools have their strengths in particular aspects. Using heterogeneous specification, these strengths can be combined with comparably small effort.

We provide a general semantic framework for heterogeneous specification in Heterogeneoous CASL, as well as a proof calculus and tool support. We show that Grothendieck institutions based on institution comorphisms can serve as the underlying mathematical framework. In particular, we show how to extend the verification semantics given for structured specifications in CASL Reference Manual to the heterogeneous case. This semantics translates a heterogeneous specification into a kernel formalism called development graphs.

The heterogeneous tool set provides tool support for heterogeneous specification. Based on an object-oriented interface for institutions (using type classes in Haskell), it implements the Grothendieck institution and provides a heterogeneous parser, static analysis and proof support for heterogeneous specification. This is based on parsers, static analysers and proof support for the individual institutions, on the above mentioned heterogeneous verification semantics, and on a proof calculus for development graphs over the Grothendieck institution.
Tuesday 20th July 2004, 14:00
Robert Recorde Room
Department of Computer Science