Merging railway standard notations in a formal dsl-based framework

Abstract

The design of a railway signalling system may be validated using three basic concepts: (1) functional standards, (2) domain specific notations, and (3) safety requirements checking. However, there is a lack of tools that merge these notions in a unified framework to be used by standardisation authorities, as well as domain experts and safety engineers. In this ongoing work we make the bridge between the three notions using Meeduse, a tool in which the B method is applied in order to formally reason on the correctness of domain specific languages (DSLs) and simulate their dynamic semantics using the ProB animator. The application context of this work is that of two well known standards in the railway field: RailTopoModel and ERTMS/ETCS. We propose a railway DSL framework whose static semantics are built on top of RailTopoModel and the underlying dynamic semantics conform to ERTMS/ETCS. The overall approach is assisted by the B method, which allows us to define, prove and animate safety-critical behaviors given domain-centric models.