3.1
Import
Certified
ProB
Software producer:
Webpage:
Programme type:
Data validation
railML® compatibility
Infrastructure
3.2
Import
Certified
3.3
Import
Certified
Interlocking
3.1
Import
Certified
3.2
Import
Certified
3.3
Import
Certified
Contact:
Heinrich-Heine-Universität Düsseldorf
Michael Leuschel
Universitätsstrasse 1
40225 Düsseldorf
Details:
ProB is an animator, constraint solver and model checker that targets high-level formal specification languages, particularly the B-Method. The B-method is a mathematically rigorous approach to develop safety critical systems. The B language supports higher order relations and functions and is well-suited for industrial railway applications.
ProB can convert railML data into the B language for formal data validation. Custom validation rules can be implemented using ProB’s domain-specific rule language. Official railML semantic constraints related to infrastructure and interlocking are checked automatically. The track topology can be visualised for better localisation of errors. Animation and simulation can be used to find errors in the dynamic interlocking behaviour.
ProB has been certified as a tool of class T2 (for SIL1 to SIL4 environments according to EN50128) for several data validation applications. It is developed by the STUPS group at the Heinrich Heine University Düsseldorf and has been used for numerous CBTC and ECTS data validation projects (e.g., Paris line 1 or Barcelona line 9).
--
ProB ist ein Animator, Constraint Solver und Model Checker, der auf formale Sprachen, insbesondere die B-Methode ausgerichtet ist. Die B-Methode ist ein mathematischer Ansatz zur Entwicklung sicherheitskritischer Systeme. Die B Sprache bietet Unterstützung für Relationen und Funktionen (höherer Ordnung) und ist besonders für industrielle Anwendungen im Bahnbereich geeignet.
ProB kann railML-Daten einlesen und in die B-Methode für formale Datenvalidierung übersetzen. Eigene Validierungsregeln können mit ProBs eigener Regelsprache implementiert werden. Offizielle railML Semantic Constraints im Bezug auf Infrastruktur und Stellwerkslogik werden automatisch geprüft. Die Streckentopologie kann zur besseren Lokalisierung von Fehlern visualisiert werden. Mithilfe von Animation und Simulation kann nach Fehlern im dynamischen Stellwerksverhalten gesucht werden.
Das ProB-Werkzeug ist für die Klasse T2 (für SIL1- bis SIL4-Umgebungen gemäß EN50128) für verschiedene Datenvalidierungsanwendungen zertifiziert. Es wird von der STUPS-Gruppe an der Heinrich-Heine-Universität Düsseldorf entwickelt und wurde für viele industrielle CBTC und ETCS Anwendungen eingesetzt (z.B. Paris Linie 1 oder Barcelona Linie 9).
License:
freeware
In use by the following partners:
Alstom Rail Sweden 
Clearsy 
HHU Düsseldorf 
Hitachi Rail GTS Germany 
Siemens Mobility Germany (Rail Infrastructure) This data is provided by the railML partner and under their responsibility.