Heterogeneous specification in HetCASL
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 like Haskell).
-
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. pdf ps - 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.
Links:
- HetCASL Language Summary. pdf ps
- Heterogeneous tool set (Hets), a parsing, analysis and proof tool for heterogeneous specifications
- Publications
-
MULTIPLE grant proposal (unfortunately in German only) as ps
and as pdf.
Author: Dr. Till Mossakowski
| Last updated: February 3, 2006 |  |