AI 中文总结
本文报告CLEARSY公司ValidAItion项目进展，将ERTMS操作模拟器与CLEARSY数据求解器桥接，用B语言验证ETCS数据，Claude生成规则库，工具链与人工审核裁决，形式化规则为事实来源，大模型为受管控助手。
AI 中文摘要
大型语言模型能否参与ERTMS/ETCS数据的生成与验证，同时不破坏CENELEC EN 50128/50716标准要求的认证论证？ERTMS/ETCS是分布式安全关键系统（含轨旁、车载、无线闭塞中心），其行为由UNISIG子集的大量数据参数化，该数据中的错误会在分布式架构中传播。本文报告了CLEARSY公司ValidAItion项目正在进行的工业研究进展，该项目将ERTMS操作模拟器与CLEARSY数据求解器桥接，并对轨旁数据应用B数学语言表达的规则。构建过程中，大语言模型Claude通过模型上下文协议服务器生成规则库和解析器；每条提案都会被下游工具链和系统性人工审核裁决，工具链已拒绝了一个语法有效但语义非法的生成场景。本文的贡献是架构与工业层面的，而非算法层面：该工作结合了CLEARSY已在用的框架（CLEARSY数据求解器、ERTMS操作模拟器）与对话式创作循环，并未提出新的形式化方法。这是一份进展报告：规则覆盖范围正在扩大，人工审核活动正在进行，定量结果将另行发表。基于目前收集的证据，本文认为，B数学语言的形式化规则必须作为事实来源，而大语言模型仅作为分布式安全关键铁路系统中的受管控助手：AI提出方案，形式化权威裁决，人工确认。
英文摘要
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.
CommentsSubmitted and accepted to DisCoRail @ISOLA 2026
