ProB for railML

<<This page is under construction and will be extended soon!>>

ProB can read in and translate railML 3 data to the formal B language.

In particular, ProB can be used for

Formal semantic validation of the static data
- including additional data structures computed from the data, e.g. route paths
- output: HTML or XML validation report
Visualisation of the topology
- either by explicit visualisation data provided in the railML file
- or automatically using Graphviz (for validation; this is not a schematic track plan)
Animation/Simulation
- for validation and verification of the dynamic interlocking behaviour

The import interface of ProB is called railML2B and is certified for railML 3.1, 3.2, and 3.3.

ProB is also certified as a tool of class T2 (SIL4) for data validation according to the Cenelec EN 50128 standard.

More information about the industrial use of ProB for railways can be found here.

How to Use railML2B

railML2B is the core implementation of the railML import used by ProB.

Quick Start

railML2B is usable via

ProB's tooling IDE ProB2-UI,
a command line interface (CLI) or by
direct integration into Java projects.

For a quick start, we recommend using ProB2-UI (download the snapshot version here).

In the menu bar, select Advanced > Data Import > railML 3 or open a .railml/.railmlx directly. The railML 3 import dialogue should be visible now.

Paper/Citing

The first version of ProB's railML import feature has been presented at ICECCS 2024 in Cyprus: Validation of railML Using ProB

@InProceedings{railml-prob,
    author={Jan Gruteser and Michael Leuschel},
    title={Validation of railML Using ProB},
    booktitle={Proceedings ICECCS 2024},
    year={2024},
    series={LNCS},
    volume={14784},
    publisher={Springer},
    pages={245--256},
    doi={10.1007/978-3-031-66456-4_13}
}

Partner

The Heinrich Heine University Düsseldorf is a partner of railML.org.