[vc_row][vc_column width=”1/4″][vc_single_image image=”416″ img_size=”150×150″ alignment=”center” css_animation=”appear”][/vc_column][vc_column width=”3/4″][vc_column_text]

Situation

Im Rahmen des europäischen FP7 Projekts Deploy hat Siemens die Software ProB eingesetzt um herauszufinden, ob sie in der Lage ist, automatisch bestehende B-Modelle zu überprüfen. Diese Modelle, die Gleisstrukturen und Signaldaten beschreiben, wurden bereits produktiv eingesetzt. Bei Siemens wurden zum damaligen Zeitpunkt mehrere Wochen darauf verwendet, um bestimmte Eigenschaften des Modells manuell zu überprüfen. Der dazu nötige Aufwand entsprach etwa einem Personenmonat.[/vc_column_text][/vc_column][/vc_row][vc_row][vc_column width=”1/4″][vc_single_image image=”417″ img_size=”150×150″ alignment=”center” css_animation=”appear”][/vc_column][vc_column width=”3/4″][vc_column_text]

Aufgabe

Im Forschungsbericht D41 des Deploy-Projektes ist die Herausforderung beschrieben: Siemens sandte dem STUPS Team an der Heinrich-Heine-Universität Düsseldorf die Modelle der San Juan Fallstudie am 8. Juli 2008 zu. Es handelte sich dabei um 23.000 Zeilen B verteilt auf 79 Dateien. Davon sollten zwei Modelle untersucht werden, ein einfaches und ein kompliziertes. Das STUPS Team benötigte eine Weile um sich in die Modell einzuarbeiten und den neuen Parser, dessen Entwicklung gerade abgeschlossen wurde, so anzupassen, dass sie eingelesen werden konnten.[/vc_column_text][/vc_column][/vc_row][vc_row][vc_column width=”1/4″][vc_single_image image=”418″ img_size=”150×150″ alignment=”center” css_animation=”appear”][/vc_column][vc_column width=”3/4″][vc_column_text]

Lösung

Mittels ProB konnte das einfachere Modell direkt analysiert werden. Dabei entdeckte das Werkzeug, dass eine der getroffenen Annahmen nicht erfüllt wurde. Um auch die Analyse des komplizierten Modells zu ermöglichen, wurde ProB in einigen Punkten verbessert, die letztendlich allen Anwendern zu Gute kommen.

Am 8. Dezember 2008 konnte das kompliziertere Modell schließlich vollständig analysiert werden, wobei vier Fehler entdeckt wurden. Diese Fehler waren dem STUPS-Team vorher nicht bekannt und Siemens hat dem Team auch keinerlei Hinweise darauf gegeben, dass das Modell nicht vollständig korrekt war. Wie es sich herausstellte, waren es genau die Fehler, die auch Siemens im Laufe der manuellen Überprüfung fand.[/vc_column_text][/vc_column][/vc_row][vc_row][vc_column width=”1/4″][vc_single_image image=”419″ img_size=”150×150″ alignment=”center” css_animation=”appear”][/vc_column][vc_column width=”3/4″][vc_column_text]

Ergebnis

Die Anwendung von ProB hat sich als voller Erfolg erwiesen. Mehrere Wochen manueller Analyse erledigte ProB in etwa 17 Minuten (mit der damaligen Version 1.3.0). Die Software wurde seitdem stetig verbessert und sie benötigt in der aktuellen Version mittlerweile weniger als eine Minute, um alle Annahmen zu überprüfen.[/vc_column_text][/vc_column][/vc_row]