Encapsulating Formal Methods within Domain Specific Languages: A Solution for Verifying Railway Scheme Plans

TL;DR

This paper presents a methodology for creating domain-specific languages that incorporate formal methods to improve railway scheme plan verification, addressing industrial adoption challenges.

Contribution

It introduces a novel methodology for developing DSLs with formal methods, demonstrated through a successful railway domain case study.

Findings

Improved verification scalability for railway schemes

Enhanced accessibility of formal methods for practitioners

Successful application of the methodology in industry context

Abstract

The development and application of formal methods is a long standing research topic within the field of computer science. One particular challenge that remains is the uptake of formal methods into industrial practices. This paper introduces a methodology for developing domain specific languages for modelling and verification to aid in the uptake of formal methods within industry. It illustrates the successful application of this methodology within the railway domain. The presented methodology addresses issues surrounding faithful modelling, scalability of verification and accessibility to modelling and verification processes for practitioners within the domain.