The Heterogeneous Tool Set, Hets

Heterogeneous specification becomes more and more important because complex systems are often specified using multiple viewpoints, involving multiple formalisms (see Fig. 1). Moreover, a formal software development process may lead to a change of formalism during the development.

Some of the current heterogeneous approaches deliberately stay informal, like UML. Current formal integration approaches have the drawback that they are uni-lateral in the sense that typically there is one logic (and one theorem prover) which serves as the central integration device, even if this central logic may not be needed or desired in particular applications.

By contrast, the heterogeneous tool set is a both flexible,multi-lateral and formal (i.e. based on a mathematical semantics) integration tool, providing parsing, static analysis and proof management for heterogeneous multi-logic specifications by combining various tools for individual specification languages. Unlike other tools, it treats logic translations (e.g. codings between logics) as first-class citizens. The architecture of the heterogeneous tool set is shown in Fig. 2. In the sequel, we will explain the details of this figure.