Universität Bremen  
  FB 3  
  Group BKB > Research > Formal Methods > Formal specification > Deutsch

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.


Author: Dr. Till Mossakowski
  Group BKB 
Last updated: February 3, 2006   impressum