Ein Web-Interface für den ProB Animator
Author
Jens Krüger
Abstract
Formale Methoden, wie die B-Methode eine ist, werden in der heutigen Zeit, in der so gut wie kein hoch entwickelter Industriezweig mehr ohne Software auskommt, immer wichtiger um zuverlässige, wenn möglichst fehlerfreie, Software zu entwickeln. Insbesondere in kritischen Anwendungen, bei denen es um sehr viel Geld oder sogar um Menschenleben geht, können Softwarefehler verheerende Folgen haben. Ein Tool zur Analyse solcher Software ist ProB. ProB ermöglicht es unter anderem Spezifikationen bzw. abstrakte Maschinen auf ihre Funktionalität und auf Fehler hin zu überprüfen und so den Erstellungsprozess zu beschleunigen. Diese Bachelorarbeit befasst sich damit, den ProB Animator als Web-Interface (?My- ProB?) ohne weitere Installationen nutzen zu können. Sei es zum Testen der Software oder für das Zusammenarbeiten mit anderen Entwicklern. Die Wahl für die visuelle Darstellung der Benutzeroberfläche ist das Google Web Toolkit. Hiermit ist möglich MyProB eine interaktive Oberfläche und das Aussehen einer Desktop-Applikation zu verleihen. Wichtig war es einen Weg zu finden, GWT zuverlässig mit dem, in ein Eclipse Plugin integrierten, ProB Kern kommunizieren zu lassen. Hier fiel dieWahl auf Remote Methode Invocation. MyProB liefert, durch den Extension-Point Mechanismus von Eclipse, eine Grundlage für zukünftige Erweiterungen für das Web- Interface des ProB Model Checker. In dieser Arbeit wird auf die Architektur der GWT Anwendung des RMI Clients und Servers und auf deren Implementierungen eingegangen. Zum Verständnis der Hintergründe werden die AJAX Architektur, Eclipse und Remote Procedure Calls anhand von Beispielen erklärt. In der Einleitung finden sich kurze Einführungen in die Funktionweise der B-Methode und des ProB Model-Checker. Diese Arbeit endet mit einem Gesamtüberblick über Architektur und Benutzeroberfläche und es wird ein Ausblick über zukünftige Erweiterungen von MyProB gegeben.