The Heterogeneous Tool Set
TACAS 2007, volume 4424 of Lecture Notes in Computer Science, page 519-522. Springer-Verlag Heidelberg, (2007)Abstract
Heterogeneous specification becomes more and more important because
complex systems are often specified using multiple viewpoints,
involving multiple formalisms. Moreover, a formal software development
process may lead to a change of formalism during the development.
However, current research in integrated formal methods only deals
with ad-hoc integrations of different formalisms.
The heterogeneous tool set (Hets) is a parsing, static analysis and
proof management tool combining various such tools for individual
specification languages, thus providing a tool for heterogeneous
multi-logic specification. Hets is based on a graph of logics and
languages (formalized as so-called institutions), their tools, and
their translations. This provides a clean semantics of heterogeneous
specification, as well as a corresponding proof calculus. For proof
management, the calculus of development graphs (known from other
large-scale proof management systems) has been adapted to
heterogeneous specification. Development graphs provide an overview of
the (heterogeneous) specification module hierarchy and the current
proof state, and thus may be used for monitoring the overall
correctness of a heterogeneous development.