ProB for railML

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.

Why should I translate railML data to B?

railML is an XML-based exchange format for various types of railway data. In particular, it can contain safety-critical data about infrastructure and interlocking. When developing a real system, you may want to check whether your data is correct and meets certain (regulatory) requirements. The B method provides a way to formalise such requirements mathematically. With ProB, you can automatically validate the rules for the imported data and export the validation results as HTML and XML file. The advantage lies in the precise mathematical notation, whilst the automatic validation can also be integrated into a toolchain via the Java API.

Quick Start with railML2B

railML2B is the core implementation of the railML import used by ProB. 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.

A detailed tutorial will be available here soon.

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.