The {H}eterogeneous {T}ool {S}et
| Type of publication: | Inproceedings |
| Citation: | MossakowskiEA06 |
| Booktitle: | TACAS 2007 |
| Series: | Lecture Notes in Computer Science |
| Volume: | 4424 |
| Year: | 2007 |
| Pages: | 519-522 |
| 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. |
| Userfields: | pdfurl={http://www.informatik.uni-bremen.de/~till/papers/hets-tacas-toolpaper.pdf}, project={I4-SPIN}, psurl={http://www.informatik.uni-bremen.de/~till/papers/hets-tacas-toolpaper.ps}, status={Reviewed}, |
| Keywords: | proof heterogeneity logic institution prover theorem integration development graph |
| Authors | |
| Editors | |
|
Attachments
|
|
|
|
|
Notes
|
|
|
|
|
|
Topics
|
|
|
|
