Scholarlink

Formal methods and domain-specific languages (DSLs) are now integral to the development and assurance of railway signalling systems in compliance with CENELEC EN 50128 and EN 50129. This article presents a survey and a comparison of research works and industrial initiatives that intertwine graphical DSLs with formal verification techniques. The comparison covers modelling syntax, operational semantics, adherence to industrial standards such as RailML, EULYNX and ERTMS/ETCS, and the extent to which each solution supports verification and validation. Special attention is devoted to initiatives that rely on the B Method and its associated toolchain, notably ProB, because these initiatives demonstrate how mathematically proven artefacts can be presented to, and interactively animated by, signalling engineers through user-friendly diagrams. The study highlights the added value of visual front-ends for bridging the communication gap between domain experts and formal-methods specialists while preserving traceability from informal requirements to verified systems.

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

Bridging Formal Verification and Domain Validation in Railway Systems

  • 会议论文

  • 发表日期：

    2026年

查看全文
  • Asfand Yar,
  • Akram Idani,
  • Yves Ledru,
  • Simon Collart-Dutilleul

摘要

Formal methods and domain-specific languages (DSLs) are now integral to the development and assurance of railway signalling systems in compliance with CENELEC EN 50128 and EN 50129. This article presents a survey and a comparison of research works and industrial initiatives that intertwine graphical DSLs with formal verification techniques. The comparison covers modelling syntax, operational semantics, adherence to industrial standards such as RailML, EULYNX and ERTMS/ETCS, and the extent to which each solution supports verification and validation. Special attention is devoted to initiatives that rely on the B Method and its associated toolchain, notably ProB, because these initiatives demonstrate how mathematically proven artefacts can be presented to, and interactively animated by, signalling engineers through user-friendly diagrams. The study highlights the added value of visual front-ends for bridging the communication gap between domain experts and formal-methods specialists while preserving traceability from informal requirements to verified systems.