{"id":78,"date":"2015-01-01T08:00:00","date_gmt":"2015-01-01T07:00:00","guid":{"rendered":"https:\/\/www.formalmind.com\/uncategorised\/prob-validation-siemens-sas\/"},"modified":"2022-04-22T12:55:22","modified_gmt":"2022-04-22T10:55:22","slug":"prob-validation-siemens-sas","status":"publish","type":"post","link":"https:\/\/www.formalmind.com\/de\/success-story\/prob-validation-siemens-sas\/","title":{"rendered":"ProB-Validierung f\u00fcr Siemens SAS"},"content":{"rendered":"
\n
\n
<\/div>\n\n\n\n
\n

Situation<\/h3>\n\n\n\n

Im Verlauf des europ\u00e4ischen FP7-Projekts Bereitstellung von<\/a>, Siemens setzte die ProB-Software ein, um zu pr\u00fcfen, ob es m\u00f6glich war, ProB zur automatischen \u00dcberpr\u00fcfung 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 \u00dcberpr\u00fcfung<\/strong> (etwa ein Monat Arbeit f\u00fcr einen Mann).<\/p>\n<\/div>\n<\/div>\n\n\n\n

\n
<\/div>\n\n\n\n
\n

Herausforderung<\/h3>\n\n\n\n

Die Herausforderung, vor der das STUPS-Team (Softwaretechnik und Programmiersprachen) an der Universit\u00e4t D\u00fcsseldorf steht, wird in der Bereitstellung von Deliverable D41<\/a>. Siemens \u00fcbermittelte dem STUPS-Team am 8. Juli 2008 die Modelle f\u00fcr 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.<\/p>\n<\/div>\n<\/div>\n\n\n\n

\n
<\/div>\n\n\n\n
\n

L\u00f6sung<\/h3>\n\n\n\n

ProB wurde die M\u00f6glichkeit, das einfache Modell sofort zu analysieren<\/strong>. Ein Fehler in den Behauptungen wurde entdeckt. Daraufhin wurde ProB so verbessert, dass die Analyse des schwierigen Modells m\u00f6glich war. Die Verbesserungen, die vorgenommen wurden, waren nicht spezifisch f\u00fcr das fragliche Modell, sondern waren eher allgemeine Verbesserungen, die allen ProB-Benutzern zugute kamen. Die Ergebnisse der Analyse waren schl\u00fcssig.<\/p>\n\n\n\n

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<\/strong>. Man beachte, dass das STUPS-Team nicht \u00fcber das Vorhandensein von Fehlern in den Modellen informiert wurde (sie wurden von Siemens nicht einmal angedeutet), und zun\u00e4chst glaubte STUPS, dass es immer noch einen Fehler in ProB g\u00e4be. Tats\u00e4chlich handelte es sich aber um echte Fehler, und zwar genau um die Fehler, die Siemens selbst durch manuelle Pr\u00fcfung entdeckt hatte.<\/p>\n<\/div>\n<\/div>\n\n\n\n

\n
<\/div>\n\n\n\n
\n

Ergebnisse<\/h3>\n\n\n\n

Die Ergebnisse zeigen, dass die ProB ein gro\u00dfer Erfolg war. Anstatt mehrere Wochen zu brauchen<\/strong> um die Eigenschaften zu pr\u00fcfen manuell<\/strong>, war ProB in der Lage, die Eigenschaften in 4,15 Sekunden<\/strong> und die Behauptungen in 1017,7 Sekunden<\/strong> (ca. 17 Minuten) mit ProB<\/strong> 1.3.0. Die Leistungsoptimierung der ProB-Software wurde fortgesetzt. Die \u00dcberpr\u00fcfung der Behauptungen f\u00fcr das obige Modell dauert nun weniger als eine Minute<\/strong> unter Verwendung der aktuellen Version von ProB.<\/p>\n<\/div>\n<\/div>\n<\/div>","protected":false},"excerpt":{"rendered":"

Durch die Anpassung des ProB-Modellpr\u00fcfers konnte die Dauer der Datenvalidierung am Wegesrand von Wochen auf Minuten reduziert werden.<\/p>","protected":false},"author":1,"featured_media":1301,"comment_status":"open","ping_status":"open","sticky":false,"template":"wp-custom-template-page-large-header-dark","format":"standard","meta":{"_kadence_starter_templates_imported_post":false,"_kad_post_transparent":"","_kad_post_title":"","_kad_post_layout":"","_kad_post_sidebar_id":"","_kad_post_content_style":"","_kad_post_vertical_padding":"","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_kad_post_classname":"","footnotes":""},"categories":[17],"tags":[],"class_list":["post-78","post","type-post","status-publish","format-standard","has-post-thumbnail","hentry","category-success-story"],"_links":{"self":[{"href":"https:\/\/www.formalmind.com\/de\/wp-json\/wp\/v2\/posts\/78","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.formalmind.com\/de\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.formalmind.com\/de\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.formalmind.com\/de\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.formalmind.com\/de\/wp-json\/wp\/v2\/comments?post=78"}],"version-history":[{"count":0,"href":"https:\/\/www.formalmind.com\/de\/wp-json\/wp\/v2\/posts\/78\/revisions"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/www.formalmind.com\/de\/wp-json\/wp\/v2\/media\/1301"}],"wp:attachment":[{"href":"https:\/\/www.formalmind.com\/de\/wp-json\/wp\/v2\/media?parent=78"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.formalmind.com\/de\/wp-json\/wp\/v2\/categories?post=78"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.formalmind.com\/de\/wp-json\/wp\/v2\/tags?post=78"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}