Den Kern der B-Methode bildet eine sehr ausdrucksstarke Sprache, die auf Prädikatenlogik, Mengenlehre, Relationenrechnung, Funktionen höherer Ordnung und Arithmetik beruht. Das Herzstück unserer ProB toolset ist ein Evaluator und Constraint Solver für diese Sprache. Wir streben sowohl Effizienz als auch Korrektheit an, so dass das Tool in einem sicherheitskritischen Kontext verwendet werden kann.
Das Unternehmen ClearSy hat ein interessantes Erfolgsgeschichte über den Einsatz unseres Tools ProB für ein Reverse-Engineering-Projekt im Schienenverkehr,wo sie den Constraint Solver von ProB auf eine neue Art und Weise genutzt haben. In dem Artikel heißt es: “Die Grundsätze der Datenvalidierung wurden kürzlich mit großem Erfolg auf ein Reverse-Engineering-Projekt im Eisenbahnwesen angewandt. B und ProB haben erneut gezeigt, wie effizient sie sind, wenn sie in Kombination verwendet werden. ... Dieses Problem wurde auf elegante Weise gelöst, indem die Grundsätze der Datenvalidierung angewandt wurden: Es wurde ein B-Modell erstellt, das die beiden Graphen und ihre Eigenschaften darstellt, und ProB für die Suche nach einer Lösung verwendet.”
Nachfolgend sehen Sie den vom ProB Constraint Solver generierten Matching-Graphen zwischen dem Anwendungsbinary und dem High-Level-Quellcode:
