| Date: | 2018, November 27 |
| Author: | Grimm, Claudius |
| Title: | Entwicklung und Umsetzung einer grafischen Benutzeroberfläche zur Darstellung von Entwicklungsgraphen (Bachelor Thesis Defense) |
Eine wichtige Methode um die Korrektheit eines komplexen sicherheitskritischen Systems garantieren zu können ist formale Verifikation, basierend auf mathematischer Logik. Um jeden Aspekt eines Systems angemessen validieren zu können, wurden verschiede Logiken entwickelt. Durch das Kombinieren dieser verschieden Logiken in einer übergeordneten Logik würde die Spezialität und die damit zusammenhängenden Stärken der einzelnen Logiken verloren gehen. Weiterhin wäre eine solche Metalogik deutlich komplexer als die einzelnen Logiken. Im Gegensatz dazu ermöglichen es heterogene Spezifikationen, diese verschiedenen Logiken in einer Spezifikation zu kombinieren, in dem Übersetzungen zwischen den einzelnen Logiken definiert werden. Damit können die Stärken jeder einzelnen Logik ausnutzt werden und es bleibt die Möglichkeit erhalten, Aussagen über die Gesamtheit des Systems treffen zu können.
Das Heterogene Tool Set (Hets) [Mos05] ermöglicht es, solche heterogene Spezifikation zu lesen und zu verwalten. Zusätzlich hat Hets die Möglichkeit mit Theorembeweisern zu kommunizieren, die eine wichtige Rolle beim Verifizieren eines Systems spielen. Zum Verwalten der Struktur einer Spezifikation, sowie zum Kodieren der Übersetzungen zwischen den Logiken, nutzt Hets eine Graphenstruktur. Diese wird als Entwicklungsgraph bezeichnet.
In dieser Arbeit wird eine Anwendung zum Darstellen von Entwicklungsgraphen vorgestellt, genannt Hets-GUI. Diese bietet die Möglichkeit einen Entwicklungsgraphen in einem hierarchischen und einem force-directed Layout darzustellen. Das Hets-GUI kann unabhängig von Hets ausgeführt werden und ist plattformübergreifend einsetzbar. Beim Erstellen der Anwendung wurde darauf geachtet, dass die Bedienung möglichst intuitiv ist und keine große Einarbeitungszeit notwendig ist.
Die Anwendung basiert auf Electron und kommuniziert mit dem Hets Server über eine REST Schnittstelle. Die Oberfläche der Anwendung basiert auf React und zum Zeichnen der Graphendarstellungen wird D3 verwendet. Damit komplexe Graphen besser überblickt werden können, gibt es die Möglichkeit, einen Teil der Knoten auszublenden und nur die grobe Struktur des Graphen darzustellen.