Situation
Im Verlauf des europäischen FP7-Projekts Bereitstellung von, Siemens setzte die ProB-Software ein, um zu prüfen, ob es möglich war, ProB zur automatischen Überprüfung von B-Modellen einzusetzen. Diese Modelle wurden bereits in einer Produktionsumgebung verwendet und bezogen sich auf die Gleistopologie und Signaldaten. Zu diesem Zeitpunkt erforderten die fraglichen Eigenschaften Siemens mehrere Wochen zur manuellen Überprüfung (etwa ein Monat Arbeit für einen Mann).
Herausforderung
Die Herausforderung, vor der das STUPS-Team (Softwaretechnik und Programmiersprachen) an der Universität Düsseldorf steht, wird in der Bereitstellung von Deliverable D41. Siemens übermittelte dem STUPS-Team am 8. Juli 2008 die Modelle für die Fallstudie San Juan. Es handelte sich um 23.000 Zeilen B, verteilt auf 79 Dateien, von denen zwei zu analysieren waren: ein einfacheres Modell und ein schweres Modell. STUPS brauchte dann eine Weile, um die Modelle zu verstehen und sie durch den neuen Parser zu bringen, dessen Entwicklung zu diesem Zeitpunkt noch nicht abgeschlossen war.
Lösung
ProB wurde die Möglichkeit, das einfache Modell sofort zu analysieren. Ein Fehler in den Behauptungen wurde entdeckt. Daraufhin wurde ProB so verbessert, dass die Analyse des schwierigen Modells möglich war. Die Verbesserungen, die vorgenommen wurden, waren nicht spezifisch für das fragliche Modell, sondern waren eher allgemeine Verbesserungen, die allen ProB-Benutzern zugute kamen. Die Ergebnisse der Analyse waren schlüssig.
Am 8. Dezember 2008 war das STUPS-Team endlich in der Lage, das komplizierte Modell zu animieren und zu validieren. Dabei wurden vier Fehler festgestellt. Man beachte, dass das STUPS-Team nicht über das Vorhandensein von Fehlern in den Modellen informiert wurde (sie wurden von Siemens nicht einmal angedeutet), und zunächst glaubte STUPS, dass es immer noch einen Fehler in ProB gäbe. Tatsächlich handelte es sich aber um echte Fehler, und zwar genau um die Fehler, die Siemens selbst durch manuelle Prüfung entdeckt hatte.
Ergebnisse
Die Ergebnisse zeigen, dass die ProB ein großer Erfolg war. Anstatt mehrere Wochen zu brauchen um die Eigenschaften zu prüfen manuell, war ProB in der Lage, die Eigenschaften in 4,15 Sekunden und die Behauptungen in 1017,7 Sekunden (ca. 17 Minuten) mit ProB 1.3.0. Die Leistungsoptimierung der ProB-Software wurde fortgesetzt. Die Überprüfung der Behauptungen für das obige Modell dauert nun weniger als eine Minute unter Verwendung der aktuellen Version von ProB.
