| Publication type: |
Article in Proceedings |
| Author: |
Till Mossakowski, Christian Maeder, Klaus Lüttich |
| Editor: |
Orna Grumberg, Michael Huth |
| Title: |
The Heterogeneous Tool Set |
| Book / Collection title: |
TACAS 2007 |
| Volume: |
4424 |
| Page(s): |
519 – 522 |
| Series: |
Lecture Notes in Computer Science |
| Year published: |
2007 |
| Publisher: |
Springer-Verlag Heidelberg |
| 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. |
| PDF Version: |
http://www.informatik.uni-bremen.de/~till/papers/hets-tacas-toolpaper.pdf |
| PostScript Version: |
http://www.informatik.uni-bremen.de/~till/papers/hets-tacas-toolpaper.ps |
| Keywords: |
proof heterogeneity logic institution prover theorem integration development graph |
| Status: |
Reviewed |
| Last updated: |
23. 01. 2007 |
