{"id":126,"date":"2013-06-17T08:00:00","date_gmt":"2013-06-17T06:00:00","guid":{"rendered":"https:\/\/www.formalmind.com\/blog\/data-validation-reverse-engineering\/"},"modified":"2022-04-11T18:58:55","modified_gmt":"2022-04-11T16:58:55","slug":"data-validation-reverse-engineering","status":"publish","type":"post","link":"https:\/\/www.formalmind.com\/de\/blog\/data-validation-reverse-engineering\/","title":{"rendered":"Datenvalidierung und Reverse Engineering"},"content":{"rendered":"<p>Den Kern der B-Methode bildet eine sehr ausdrucksstarke Sprache, die auf Pr\u00e4dikatenlogik, Mengenlehre, Relationenrechnung, Funktionen h\u00f6herer Ordnung und Arithmetik beruht. Das Herzst\u00fcck unserer&nbsp;<a href=\"http:\/\/www.stups.uni-duesseldorf.de\/ProB\/\">ProB<\/a>&nbsp;toolset ist ein Evaluator und Constraint Solver f\u00fcr diese Sprache. Wir streben sowohl Effizienz als auch Korrektheit an, so dass das Tool in einem sicherheitskritischen Kontext verwendet werden kann.<\/p>\n<p><span style=\"font-size:12px;\">Das Unternehmen&nbsp;<a href=\"http:\/\/www.clearsy.com\">ClearSy<\/a>&nbsp;hat ein interessantes <a href=\"http:\/\/www.data-validation.fr\/data-validation-reverse-engineering\/#more-87\">Erfolgsgeschichte \u00fcber den Einsatz unseres Tools ProB f\u00fcr ein Reverse-Engineering-Projekt im Schienenverkehr<\/a>,wo sie den Constraint Solver von ProB auf eine neue Art und Weise genutzt haben.&nbsp;<\/span>In dem Artikel hei\u00dft es: \u201c<em>Die Grunds\u00e4tze der Datenvalidierung wurden k\u00fcrzlich mit gro\u00dfem Erfolg auf ein Reverse-Engineering-Projekt im Eisenbahnwesen angewandt. B und <a href=\"http:\/\/www.stups.uni-duesseldorf.de\/ProB\/\">ProB<\/a> haben erneut gezeigt, wie effizient sie sind, wenn sie in Kombination verwendet werden. ... Dieses Problem wurde auf elegante Weise gel\u00f6st, indem die Grunds\u00e4tze der Datenvalidierung angewandt wurden: Es wurde ein B-Modell erstellt, das die beiden Graphen und ihre Eigenschaften darstellt, und <a href=\"http:\/\/www.stups.uni-duesseldorf.de\/ProB\/\">ProB<\/a> f\u00fcr die Suche nach einer L\u00f6sung verwendet<\/em>.\u201d<\/p>\n<p>Nachfolgend sehen Sie den vom ProB Constraint Solver generierten Matching-Graphen zwischen dem Anwendungsbinary und dem High-Level-Quellcode:<\/p>\n<p><img class=\"lazyload\" data-src=\"\/sites\/default\/files\/ProBClearSy_graf.jpg\" decoding=\"async\" alt=\"\" src=\"data:image\/gif;base64,R0lGODlhAQABAIAAAAAAAP\/\/\/yH5BAEAAAAALAAAAAABAAEAAAIBRAA7\" style=\"width: 474px; height: 151px; \"><noscript><img decoding=\"async\" alt=\"\" src=\"\/sites\/default\/files\/ProBClearSy_graf.jpg\" style=\"width: 474px; height: 151px; \"><\/noscript><\/p>","protected":false},"excerpt":{"rendered":"<p>Den Kern der B-Methode bildet eine sehr ausdrucksstarke Sprache, die in der Pr\u00e4dikatenlogik, der Mengenlehre, dem Relationenkalk\u00fcl, Funktionen h\u00f6herer Ordnung und der Arithmetik wurzelt. Das Herzst\u00fcck unseres ProB-Toolsets ist ein Evaluator und Constraint Solver f\u00fcr diese Sprache. Wir streben sowohl Effizienz als auch Korrektheit an, so dass das Tool in einem sicherheitskritischen Kontext verwendet werden kann....<\/p>","protected":false},"author":1,"featured_media":0,"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-126","post","type-post","status-publish","format-standard","hentry","category-blog"],"_links":{"self":[{"href":"https:\/\/www.formalmind.com\/de\/wp-json\/wp\/v2\/posts\/126","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=126"}],"version-history":[{"count":0,"href":"https:\/\/www.formalmind.com\/de\/wp-json\/wp\/v2\/posts\/126\/revisions"}],"wp:attachment":[{"href":"https:\/\/www.formalmind.com\/de\/wp-json\/wp\/v2\/media?parent=126"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.formalmind.com\/de\/wp-json\/wp\/v2\/categories?post=126"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.formalmind.com\/de\/wp-json\/wp\/v2\/tags?post=126"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}