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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Validation of railML Using ProB

  • Jan Gruteser,
  • Michael Leuschel

摘要

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.