| Art der Veröffentlichung: |
Artikel in Sammlung |
| Autor: |
Till Mossakowski, Christian Maeder, Klaus Lüttich |
| Herausgeber: |
Bernhard Beckert |
| Titel: |
The {H}eterogeneous {T}ool {S}et |
| Buch / Sammlungs-Titel: |
VERIFY 2007, 4th International Verification Workshop |
| Band: |
259 |
| Seite(n): |
119 – 135 |
| Serie / Reihe: |
CEUR Workshop Proceedings |
| Erscheinungsjahr: |
2007 |
| Abstract / Kurzbeschreibung: |
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
specifications, 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.
We illustrate the approach with a sample heterogeneous proof
proving the correctness of the composition table of a qualitative
spatial calculus. The proof involves two different provers and
logics: an automated first-order prover solving the vast majority of
the goals, and an interactive higher-order prover used to prove a few
bridge lemmas.
|
| Internet: |
http://CEUR-WS.org/Vol-259 |
| PDF Version: |
http://sunsite.informatik.rwth-aachen.de/Publications/CEUR-WS/Vol-259/paper11.pdf |
| Schlagworte: |
heterogeneous theorem proving tools logic proofs |
| Status: |
Reviewed |
| Letzte Aktualisierung: |
08. 01. 2008 |
