Validation of railML Using ProB
摘要
The aim of this work is to translate railML 3 files to the formal B-method to enable formal verification and validation. railML is an XML-based format designed to facilitate the exchange of information about railway systems. Our approach allows syntactic and semantic validation against predefined and custom rules, using ProB and its integrated B-Rules DSL. In addition, a B-model can be generated to animate the dynamic behaviour of the specification, which can also be used for simulations and statistical tests using SimB. A technique for creating visualisations of the topology using Graphviz is presented. Finally, real-life railML case studies show that the implemented validation process can be effectively applied to complex models and that errors in these models can be successfully detected.