Heterogeneous Specification and the Heterogeneous Tool Set
Till Mossakowski · 2004
Formal specification of software systems has become more and more important, especially in safetycritical areas where one cannot take the risk of malfunction. Casl, the Common Algebraic Specification Language, is a standard for axiomatic specification of conventional software; and several extensions of Casl deal with temporal, reactive, higher-order etc. aspects. That is, we are faced with a multitude of specification languages and underlying logics. In this work, we argue that for the specification of large software systems, heterogeneous multilogic specifications are needed, since complex problems have different aspects that are best specified in different logics. A combination of all the used logics would become too complex in many cases. Moreover, 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 often have their strengths in particular aspects. Using heterogeneous specification, these strengths can be combined with comparably small effort. The specification language Casl is an expressive specification language. At the level of basic specifications, it provides first-order logic with induction, powerful datatype constructs, subsorting