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.
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.
Large language models generate code effectively but falter in enterprise settings that demand complex business rules, particularly in rule consistency and conflict detection. This study proposes the Atomic Logic Sheet (ALS), a structured representation of business logic, injected through the Hierarchical Business Logic Injection (H-BLI) framework. Four conditions were compared on a warehouse management domain, 20 runs each: requirements only; a natural-language design document; the same content with worked examples, anti-patterns, and an explicit conflict-handling directive in prose; and that content expressed in ALS. Conflict responses were adjudicated by two independent raters (κ = 0.993 and 1.000) and cross-checked against a byte-level code comparison. Logic compliance converged near 97% whenever a design document was supplied; conflict detection separated them: 10.0% and 43.1% for the requirements-only and plain-document conditions, and 100% for both content-bearing conditions, neither of which modified code. The two notations detected conflicts identically, and where they differed, the prose condition was better, so the effect follows the content a document is obliged to carry rather than its notation. A replication under a second model reproduced the gap between the requirements-only baseline and the full treatment, and a replication on independently designed conflicts reproduced the detection result for the document conditions; neither included the prose condition, so neither reproduces the comparison between notations. Schema deviation, however, was higher under ALS. As a single-domain study, replication elsewhere remains necessary.
Man-Su Kim, Museong Choi, Miseon Shim et al.· Electronics· 0 citations
The need for custom validation capabilities to ensure that models produced by both humans and LLMs are trustworthy enough to serve as the foundation of the MBSE ecosystem is addressed.
Á. Tóth, Levente Bajczi, Ármin Zavada et al.· Proceedings of the ACM/IEEE...· 0 citations
This article introduces Eiffel-tools, a language server protocol (LSP) implementation for the Eiffel programming language that uses Large Language Models (LLMs) to aid the development of statically verified software. The tool provides various interactive and non-interactive commands to produce code and specifications. It uses language and project specific knowledge to precisely direct the LLM and verifies the output using a static verifier. It crafts rich programmatic prompts for the input and corrects or rejects the output. Furthermore, it handles the retries until the program passes verification. The tool's bug fixing capability is evaluated on 2 public datasets using 3 models. The tool can fix 76% to 95% of bugs by combining LLMs and a formal verifier depending on the model and prompts used. The results show the trade-off between the number of fixing attempts and the success rate.
Alessandro Schena, I. Mustafin, Julia Kotovich· 0 citations
This paper presents a framework integrating Knowledge Graphs and Large Language Models to support a more extensible design review environment, and demonstrates its ability to retrieve and execute existing rules from the KG, capture new requests during design, and maintain a verifiable, adaptive compliance checking system.
Maen Alnuzha, Tanya Bloch· Journal of Information Techn...· 1 citation
Results showed that long-context LLMs tended to achieve higher accuracy than smaller models, suggesting that LLMs are currently better suited to support human-in-the-loop root cause analysis than to fully automate it, and motivating further work to improve prediction accuracy for log-based RCA.
Rahmanu Hermawan, Alessio Bucaioni, Eduard Paul Enoiu et al.· Innovations in Systems and S...· 0 citations
Domain-Driven Design gives teams a shared vocabulary for complex business logic, but that vocabulary only stays useful as long as the model and the code agree with each other. In practice, they drift apart: code changes outpace the model, or model revisions never make it into the codebase. This paper presents JDomInO, a bidirectional synchronization toolchain for tactical DDD that keeps a Java codebase and its domain model connected through a shared metamodel, with the goal of keeping the two in sync as the system evolves. JDomInO generates Java code structure deterministically from a domain model (forward path) and reconstructs a domain model from existing Java code (reverse path). The forward path has been fully validated on a Hotel Management scenario covering all 12 building block types in the metamodel; the reverse path's mapping logic has passed unit testing, with end-to-end validation underway. We also outline how the structured domain model produced by JDomInO could serve as a precision context layer for AI code assistants, helping them respect aggregate boundaries and DDD semantics that raw source code alone does not convey.
Wei-Xing Zhang, Mario Herb, W. Cheng et al.· 0 citations
We use cookies to run the site and, with your consent, for analytics and to show ads.
See our Cookie Policy.
