Machine-Readable Railway Regulations - A Formal Framework for Automated Compliance Verification in Engineering and Operations

Railway systems are governed by extensive regulatory frameworks — spanning European Technical Specifications for Interoperability (TSIs), national regulations such as Switzerland's Eisenbahnverordnung (EBV), and infrastructure-manager-specific standards — that collectively encompass thousands of pages of natural language text. In particular, the ERTMS strategy of the Swiss Federal Office of Transport (BAV) defines the roadmap for modernizing the Swiss railway network, with a strong focus on transitioning to ETCS Level 2 (ETCS L2) and implementing "Führerstandsignalisierung" (FSS – cab signaling) and Massnahme 11 (F11 – Vehicle upgrades) nationwide to improve capacity, safety, and interoperability. Verifying that a proposed railway design or operational plan complies with these regulations is currently a labor-intensive, error-prone, and expert-dependent process that cannot keep pace with the growing complexity and digital throughput of modern railway engineering workflows.

This project proposes to develop FORMALRAIL, a formal framework for translating human-readable railway regulations into machine-executable specifications, enabling automated compliance verification of digital railway design and operations artifacts. The core scientific challenge lies at the intersection of formal methods, knowledge representation, and natural language processing: regulations are often ambiguous, sometimes even conflicting, hierarchically structured, context-dependent, and laden with cross-references and exceptions — properties that fundamentally resist naive or direct formalization.

Building on the PI's prior work on the Rulebooks formalism for autonomous vehicles — a mathematically rigorous approach for encoding hierarchically-structured behavioral rules drawn from traffic law, ethics, and cultural norms, developed and deployed in production at nuTonomy (currently Motional) — we will extend and adapt this methodology to the railway domain. The project will pursue three interrelated objectives: (1) development of a formal domain ontology for Swiss and European railway entities and regulatory constraint types; (2) creation of an NLP-assisted pipeline for semi-automatically extracting structured, machine-executable rules from regulatory text, validated by domain experts; and (3) design and prototyping of automated compliance checking algorithms for railway designs expressed in standard digital formats (e.g., railML). 

The framework will be grounded in and validated against real-world Swiss railway regulations and engineering data, in close collaboration with SBB and Siemens Mobility. The primary deliverables are an open formal ontology, a prototype compliance checking tool, and 2–3 peer-reviewed publications. The long-term goal is to lay the scientific foundation for industry-grade, continuously integrated automated compliance checking tools, which will be developed and deployed by the industrial partners.