Validating ETCS Data with the B Mathematical Language: An Industrial Pipeline and a Blueprint for LLM Integration Thierry Lecomte and Vincent Germain
arXiv:2607.26111v1 [cs.SE] 28 Jul 2026
CLEARSY, Aix en Provence, France, {thierry.lecomte, vincent.germain}@clearsy.com
Abstract. Can large language models participate in the production and validation of ERTMS/ETCS data without undermining the certification arguments required by CENELEC EN 50128/50716? ERTMS/ETCS is a distributed safety-critical system (trackside, onboard, radio-block centre) whose behaviour is parameterised by large volumes of data drawn from the UNISIG Subsets; errors in that data propagate through the distributed architecture. This paper reports the current status of an ongoing industrial research effort at CLEARSY, ValidAItion, that bridges the ERTMS Operational Simulator to the CLEARSY Data Solver and applies rules expressed in the B mathematical language to that trackside data. During construction, a large language model (Claude) has authored the rule corpus and the parsers through a Model Context Protocol server; every proposal is adjudicated by the downstream toolchain and by systematic human review, and the toolchain has already rejected a syntactically valid but semantically illegal generated scenario. The contribution is architectural and industrial, not algorithmic: the work combines frameworks already in use at CLEARSY (CLEARSY Data Solver, ERTMS Operational Simulator) with a conversational authoring loop, rather than proposing a new formal method. It is a progress report: rule coverage is growing, the human-review campaign is underway, and the quantitative results will be published separately. The paper argues, on the evidence gathered so far, that formal rules in the mathematical language of B must remain the source of truth, while the language model serves as the fenced assistant in a distributed safety-critical railway system: AI proposes, the formal oracle disposes, the human confirms.
Keywords: B mathematical language, ERTMS/ETCS, Subset-026, data validation, formal methods, LLM, MCP, safety-critical railway
1
Introduction
ERTMS and its ETCS layer are being rolled out across an expanding share of the European network. Baseline 3 Release 2 consolidates the specification under the UNISIG Subsets (026 System Requirements, 036 Eurobalise FFFIS, 044 Euroloop FFFIS, 085 Eurobalise test). Production use of ETCS depends not only on code
being correct, but on data (balise telegrams, route data, speed profiles, linking distances, movement-authority ranges) being correct with respect to thousands of rules distilled from those Subsets. Data errors scale with deployment: every new line re-authors hundreds of kilometres of trackside data under time and budget pressure. Data validation is therefore one of the most scalable industrial applications of formal methods in railway, pursued at CLEARSY since the DTVT1 work of the 2010s [16,17]. Three pressures are reshaping this activity in 2026. First, the growth of Subset coverage expected from modern projects; Baseline 4 will add more shall statements. Second, the increasing demand for safety in mainline deployment. Formal data validation has a long industrial track record in Communication-Based Train Control for metro lines (CBTC); its use for mainline ERTMS/ETCS is recent. At the same time, the CENELEC standards applicable to this activity have tightened: the successor of EN 50128, EN 50716, now lists formal methods as highly recommended at every Safety Integrity Level, SIL-1 and SIL-2 included, whereas EN 50128 only recommended them for those levels [6,7]. Safety authorities have reinforced the same expectation: following the 2019 La Milesse overspeed event on the Paris–Rennes high-speed line (TGV operating under ETCS Level 2, travelling at 165 km/h through a turnout authorised to 100 km/h), the French BEA-TT recommended that the evaluation of ETCS-data validation make explicit use of verification, testing and formal-proof tools [3]. Third, the arrival of large language models in engineering workflows: LLMs accelerate drafting and exploration but also produce plausible-looking artefacts that are semantically wrong. In a context further regulated, for AI-assisted systems, by the EU AI Act Article 14 [11], an LLM that confidently writes invalid ETCS data is worse than no LLM at all. Position. Rather than treat LLMs as a replacement for formal methods, we argue for an inversion: formal rules in the B mathematical language [1] (set theory, first-order logic, relations, arithmetic; no B machines, refinements or implementations) remain the source of truth, and LLMs are fenced assistants: every output is adjudicated by a formal oracle and by systematic human review. This stance follows the broader line sketched at FM 2026 [19]; the present paper instantiates it on ETCS Subset-026/036/044/085 trackside data validation. Scope. We call this effort ValidAItion throughout the paper. It is a progress report. At the time of writing, 22 of the 43 Subset-derived tractable rules are formalised as predicates in the mathematical language of B and further rules are being added; the human-review campaign is underway; and the full 82-rule solver sweep on the three ERTMS Operational Simulator (OP SIMU) production databases is in preparation. The paper establishes the pipeline, the architectural stance, the coverage denominator and the governance structure; the quantitative outcomes of the review campaign and of the production sweep will appear in a follow-up paper. 1
DTVT denotes a data-validation tool used by Alstom Transport SA; the term is retained here as a historical reference to the CLEARSY work of the 2010s on that family of projects.
Section 2 gives the ERTMS/ETCS background. Section 3 explains the rationale. Section 4 describes the ValidAItion pipeline. Section 5 reports the case study, coverage, rule corpus, error taxonomy and human-review artefacts. Section 6 presents the blueprint for fenced LLM-assisted engineering. Section 7 surveys related work. Section 8 concludes.
2
Background: ERTMS/ETCS and the Subsets
ERTMS is a distributed, layered system. Trackside equipment (balises, radio-infill units, radio-block centres) transmits information to onboard units (OBUs) that compute a Movement Authority (MA), monitor the train’s adherence to a Static Speed Profile (SSP) and apply service or emergency braking when necessary. The correctness of this distributed behaviour depends on the consistency of the data that parameterises it: the same balise-group identifiers, linking tables, MA segments and SSP entries are read by the trackside generator, encoded into telegrams, transmitted through the radio-balise protocols, and interpreted by the onboard unit. An inconsistency at any point in that chain manifests as a distributed fault. The data-validation activity addressed in this paper targets this parameter layer of the distributed system. The information flow is standardised by the UNISIG Subsets, which define the radio and balise protocols (Subset-036, Subset-044, Subset-058), the test specifications (Subset-076, Subset-085), and the overall System Requirements Specification (Subset-026). Among the Subsets, Subset-026 carries the bulk of the functional specification: it defines the ETCS modes and transitions, the packets exchanged between trackside and onboard, and the operational rules for levels L0, L1, L2 and L3. Subset-036 specifies the Eurobalise FFFIS (physical-layer signalling, telegram coding, CRC), and Subset-085 specifies how those telegrams must be tested. Subset-044 covers the Euroloop FFFIS. Together they constrain every bit encoded in a balise telegram and every kilometre of track data that a project must author and validate before commissioning. The rules derived from these Subsets fall into two broad categories that matter for the present work. A first category, which we call geometric/static, governs the physical placement and identification of trackside equipment: balise groups (BGs) must be a minimum distance apart, must lie on valid edges, must carry unique identifiers within a project; gradient profiles must cover the extent of each MA; SSP speed entries must be positive and non-decreasing on certain segments; linking distances must lie within ranges specified for each Level. These rules can be checked purely from a geometric model of the track (nodes, edges, signals, balise groups, telegrams’ linking tables) without simulating the onboard unit. A second category, which we call onboard/operational, governs the reaction of the OBU to received information, the bit-level encoding and scrambling of telegrams, the operational procedures for session handover, and the definition of national values. These rules require either a full model of the onboard state machine, a bit-exact decoder of the telegram payload, or operational knowledge that is orthogonal to the trackside dataset.
This partition is decisive for the scope of any industrial data-validation pipeline built from trackside sources alone. In Sect. 5.2 we give a quantitative classification along these lines for the 147 rules drawn from Subsets 026, 036, 044 and 085, and we use it as the explicit coverage denominator for our claims. Two further points bear on the rest of the paper. First, ETCS data validation is by nature scalable: the rule set is finite and standardised, while the data it must check grows with every deployed kilometre of line. The rule-formalisation cost is paid once and amortised across many deployments, an economic profile favourable to formal methods. Second, the quality of the realistic data used in validation matters: toy examples do not surface the rule-interaction patterns that arise in production topologies. In our case study we rely on the databases of the ERTMS Operational Simulator (OP SIMU), which carry industrial-grade track layouts including the nine-track CLEARSY demonstration database. The remainder of the paper uses the word fencing for the architectural stance adopted throughout: an LLM proposes engineering artefacts (rules, parsers, scenarios), and every proposal is filtered by a formal oracle (the CLEARSY Data Solver discharging predicates expressed in the mathematical language of B over JSON, or OP SIMU on scenario reload) and by systematic human review before it is retained. The metaphor is structural rather than rhetorical: the formal toolchain and the human reviewer act as a wall around the LLM, letting through only what they can adjudicate against a Subset clause or a documented engineering convention. The pipeline described in Sect. 4 instantiates this stance on ETCS trackside data; the blueprint of Sect. 6 generalises it to engineer-in-the-loop use.
3
Rationale: Why B-Math, Why Data Validation, Why Now
The motivation is to reconcile two activities pursued in largely separate teams at CLEARSY. On one side, the formal modelling of software and systems and the data validation of the constant parameters that parameterise them, grounded in the B method for code and in the B mathematical language for project data [16,20,4]. On the other, the simulation of ETCS systems for education, training and testing, integrated with testbenches for onboard and trackside equipment and used to study how change requests to the UNISIG Subsets modify the overall behaviour [17]. These two worlds rarely meet: the first operates on structured data with formal tools, the second on behaviour with simulators. The present work connects them and shows, on real OP SIMU databases, that formal methods can be applied within a pure simulation activity.
The industrial vehicle of the approach is the CLEARSY Data Solver 2 , in which rules are written in a controlled B-math syntax with intermediate constructions (.ic), accessors (.acc) and compute variables (.cv). The choice of the B mathematical language is pragmatic: its core (set theory, relations, first-order logic, arithmetic) is expressive enough for the data-validation obligations drawn from the Subsets, and the solver is a mature industrial platform familiar to the CENELEC certification community. We make no claim of new formalism or new solver technique; the contribution of this paper is architectural and industrial, not algorithmic. The choice of B-math, the Atelier B ecosystem, OP SIMU and the CLEARSY Data Solver is not a neutral evaluation of alternatives but reflects the frameworks already in industrial use at CLEARSY today; the research question we address is how to combine them with LLM-assisted authoring, not how to replace them. The rules are predicates over the project data, not software to be executed on a train: no B machine, refinement or implementation is produced in this activity. The target is OP SIMU itself. OP SIMU executes ETCS scenarios on a reference virtual machine and stores each scenario as a MySQL dump; the dumps are the authoritative input of the simulator and the primary source of our test data. ValidAItion converts a dump to the solver’s input format, discharges the formal rules derived from Subsets 026/036/044/085, and returns an OK/KO verdict together with counter-examples. The commitment is deliberately scoped: the translators and generators of the chain (SQL-to-JSON bridge, parsers, LLMauthored rule drafts) are not themselves certified today; the formal stance is carried by the solver’s discharge of the B-math predicates and by the subsequent human review. The reason the activity deserves attention now is the LLM question: by 2026 signalling engineering will not remain untouched by LLM-based assistance, and the proper place for an LLM in a safety-critical ecosystem is fenced : a proposer whose outputs are adjudicated by a formal oracle and reviewed by a human, never a decider.
4
The ValidAItion Pipeline
The ValidAItion proof of concept connects two worlds that, until this work, were unconnected inside CLEARSY: the ERTMS Operational Simulator (OP SIMU), which stores ETCS scenarios as MySQL dumps and executes them on a reference VM, and the CLEARSY Data Solver, which discharges predicates in the B mathematical language over structured project data. The bridge is a Python command-line interface (CLI), the DataProcessor, that parses the OP SIMU SQL dumps, produces the JSON and JSON-Schema files expected by the solver, 2
The CLEARSY Data Solver (https://www.clearsy.com/en/tools/data-solver/) is the industrial packaging of the Caval rule engine with the ProB constraint solver as back-end, developed within the Atelier B ecosystem. The product is certified T2 under CENELEC EN 50128 [6], which makes it usable as a verification tool for safety-related software up to SIL 4. Version details of the underlying engines are given in Sect. 5.1.
carries structured project rules expressed in the mathematical language of B, and orchestrates the execution of those rules. An LLM (Claude), exposed to the database through a Model Context Protocol (MCP) server, participated in the construction of the rule corpus and the parsers under human review and was in every case adjudicated by the downstream toolchain. Figure 1 summarises the three roles of the pipeline (authoring, data transport and adjudication) and marks the six artefacts that are subject to systematic human review. We emphasise once more that no B machine, refinement or implementation is produced: the rules are predicates over the project data, not software. We make this scope explicit because it has been queried in review. The activity described here intentionally uses the mathematical language of B (set theory, first-order logic, relations and arithmetic) as a predicate language over project data; it does not produce B machines, refinements or implementations because the artefact being validated is constant trackside data, not a stateful computation to be refined into code. This is neither a limitation of the B language — which can model such a computation when one exists — nor a deferral; it is a fit of method to artefact. A future activity that produced a derived safety-critical computation (e.g. an onboard runtime check derived from the validated dataset) would justify a chain from B machines through refinement to implementation, and the success rate of such a chain would then be a relevant metric. The present paper does not undertake that step.
4.1
Architecture, file formats and bridge
The pipeline has two legs. On the data leg, dataprocessor sql2json reads the OP SIMU MySQL dump, reconstructs the track topology and telegram-linking tables, and emits a .json data file with its matching .jsonsd schema; an integrated decoder handles Packets 5 (linking), 12 (MA), 21 (gradient) and 27 (SSP), while bit-level payload encoding (CRC, scrambling, substitution) remains out of scope. On the authoring leg, Claude accesses the same database through a FastMCP server and drafts the rule corpus in six Lark3 -parsed formats: .json data, .jsonsd JSON-Schema, .rule rules in B-math syntax (FOR / WHERE / SELECT / VERIFY), .ic intermediate constructions, .acc accessors over the JSON, and .cv compute variables for auxiliary computations. Round-trip parse/generate is verified by 324 pytest tests; all quantities are in metres with edge-local abscissae (positions measured along a track-graph edge, from that edge’s start node). Two roles are explicit throughout: the LLM is a proposer and the CLEARSY Data Solver is the adjudicator ; every predicate is discharged by the solver and every LLM-authored edit is confirmed by a human review before being retained. 3
Lark, https://github.com/lark-parser/lark, an LALR/Earley parser library for Python used here to parse the six custom file formats.
AUTHORING
DATA
ADJUDICATION
ETCS Subsets 026 / 036 / 044 / 085
OP SIMU SQL dump L1 FS, Webinar, CLEARSY Demo
CLEARSY Data Solver
5 1
LLM (Claude) via FastMCP 2
.rule .ic .acc .cv
3
DataProcessor sql2json + decoder Pkt 5/12/21/27
6
OK / KO reports + counter-examples
developed with Claude Code 4
.json .jsonsd
Fig. 1: ValidAItion pipeline. Three columns: authoring (LLM + MCP), data transport (DataProcessor; sql2json and the telegram decoder were themselves developed with Claude Code under human review), adjudication (CLEARSY Data Solver). The dashed arrow is the LLM-to-OP SIMU feedback path for scenario editing. Red-circled numbers mark artefacts subject to systematic human review: (1) Subset-clause-to-rule mapping; (2) .rule / .ic / .acc / .cv drafts; (3) OP SIMU SQL dump provenance; (4) .json / .jsonsd produced by sql2json; (5) LLM-generated scenarios before reload into OP SIMU; (6) counter-examples before engineering action.
4.2
Worked example: Rule BG Min Distance
The rules are best read in full text. The minimum inter-balise distance within a balise group is governed by SS-036 §7.5 and specialised at CLEARSY as ETCS Rule 1.14 ; its ValidAItion formalisation is a single .rule file: FOR BAL1, BAL2 WHERE BAL1 : dom(DEMO::balise_item@NID_BG) & BAL2 : dom(DEMO:: balise_item@NID_BG) & BAL1 /= BAL2 & DEMO::balise_item@NID_BG(BAL1) = DEMO::balise_item@NID_BG(BAL2) & DEMO::balise_item@edge (BAL1) = DEMO::balise_item@edge (BAL2) THEN SELECT DEMO::balise_item@abscissa(BAL1) <= DEMO:: balise_item@abscissa(BAL2) THEN VERIFY abs(DEMO::balise_item@abscissa(BAL2) - DEMO::balise_item@abscissa(BAL1)) >= 500 ENDVERIFY ENDSELECT ENDFOR
(The solver scales distances by 102 , so 5 m maps to 500 internal units.) The rule quantifies over two balises of the same balise group on the same edge (a track
segment between two topological nodes), orders them by abscissa to avoid the symmetric obligation, and asserts their absolute distance is at least 5 m. The syntax is pure mathematical language of B [1] (set membership, dom, function application, equality, arithmetic) inside a FOR / WHERE / SELECT / VERIFY envelope that the CLEARSY Data Solver compiles into proof obligations. Accessors are typed projection functions over the JSON data, defined in the corresponding .acc file; here DEMO::balise item@NID BG maps a balise identifier to the NID BG field of its JSON record. The solver discharges one obligation per pair satisfying the WHERE clause, reports a counter-example on failure, and emits an OK/KO verdict; this rule executes in about seven seconds on a database of the size of the CLEARSY OP SIMU demonstration scenarios (Sect. 5.1). A more complex rule illustrates the predicate language’s reach. Rule MA Section Count Valid (SS-026 §3.11) asserts that a Movement Authority packet’s N ITER-encoded section list contains exactly as many sections as declared, that every L SECTION is positive and bounded by the project’s maximum MA extent, and that the last section’s end marker is consistent with the SSP. The rule quantifies over each MA packet in the dataset, projects out the declared and observed section counts via two .acc accessors, traverses the section list with a .cv compute variable, and emits one obligation per inconsistency. Where Rule BG Min Distance is a single geometric predicate over a homogeneous collection, this one combines structural traversal, arithmetic bounds and a cross-reference between the MA and the SSP packets; the predicate language handles both without escaping into procedural code. 4.3
MCP surface and scope invariant
We call the set of MCP tools exposed to the LLM the MCP surface, and we keep this surface narrow by design. The OP SIMU side exposes a FastMCP4 server with read primitives (get database summary, list tables, get table schema, query table) and create-read-update-delete (CRUD) primitives (load sql, export sql, reset database, delete entity, update entity), plus further scenario-construction tools. The MCP surface lets the LLM read and propose edits through a typed, logged API, but never write authoritative artefacts. Those are (i) the rule corpus expressed in the mathematical language of B, adjudicated by the solver and human-reviewed, and (ii) the scenario SQL files, adjudicated by OP SIMU on reload. MCP is the only interface between the LLM and the database — in this sense a narrow waist, since every interaction passes through it — and the toolchain remains the oracle that adjudicates every artefact. The pipeline validates only rules discharged against the JSON track model produced by sql2json and against the decoded Packets 5/12/21/27. This scope is bounded by 43 of the 147 catalogued Subset rules. We have authored 82 rules against this scope: 22 Subset-derived and 60 engineering and integrity rules (see Sect. 5.2). The remaining 104 Subset rules require bit-exact payload decoding, 4
FastMCP, https://github.com/jlowin/fastmcp, an open-source Python framework for Model Context Protocol servers.
OBU simulation, or operational knowledge, and are out of scope. We state this scope invariant explicitly: no claim made here extends beyond the 43-rule scope.
5
Case Study and Results
5.1
Experimental setup
The sql2json bridge has been exercised end-to-end on three OP SIMU reference databases (L1 FS Scenario, Webinar BL3 2026 and CLEARSY Demo v360, nine tracks), producing their .json/.jsonsd pair; a deliberately-seeded KO dataset, complex station ko, serves as negative control. As of the present writing, the rule corpus consists of 82 .rule files with their supporting .ic, .acc and .cv auxiliaries, authored by Claude under human review. Out of these 82 rules, 22 are directly derived from clauses of the UNISIG Subsets. The remaining 60 are engineering guidelines and internal-integrity rules that do not correspond to a specific Subset clause; if violated, they would lead the simulator either to reject the scenario or to exhibit ambiguous behaviour (for example switch-edge consistency, balise-abscissa non-negativity, platform or waking-zone overlap, joint uniqueness, Subset-36 reserved-value ranges). The solver discharge of the 42 rules authored in the initial batch has been executed end-to-end on the seeded control dataset, and a first sweep of three telegram-content rules on the L1 FS Scenario production database has been completed. The remaining production-database sweep is reserved for the immediate near-term step. The CLEARSY Data Solver is configured with the Caval 2.6.0-rc3 rule engine (standalone mode) and the ProB 1.12.2-fix1 constraint solver as back-end, with default fractional digits = 2. Data provenance and confidentiality. All data used in this study is nonconfidential. The UNISIG Subsets are publicly available from the European Union Agency for Railways; the three OP SIMU databases are CLEARSY’s internal demonstration and webinar scenarios (authored in-house for training and demonstration purposes), not customer project data. The LLM (Claude) was operated through a controlled MCP interface exposing only these demonstration assets: no customer data, proprietary configuration, or safety case from a CLEARSY project was shared with the model at any stage. 5.2
Coverage of the Subsets
The 147 rules extracted from Subsets 026, 036, 044 and 085 are partitioned as shown in Table 1. This partition is the coverage denominator used throughout the paper. Of the 43 rules tractable from JSON (Table 1), 22 are today formalised as .rule files and discharged by the solver; a further 21 tractable rules remain to be authored (notably the cross-edge balise-distance checks that require path-traversal intermediate constructions, and the more complex packet parsing for incremental SSP distances and MA sections). The 82-rule corpus mentioned in Sect. 5.1 is
Table 1: Classification of the 147 rules; 43 are tractable from the JSON track model produced by sql2json. Category
Count Tractable? Why
Track geometry
43
Yes
Telegram content
45
No
Onboard behaviour Operational
30 19
No No
Encoding
10
No
Total
147
Edges, nodes, signals, balise groups, distances Requires decoding balise telegram hex (packets) Needs OBU simulation (modes, braking) Procedures, national values, session management Bit-level CRC, scrambling, substitution (SS-036) 43 tractable (29.3%)
therefore composed of 22 Subset-derived rules (a subset of Table 1’s 43 tractable rules) plus 60 engineering guidelines and internal-integrity rules outside the catalogue, which govern dataset-internal consistency rather than Subset clauses; 82 – 22 = 60. Why the other four classes are excluded. The 104 non-tractable rules are out of scope for distinct reasons: Telegram content (45) requires bit-level payload decoding beyond our field-level decoder for packets 5/12/21/27; Onboard behaviour (30) requires an executable OBU model, outside a static trackside check; Operational (19) lives outside the trackside dataset (procedures, session handover, national values); Encoding (10) is enforced by the trackside encoder hardware and a separate conformance campaign (SS-036 §8: CRC, scrambling, substitution). The pipeline adjudicates the what of ETCS data; the excluded classes adjudicate the how of its transport, interpretation and operation. 5.3
Validation results
Seeded control dataset. On complex station ko, out of 42 rules applied, 28 reported OK, 7 KO (each KO matching one of the violations deliberately seeded in the control dataset) and 7 NONE (the dataset did not contain any item relevant to the rule; a scenario with no loops cannot be tested against Rule Loop Max Length). The seven KO rules are BG NPIG Order, Balise Within Edge, Linking {Distance Range L1, Target Exists}, MA VMAIN Positive, SSP Speed Positive and Signal DangerPoint Positive; the seven NONE rules cover loops, joints, SvL hierarchy, uniqueness names and waking zones. The consolidated report lists 8 counterexamples across the seven KO rules; 43 SIL4 verify statements passed, 0 errors, 0 warnings; total wall clock ≈ 5 min, per-rule 7–11 s. Two observations matter. First, the 42-rule sweep is compatible with an interactive authoring loop. Second, NONE is a first-class outcome: when a rule has no applicable data, the solver
says so rather than returning a spurious OK. A rule silent for lack of data is not a rule that has adjudicated anything, which matters for the fencing stance of this paper. The pending sweep on the three production-intent OP SIMU databases is expected to yield a materially lower KO rate, since those databases are authored by CLEARSY and well-formed by construction. Its value therefore lies less in finding errors and more in measuring wall-clock scaling, proof-obligation counts and NONE-distribution at realistic topological complexity. First production-database sweep. A first discharge on L1 FS Scenario (singletrack Level 1 Full-Supervision, 3 signals, 3 balise groups, 6 balises) exercised three telegram-content rules (Rule MA EOA Or LOA, Rule MA Section Count Valid, Rule SSP Has End Marker). All three reported OK, 0 counter-examples, 8 s per rule. This is our first solver run on a production-intent OP SIMU database; the full 82-rule sweep on the three production databases remains the immediate near-term step. Problems encountered while developing the pipeline. Three classes of issue surfaced during pipeline development; their resolution shaped the final design described in Sect. 4. JSONSD-driven typing and scaling: the solver infers types from the JSONSD (e.g. NID BG is string, not integer) and multiplies number-typed fields by 10default fractional digits ; early drafts of distance rules used the wrong type or unscaled values and failed until aligned with the schema. Referential integrity enforced at load time: the referencedTypes field causes the solver to reject data with dangling references before any rule runs. This made “balise references a valid edge”-style rules redundant and required that even our deliberately-KO test tracks remain loadable (otherwise a test track breaking referential integrity would be rejected before reaching the rule under test). OP SIMU MD5 fingerprints: two MD5 fields are computed via the genmd5 utility on the Red Hat Enterprise Linux (RHEL) 7 reference VM; LLM-generated scenarios that omit this step are rejected by OP SIMU on reload, which is the documented fence event of Sect. 5.6. Each issue was caught by the solver, by the OP SIMU loader, or by human review, and logged in the project’s internal record. 5.4
Error taxonomy
Five durable classes of error mode emerge from the KO verdicts on the complex station ko control, each anchored to a Subset clause and at least one KO rule: E1 Balise-group geometry (SS-036 §7.5, SS-026 §3.4; BG NPIG Order); E2 Positionality (§3.6; Balise Within Edge); E3 Linking inconsistency (§3.4; Linking Distance Range L1, Linking Target Exists); E4 Positivity/range (§3.11, §3.12; MA VMAIN Positive, SSP Speed Positive, Signal DangerPoint Positive); E5 Coverage incoherence (§3.11, §3.12; addressed by a rule but not exercised by the control dataset). A sixth class, uniqueness, is addressed by at least one rule in the 82-rule corpus but returned NONE on
the control. These classes are intentionally model-independent, and the 82-rule implementation (22 Subset-derived plus 60 engineering/integrity) is one instance of the partition. 5.5
Human-in-the-loop review
The fencing stance rests on two lines of defence: the solver adjudicates every B-math predicate, and a human reviewer adjudicates every LLM-authored or machine-generated artefact that feeds, shapes or interprets that adjudication. The solver catches what is formally wrong; the reviewer catches what is silently misaligned with intent or with the Subsets. It is important to note that human cross-verification is not an invention of this work: CLEARSY’s current industrial data-validation process already requires that rules, intermediate constructions, accessors and the structured input artefacts (JSON, XML when applicable) be reviewed by an engineer other than their designer before being retained. What the present paper adds is the extension of that established cross-verification discipline to LLM-authored artefacts, and its codification into a governance table aligned with EN 50716 tool-qualification expectations. Table 2 makes explicit which artefacts of the chain are reviewed, by whom, against what reference, and what triggers a reject-and-redo cycle. The review targets fall into three families: authoring artefacts produced by the LLM and read into the solver (rules, intermediate constructions, accessors, compute variables, the mapping from Subset clauses to rule identifiers); transport artefacts produced by the DataProcessor and OP SIMU (SQL dumps, JSON/JSONSD pairs, generated scenarios to reload); and adjudication artefacts produced by the solver (OK/KO reports, counter-examples, NONE verdicts). Each artefact has a canonical reference: the UNISIG Subsets for rule content, the DataProcessor design documentation for schema conventions, the OP SIMU simulator itself for scenario loadability, and the project’s internal data-validation conventions for engineering-guideline rules. The eight review targets are not ad hoc: they emerge from the three families above with one target per artefact class that materially carries the fencing argument, and together they cover every artefact in the pipeline of Fig. 1 whose review affects an oracle verdict or its interpretation. Table 2 lists those eight targets with their reviewer, reference and rejection trigger. The table is the governance spine of an EN 50716-compatible tool-qualification argument for the pipeline: every LLM-authored artefact has a reviewer and a reject-and-redo loop before it is retained, and every oracle verdict is humanadjudicated before an engineering action follows. The human-review campaign is ongoing at the time of writing; the quantitative results (counts of accepted, rejected and reworked artefacts per review target; typical rework time; reviewer effort per authored rule; most frequent rejection triggers observed across the eight targets) are deferred to a dedicated follow-up paper, where they will be reported together with the outcome of the full 82-rule solver sweep on the three OP SIMU production databases. The present paper establishes the governance structure; the quantitative evidence that populates it comes next.
.ic intermediate constructions and .acc B-math reviewer accessors authored by the LLM
.cv compute variables (auxiliary impera- B-math reviewer tive)
OP SIMU SQL dump received from the Signalling engineer simulator (provenance)
.json / .jsonsd produced by sql2json DataProcessor engineer SQL dump as authoritative Round-trip mismatch; inferred (schema and content fidelity) source; DataProcessor design waking zone disagrees with the spec SQL; type declared integer where JSONSD expects string
LLM-generated scenarios proposed for Signalling engineer reload into OP SIMU
Solver counter-examples (KO rule reports) B-math reviewer; before engineering action nalling engineer
H3
H4
H5
H6
H7
H8
sig- The rule under evaluation; the Counter-example reflects a rule Subset clause it encodes defect rather than a data defect; localisation ambiguous; engineering remediation not derivable
OP SIMU on reload (the simula- OP SIMU refuses to load; semantor itself) tic anomaly visible in a simulator run
CLEARSY in-house Unknown origin; customer data demonstration-scenario cat- inadvertently included; MD5 finalogue gerprints missing
CAFE/Caval .cv semantics doc- Unintended side-effect; off-by-one umentation in loop; numeric overflow at scaled units
Reference JSONSD schema; Accessor arity wrong; .ic conproject accessor conventions fuses edge-local and global abscissa; type signature mismatches the JSONSD
Corresponding Subset clause and Predicate over-approximates or the project’s B-math style guide under-approximates the clause; solver type error; unit mismatch
.rule drafts authored by the LLM B-math reviewer (FOR / WHERE / VERIFY predicates in Bmath)
Rejection trigger
H2
Reference
Subset-clause to rule-identifier mapping Signalling engineer; B- UNISIG Subsets (026, 036, 044, Clause not covered, misinter(traceability table linking each Subset math reviewer 085) preted, or rule covers more than clause in scope to one or more .rule files) its clause states
H1
Reviewer
Artefact under review
#
Table 2: Human-review targets in the ValidAItion chain. Results columns are populated in a follow-up study.
5.6
LLM-in-construction: return of experience
The LLM accelerated ingestion of the Subsets into the 147-rule catalogue, the drafting of .rule and .ic artefacts from Subset clauses, the Lark grammars, and the SQL schema synthesis feeding sql2json. It also produced plausiblebut-wrong artefacts caught by the toolchain or by a reviewer (wrong accessor arity, edge-local vs global abscissa confusion, over-approximated BG-distance predicates). The archetypal fence event is a scenario SQL file authored by Claude that was syntactically well-formed, parsed correctly, passed the round-trip, yet OP SIMU refused to load it: the LLM produced a plausible artefact, the oracle rejected it, and no invalid data entered the project. The pragmatic lesson is that an LLM is useful for drafting and exploration, not a substitute for the toolchain’s adjudication and for systematic human review.
6
Blueprint: Fencing AI with B via MCP
Sections 4 and 5 described the LLM+MCP+oracle loop used to build ValidAItion. The same architecture is a natural substrate for the use phase: a signalling engineer who is not a formal-methods expert asks natural-language questions (“which balise groups violate the minimum-distance rule?”, “propose a gradient adjustment for MA extent over route R17”), the LLM consults the database through the MCP server and proposes a concrete edit, and the solver discharges the affected rules before the edit is committed. The diagnostic returns to the engineer in natural language, grounded in a structured solver report. Beyond what exists today (the nine or more create-read-update-delete (CRUD) tools on OP SIMU databases mentioned in Sect. 5.6, the LLM-authored rule corpus, and one documented fence event), the blueprint adds a bidirectional tool surface (invoke caval validation(rule id, scope) and explain ko(report id) so the LLM can drive the oracle and reason over its diagnostics), an orchestration pattern (LLM plans, oracle adjudicates, engineer confirms), and a traceability log pairing every LLM proposal with its oracle verdict, which is the basic artefact for controlled AI assistance under EN 50716 [7] tool qualification and AI Act Article 14 [11]. Residual risks are coverage holes (an unformalised rule cannot fence an LLM error in its class, hence the coverage denominator of Sect. 5.2), oracle soundness (a wrong rule lets errors through, rule review remains a human responsibility), LLM capability drift, and prompt injection through engineer input. On the CLEARSY Data Solver side, the pattern calls for structured JSON diagnostics, incremental validation (re-discharging only the rules affected by an edit), and a reusable library of .ic / .acc primitives so that rule authoring stays cheap as coverage grows.
7
Related Work
7.1
Railway formal methods and ETCS
Closest to our tool stack, Hansen and Leuschel et al. showed that a formal B model executed by ProB can run at runtime to control real trains in an ETCS
Hybrid Level 3 field demonstration with Thales, with per-event response times of 0.03–0.14 s [14,15]; Dghaym et al. develop a parallel Event-B modelling with iUML-B [9], and Leuschel and Nayeri extend the approach to Level-3 moving block [21]. These works establish that ProB, the solver back-end used in the CLEARSY Data Solver, is already accepted in safety-critical railway validation contexts. Broader surveys are given in [12,2]. In the dynamic-behaviour line, Saddem-Yagoubi et al. use UPPAAL timed automata for the ETCS L3 Loss-ofTrain-Integrity scenario [25]. Our work differs in scope from all of these: we do not prove the ETCS protocol itself and we do not target dynamic behaviour; we validate deployed trackside data against a rule set drawn from the Subsets, on an industrial simulator database.
7.2
The B mathematical language for ETCS and railway data
Within the B tradition, the DTVT work reported in [16] and the more recent ERTMS simulation effort in [17] are the most immediate predecessors of ValidAItion; both use the B mathematical language to express data-validation predicates rather than B machines to produce software. The CLEARSY Safety Platform report [20] and the First Twenty-Five Years of Industrial Use of the B-Method [4] describe, separately, the industrial host platform that makes the B method (machines, refinements and implementations) viable at SIL 4 for safetycritical software, which is a distinct activity. We extend the data-validation line by connecting the CLEARSY Data Solver to the OP SIMU database through an automatic bridge, and by publishing an explicit coverage denominator over Subsets 026/036/044/085.
7.3
LLM + formal methods, AI in rail
LLM-assisted formal methods are an active area in 2024–2026 but remain largely generic. A broader survey of pragmatic AI uses in formal-methods railway projects at CLEARSY (LLM-assisted specification synthesis, AI-assisted B proof tactics, machine-learning perception fenced by a formally verified safety controller [18], and multimodal-LLM transformation of relay diagrams into propositional logic) is given in [19]; the present paper drills into one of those activities, ETCS data validation. Within the ProB / B-method neighbourhood, Vu, Dunkelau and Leuschel validate reinforcement-learning agents with safety shields [26], Gruteser et al. combine formal models, safety shields and certified control for AI-based train systems [13], and Rossbach et al. propose an evaluation methodology for AI in autonomous railway systems [24]. Capozucca et al. [5] and Dixon et al. [10] explore LLM-assisted B pedagogy and neural-network verification respectively. Our distinctive element is that the LLM/MCP loop was used during construction of the rule corpus and the parsers, not as an end-user feature, with the CLEARSY Data Solver over B-math predicates as the adjudicating oracle backed by systematic human review.
7.4
Differentiation against the closest 2025 works
Two 2025 railway-community papers are closest in framing to the present work and deserve explicit differentiation. Yar, Idani, Ledru and Collart-Dutilleul [27] propose an executable-DSL layer over B specifications so that domain experts can animate and validate signalling models without reading B text. The contribution is a validation interface for signalling behaviour models. Our work differs on three axes: (i) our target is ETCS trackside data (balise groups, linking, SSP, gradients) drawn from an SQL simulator database, not signalling behaviour models; (ii) we use the B mathematical language directly as a predicate language over JSON data rather than animating B specifications; (iii) our engineer-in-the-loop bridge is a conversational LLM+MCP interface, not an executable DSL. Reiter, Wetenkamp, Schmid, Kretzschmar and Iffländer [23] target the chain from natural-language signalling requirements to formal specifications and then to verified code. Their concern is requirement-to-code traceability and software synthesis. Our concern is the complementary problem: we do not synthesise software; we validate data, and we do so for ETCS Subset-026/036/044/085 artefacts authored from an existing industrial simulator. Where their toolchain produces code, ours produces an OK/KO verdict over a deployed dataset; both chains need tool qualification under EN 50716 [7], but they qualify different things. Relative to these two, the distinctive elements of ValidAItion are: the datacentric rather than behaviour-centric or code-centric framing, the SQL-to-B-math bridge anchored on OP SIMU, and the LLM-in-construction return of experience with a documented fence event (Sect. 5.6).
8
Conclusion
We have reported on the current status of ValidAItion, an ongoing industrial research effort at CLEARSY that connects OP SIMU to the CLEARSY Data Solver and applies rules expressed in the B mathematical language to ETCS trackside data. The paper makes three contributions: (i) an industrial pipeline with an automatic SQL-to-JSON bridge, a telegram decoder for Packets 5/12/21/27, and an executable corpus of 82 rules run under the solver (Sect. 4, Sect. 5); (ii) a falsifiable coverage classification of the 147 rules drawn from the Subsets, with 43 tractable from the JSON track model (22 authored so far) and 104 out of scope for explicitly justified reasons (Sect. 5.2); (iii) an LLM+MCP construction methodology fenced by the solver and by systematic human review (Sect. 5.5), extended to a blueprint for engineer-in-the-loop data validation (Sect. 6). A model-independent error taxonomy of five durable classes underpins the empirical spine. One documented fence event illustrates the stance we advocate: OP SIMU refused a syntactically valid LLM-generated scenario, and no invalid data entered the project. In safety-critical ETCS data work, formal rules in the B mathematical language must remain the source of truth: AI proposes, the formal oracle disposes, the human confirms.
What is done, in progress, and planned. Done. The pipeline is operational end-toend on the seeded control dataset (42 rules, 28 OK, 7 KO, 7 NONE) and on a first production database (three telegram-content rules on L1 FS Scenario). Rule authoring has reached 82 rules; the coverage denominator, the error taxonomy and the human-review table are established. In progress. The human-review campaign is underway on the eight review targets of Table 2; the full 82-rule solver sweep on the three OP SIMU production databases is being set up; additional Subset rules are being formalised, in particular the cross-edge balise-distance checks and the incremental SSP / MA-section packet parsing that will close the gap towards the 43 tractable clauses. Planned. A follow-up paper will report the quantitative outcome of the human-review campaign (acceptance / rejection / rework counts per target) and of the full solver sweep (per-database OK/KO/NONE distributions, wall-clock scaling, proof-obligation counts), together with the tool-qualification argument for the currently uncertified transport layer under EN 50716. Longerterm work engages with the certification community on the implications of an LLM-assisted but oracle-fenced and human-reviewed data-validation workflow, and characterises the additional human-review effort induced by running a smaller, privacy-preserving LLM on-premises rather than a hosted frontier model. A further research direction concerns scenario intent. The current pipeline verifies that a scenario’s trackside data complies with the Subsets, but it does not assess whether the scenario achieves the pedagogical or testing objective for which it was designed. For example, a scenario intended to train drivers to handle a telecommunication loss and to use the Override button to resume their journey requires an ETCS Level 2 topology; the same scenario is unrealisable on a Level 1 track, where no radio session exists and Override has no operational meaning. An LLM with sufficient knowledge of ETCS operational modes and of the training curriculum could assist the scenario designer by checking the feasibility of the stated intent against the topology before the scenario is authored in detail, and by flagging mismatches early. This would extend ValidAItion from data compliance (are the rules satisfied?) to intent adequacy (can this topology support the intended training objective?).
Confidentiality and the private-LLM trade-off. The present study relies exclusively on non-confidential inputs (public UNISIG Subsets, CLEARSY’s in-house demonstration databases), with a hosted frontier LLM behind a narrow MCP surface that never exposed customer data. Real customer projects require running the LLM on private or on-premises infrastructure, as reported in [19]. Open-weight models deployable on private infrastructure (Llama, Mistral, Qwen families) trail hosted frontier models (Claude, GPT, Gemini) by a measurable margin on head-to-head preference evaluations [8] and on reasoning, code and instructionfollowing benchmarks [22]. A fenced architecture partially compensates: the oracle catches a plausible-but-wrong artefact regardless of proposer capability, and the quantitative question becomes not “can a local LLM be trusted?” but “how much human-review effort does a weaker proposer add?”, a natural follow-up study.
Acknowledgements The authors thank the CLEARSY data validation team for the industrial context and the OP SIMU access, and acknowledge the companion work presented at FM 2026 [19].
References 1. Abrial, J.: The B-book - assigning programs to meanings. Cambridge University Press (2005) 2. ter Beek, M.H., Chapman, R., Cleaveland, R., Garavel, H., Gu, R., ter Horst, I., Keiren, J.J.A., Lecomte, T., Leuschel, M., Rozier, K.Y., Sampaio, A., Seceleanu, C., Thomas, M., Willemse, T.A.C., Zhang, L.: Formal methods in industry. Formal Aspects of Computing 37(1) (2024) 3. Bureau d’Enquêtes sur les Accidents de Transport Terrestre: Rapport d’enquête technique sur la survitesse d’un TGV à la milesse (72) le 22 décembre 2019 sur la LGV bretagne – pays de la loire. Tech. Rep. 2020-01, BEA-TT (2020), https://www.bea-tt.developpement-durable.gouv.fr/IMG/ pdf/rapport_beatt_2020_01.pdf, recommendation to use verification, testing and formal-proof tools in the assessment of ETCS data validation 4. Butler, M., Körner, P., Krings, S., Lecomte, T., Leuschel, M., Mejia, L.F., Voisin, L.: The first twenty-five years of industrial use of the B-method. In: ter Beek, M.H., Ničković, D. (eds.) Formal Methods for Industrial Critical Systems. pp. 189–209. Springer International Publishing, Cham (2020) 5. Capozucca, A., Yampolskyi, D., Goldberg, A., Cristı́a, M.: Do AI assistants help students write formal specifications? a study with ChatGPT and the B-Method. In: IEEE 37th Int’l Conference on Software Engineering Education and Training (CSEE&T 2025). pp. 19–29 (2025) 6. CENELEC: EN 50128: Railway applications – communication, signalling and processing systems – software for railway control and protection systems (2011), standard 7. CENELEC: EN 50716: Railway applications – requirements for software development (2023), successor of EN 50128 8. Chiang, W.L., Zheng, L., Sheng, Y., Angelopoulos, A.N., Li, T., Li, D., Zhu, B., Zhang, H., Jordan, M.I., Gonzalez, J.E., Stoica, I.: Chatbot arena: An open platform for evaluating LLMs by human preference. In: Proceedings of the 41st International Conference on Machine Learning (ICML 2024). PMLR, vol. 235 (2024), https://proceedings.mlr.press/v235/chiang24b.html 9. Dghaym, D., Dalvandi, M., Poppleton, M., Snook, C.: Diagram-led formal modelling using iUML-B for hybrid ERTMS level 3. In: Abstract State Machines, Alloy, B, TLA, VDM, and Z. ABZ 2018. Lecture Notes in Computer Science, Springer (2018), https://eprints.soton.ac.uk/417755/1/paper_abz2018.pdf 10. Dixon, C., Sheridan, M., et al.: Modelling and verifying robotic software that uses neural networks. In: Formal Methods (FM 2023). Lecture Notes in Computer Science, vol. 14157. Springer (2023) 11. European Parliament and Council: Regulation (EU) 2024/1689 – artificial intelligence act – article 14 (human oversight) (2024) 12. Fantechi, A., Gnesi, S., Ferrari, A., et al.: Models for formal methods and tools: the case of railway systems. Software and Systems Modeling (2025)
13. Gruteser, J., Rossbach, J., Vu, F., Leuschel, M.: Using formal models, safety shields and certified control to validate AI-based train systems. In: Formal Methods for Autonomous Systems (FMAS 2024). EPTCS (2024) 14. Hansen, D., Leuschel, M., Körner, P., Krings, S., Naulin, T., Nayeri, N., Schneider, D., Skowron, F.: Using a formal B model at runtime in a demonstration of the ETCS hybrid level 3 concept with real trains. In: Abstract State Machines, Alloy, B, TLA, VDM, and Z. ABZ 2018. Lecture Notes in Computer Science, Springer (2018), proB executing a formal B model at runtime to control real trains during the Thales ETCS hybrid L3 field demonstration 15. Hansen, D., Leuschel, M., Körner, P., Krings, S., Naulin, T., Nayeri, N., Schneider, D., Skowron, F.: Validation and real-life demonstration of ETCS hybrid level 3 using a formal B model. International Journal on Software Tools for Technology Transfer 22(3) (2020) 16. Lecomte, T.: Formally checking large data sets in the railways. In: Proceedings of the DTVT / railway data-validation workshop series (2012), CLEARSY DTVT methodology and tooling 17. Lecomte, T.: Formal validation and ERTMS simulation. In: Leveraging Applications of Formal Methods, Verification and Validation. ISoLA 2024 – DisCoRail track. Lecture Notes in Computer Science, Springer (2024) 18. Lecomte, T.: Formal development of a safety controller for machine learning outputs in vital railway systems. In: ter Beek, M.H., Teixeira, L. (eds.) Formal Methods: Foundations and Applications. pp. 196–206. Springer Nature Switzerland, Cham (2026) 19. Lecomte, T., Almeida, D., Maury, N.: Pragmatic uses of AI in formal methods-based railway projects: Early lessons and perspectives. In: FM 2026 – 26th International Symposium on Formal Methods, Tokyo, Japan. Lecture Notes in Computer Science, Springer (2026), extended abstract; companion paper to the present submission 20. Lecomte, T., Deharbe, D., Fournier, P., Oliveira, M.: The CLEARSY safety platform: 5 years of research, development and deployment. Science of Computer Programming 199, 102524 (2020) 21. Leuschel, M., Nayeri, N.: ETCS level 3 moving block: Modelling, visualisation and proof. In: Reliability, Safety, and Security of Railway Systems. RSSRail 2023. Lecture Notes in Computer Science, Springer (2023) 22. Liang, P., Bommasani, R., Lee, T., et al.: Holistic evaluation of language models. Transactions on Machine Learning Research (TMLR) (2023), https://openreview. net/forum?id=iO4LZibEqW, live leaderboard at https://crfm.stanford.edu/ helm/ 23. Reiter, F., Wetenkamp, R., Schmid, R., Kretzschmar, R., Iffländer, L.: Towards an end-to-end toolchain for traceable and verifiable railway signalling specifications. In: Rigorous State-Based Methods. ABZ 2025. Lecture Notes in Computer Science, vol. 15728. Springer (2025) 24. Rossbach, J., De Candido, O., Hammam, A., Leuschel, M.: Evaluating AI-based components in autonomous railway systems: A methodology. In: KI 2024: Advances in Artificial Intelligence. Lecture Notes in Computer Science, vol. 14992. Springer (2024) 25. Saddem-Yagoubi, R., Beugin, J., Ghazel, M.: ERTMS/ETCS L3: Usable formal models for the “loss of train integrity” operation scenario. In: Verification and Evaluation of Computer and Communication Systems. VECoS 2024, Djerba, Tunisia, October 16–18, 2024, Proceedings. pp. 174–188. Lecture Notes in Computer Science, Springer (2024), hAL hal-04997909; project PERFORMINGRAIL
26. Vu, F., Dunkelau, J., Leuschel, M.: Validation of reinforcement learning agents and safety shields with ProB. In: NASA Formal Methods (NFM 2024). Lecture Notes in Computer Science, Springer (2024) 27. Yar, A., Idani, A., Ledru, Y., Collart-Dutilleul, S.: Bridging formal verification and domain validation in railway systems. In: Reliability, Safety, and Security of Railway Systems. RSSRail 2025, Pisa, Italy, November 26–28, 2025, Proceedings. Lecture Notes in Computer Science, vol. 16236. Springer (2025)