icon-situation

Ausgangssituationrodin-handbook

Deploy war ein europäisches FP7 Projekt mit dem Ziel, Techniken und Methoden für die Entwicklung sicherheitskritischer Systeme mittels formaler Methoden voranzutreiben und weiterzuentwickeln.

Ein zentrales Ziel war es, die sogenannte Rodin Platform weiterzuentwickeln und für Anwender aus der Industrie zugänglich zu machen.

icon-challenge

Aufgabe

Rodin war zu Beginn des Deploy Projekts im Jahre 2008 bereits eine ausgereifte Plattform, jedoch lies in dieser Zeit die dazugehörige Dokumentation noch zu wünschen übrig. Neben veralteten und redundanten Informationen waren viele Teile und Funktionen der Plattform noch nicht vollständig dokumentiert. Zudem erschwerten diverse externe Quellen, wie z.B. einzelne PDF Dateien, eine zusammenhängende Suche in der Dokumentation. Weder Industrie- noch akademische Partner des Deploy Projektes waren dazu bereit Ressourcen für diese Aufgabe bereitzustellen.

icon-solution

Lösungskonzept

Formal Mind übernahm daraufhin die Aufgabe an der Umsetzung für ein neues Handbuch für die Rodin Plattform zu arbeiten. Die erste Aufgabe bestand darin, eine sorgfältige Problemanalyse durchzuführen. Das Ergebnis der Analyse war die Umsetzung eines einheitlichen Build Prozesses und die Verwendung einer einzigen zentralen Quelle für das Handbuch. Dabei sollten drei unterschiedliche Formate unterstützt werden: PDF, HTML und ein Eclipse Help Plugin.

Während des gesamten Projekts war die Rodin Community dazu aufgerufen, sich am Projekt zu beteiligen und ihre Wünsche, Kritik und Verbesserungsvorschläge beizusteuern.

Das eigentliche Schreiben des Handbuches wurde in vier Iterationen aufgeteilt, welche jeweils acht Wochen Laufzeit hatten. Dies ermöglichte uns u.a. auf die Rückmeldung der Community zu reagieren und nachfolgende Iterationen dementsprechend anzupassen. Weiterhin wurde in der dritten Iteration ein ausführlicher Nutzertest durchgeführt. Der Test bestand darin, dass Nutzer (mit und ohne Erfahrung) mit Hilfe des Handbuches eine formale Spezifikation in Event-B und Rodin realisieren sollten. Die Ergebnisse wurden in der letzten Iteration berücksichtigt.

icon-result

Ergebnisse

Bei Amazon kaufen

Handbuch als PDF

Handbuch als HTML

Das Ergebnis waren ein Handbuch mit 178 Seiten im PDF Format, eine HTML Version und ein Eclipse Help Plugin, welches mit der Rodin Platform ausgeliefert werden kann. Dabei wurden einige relevante Teile der alten Dokumentation angepasst, um diese im neuen Handbuch wiederzuverwenden. Der größte Teil wurde jedoch neu geschrieben.

Weiterhin wurde ein Continuous Build System auf dem Server der Universität Düsseldorf bereitgestellt. Das System aktualisiert automatisch das Handbuch in den genannten Formaten, sobald neuer Inhalt beigesteuert wurde. Dies ermöglicht eine ständige Verfügbarkeit der neustens und aktualisierten Fassung des Handbuches.

Nicht nur die Stakeholder waren sehr zufrieden mit dem Ergebnis. Durch Automatisierung und einer guten Dokumentation, ist jeder Commiter mit Latex Kenntnissen in der Lage das Handbuch zu pflegen.