{"id":327,"date":"2015-01-01T08:00:08","date_gmt":"2015-01-01T07:00:08","guid":{"rendered":"https:\/\/www.formalmind.com\/de\/?page_id=327"},"modified":"2022-04-11T18:58:54","modified_gmt":"2022-04-11T16:58:54","slug":"prob-validation-siemens-sas-2","status":"publish","type":"post","link":"https:\/\/www.formalmind.com\/de\/blog\/prob-validation-siemens-sas-2\/","title":{"rendered":"ProB-Validierung f\u00fcr Siemens SAS"},"content":{"rendered":"<p>[vc_row][vc_column width=&#8221;1\/4&#8243;][vc_single_image image=&#8221;416&#8243; img_size=&#8221;150&#215;150&#8243; alignment=&#8221;center&#8221; css_animation=&#8221;appear&#8221;][\/vc_column][vc_column width=&#8221;3\/4&#8243;][vc_column_text]<\/p>\n<h2>Situation<a href=\"http:\/\/www.deploy-project.eu\/\"><img data-src=\"https:\/\/www.formalmind.com\/wp-content\/uploads\/2016\/04\/deploy-300x211.png\" decoding=\"async\" class=\"alignright size-medium wp-image-364 lazyload\" src=\"data:image\/gif;base64,R0lGODlhAQABAIAAAAAAAP\/\/\/yH5BAEAAAAALAAAAAABAAEAAAIBRAA7\" alt=\"deploy\" width=\"300\" height=\"211\" \/><noscript><img decoding=\"async\" class=\"alignright size-medium wp-image-364\" src=\"https:\/\/www.formalmind.com\/wp-content\/uploads\/2016\/04\/deploy-300x211.png\" alt=\"deploy\" width=\"300\" height=\"211\"><\/noscript><\/a><\/h2>\n<p>Im Rahmen des europ\u00e4ischen <a href=\"http:\/\/ec.europa.eu\/research\/fp7\">FP7<\/a> Projekts <a href=\"http:\/\/www.deploy-project.eu\/\">Deploy<\/a> hat Siemens die Software ProB eingesetzt um herauszufinden, ob sie in der Lage ist, automatisch bestehende B-Modelle zu \u00fcberpr\u00fcfen. 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 \u00fcberpr\u00fcfen. Der dazu n\u00f6tige Aufwand entsprach etwa einem Personenmonat.[\/vc_column_text][\/vc_column][\/vc_row][vc_row][vc_column width=&#8221;1\/4&#8243;][vc_single_image image=&#8221;417&#8243; img_size=&#8221;150&#215;150&#8243; alignment=&#8221;center&#8221; css_animation=&#8221;appear&#8221;][\/vc_column][vc_column width=&#8221;3\/4&#8243;][vc_column_text]<\/p>\n<h2>Aufgabe<\/h2>\n<p>Im <a href=\"http:\/\/www.deploy-project.eu\/pdf\/D41-Siemens-final-full.pdf\">Forschungsbericht D41<\/a> des Deploy-Projektes ist die Herausforderung beschrieben: Siemens sandte dem STUPS Team an der Heinrich-Heine-Universit\u00e4t D\u00fcsseldorf 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\u00f6tigte 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=&#8221;1\/4&#8243;][vc_single_image image=&#8221;418&#8243; img_size=&#8221;150&#215;150&#8243; alignment=&#8221;center&#8221; css_animation=&#8221;appear&#8221;][\/vc_column][vc_column width=&#8221;3\/4&#8243;][vc_column_text]<\/p>\n<h2>L\u00f6sung<\/h2>\n<p>Mittels ProB konnte das einfachere Modell direkt analysiert werden. Dabei entdeckte das Werkzeug, dass eine der getroffenen Annahmen nicht erf\u00fcllt wurde. Um auch die Analyse des komplizierten Modells zu erm\u00f6glichen, wurde ProB in einigen Punkten verbessert, die letztendlich allen Anwendern zu Gute kommen.<\/p>\n<p>Am 8. Dezember 2008 konnte das kompliziertere Modell schlie\u00dflich vollst\u00e4ndig analysiert werden, wobei <strong>vier Fehler entdeckt<\/strong> 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\u00e4ndig korrekt war. Wie es sich herausstellte, waren es genau die Fehler, die auch Siemens im Laufe der manuellen \u00dcberpr\u00fcfung fand.[\/vc_column_text][\/vc_column][\/vc_row][vc_row][vc_column width=&#8221;1\/4&#8243;][vc_single_image image=&#8221;419&#8243; img_size=&#8221;150&#215;150&#8243; alignment=&#8221;center&#8221; css_animation=&#8221;appear&#8221;][\/vc_column][vc_column width=&#8221;3\/4&#8243;][vc_column_text]<\/p>\n<h2>Ergebnis<\/h2>\n<p>Die Anwendung von ProB hat sich als voller Erfolg erwiesen. <strong>Mehrere Wochen manueller Analyse<\/strong> erledigte ProB in etwa <strong>17 Minuten<\/strong> (mit der damaligen Version 1.3.0). Die Software wurde seitdem stetig verbessert und sie ben\u00f6tigt in der aktuellen Version mittlerweile <strong>weniger als eine Minute<\/strong>, um alle Annahmen zu \u00fcberpr\u00fcfen.[\/vc_column_text][\/vc_column][\/vc_row]<\/p>\n","protected":false},"excerpt":{"rendered":"<p>[vc_row][vc_column width=&#8221;1\/4&#8243;][vc_single_image image=&#8221;416&#8243; img_size=&#8221;150&#215;150&#8243; alignment=&#8221;center&#8221; css_animation=&#8221;appear&#8221;][\/vc_column][vc_column width=&#8221;3\/4&#8243;][vc_column_text] Situation Im Rahmen des europ\u00e4ischen FP7 Projekts Deploy hat Siemens die Software ProB eingesetzt um herauszufinden, ob sie in der Lage ist, automatisch bestehende B-Modelle zu \u00fcberpr\u00fcfen. Diese Modelle, die Gleisstrukturen und Signaldaten beschreiben, wurden bereits produktiv eingesetzt. Bei Siemens wurden zum damaligen Zeitpunkt mehrere Wochen darauf verwendet,&#8230;<\/p>\n","protected":false},"author":1,"featured_media":368,"comment_status":"open","ping_status":"open","sticky":false,"template":"single-no-separators","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":[13],"tags":[],"class_list":["post-327","post","type-post","status-publish","format-standard","has-post-thumbnail","hentry","category-blog"],"_links":{"self":[{"href":"https:\/\/www.formalmind.com\/de\/wp-json\/wp\/v2\/posts\/327","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=327"}],"version-history":[{"count":0,"href":"https:\/\/www.formalmind.com\/de\/wp-json\/wp\/v2\/posts\/327\/revisions"}],"wp:attachment":[{"href":"https:\/\/www.formalmind.com\/de\/wp-json\/wp\/v2\/media?parent=327"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.formalmind.com\/de\/wp-json\/wp\/v2\/categories?post=327"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.formalmind.com\/de\/wp-json\/wp\/v2\/tags?post=327"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}