DFG Project MULTIPLE
HetCASL - a heterogeneous specification language
HetCASL is developed wihin the DFG Project MULTIPLE:
Multi-logic systems as a basis for heterogeneous specification and development
Formal methods are important for the development of correct software,
particularly in safe-critical areas. Often, within one software development
project, several different languages and tools are needed. To ensure the
proper interaction of different languages and tools, it is important that
they are semantically related.
The HetCASL environment offers the following:
A (constantly growing) graph of different logics with translations between them.
This graph covers the international standard CASL
(Common algebraic specification language), its restrictions and extensions
(like HasCASL, CspCASL, ModalCASL),
but also completely different languages (and even programming languages
The heterogeneous specification language HetCASL that
allows to combine specifications written in different logics. HetCASL
is parameterized over an arbitrary but fixed logic graph,
like the one above.
HetCASL comes with a formal semantics and a proof calculus,
the latter is subject of ongoing research.
HetCASL Language Summary.
The Heterogeneous tool set (Hets),
that can parse and statically analyse HetCASL, based on
parsers and static analysers for the individual logics
of the logic graph.
HetCASL specifications are transformed into so-called
development graphs, which are the basis for
heterogeneous theorem proving.