Model-Driven Discipline for Multi-Agent LLMs: Requirement-to-Verification Generation of Traceable System Models
Abstract Overview
This paper presents RADIANT, a requirement-driven engineering methodology that combines model-driven engineering with multi-agent large language models to generate traceable system models across multiple development phases. Starting from a manually authored requirement model, the approach generates a concept model, a domain-specific modelling language, a conforming system model, and a behaviour model, together with executable element-level traceability links. The behaviour models are translated into CSP and checked with FDR for properties such as deadlock freedom and convergence, with a repair loop driven by counterexamples. The paper evaluates the pipeline on an autonomous underwater vehicle case study, compares multi-agent and single-agent configurations across three LLMs, and examines change-impact analysis, efficiency, and transfer to a second robotic domain.
Novelty
The distinctive contribution is an end-to-end, requirement-to-verification methodology that generates heterogeneous engineering models and executable traceability links by construction, rather than recovering links after the fact. It integrates a generic multi-agent generate/check/refactor/trace architecture with formal verification and automated change-impact analysis in a unified model-driven workflow.
Results
Across three LLMs, the multi-agent decomposition consistently improved the syntactic validity of generated formal artefacts, and improved executability where the underlying model's code generation was strong enough, although semantic gains were model-dependent. On the AUV case study, the generated behaviour model was formally verified as deadlock-free and convergent, change-impact analysis achieved exact impact identification, and a six-participant study reported roughly a 10-15x reduction in development time versus manual modelling. The unchanged pipeline also successfully transferred to a second robotic domain, producing passing artefacts in all phases.
Key Points
- RADIANT uses a manually created requirement model as the sole authored input and automatically derives downstream concept, DSML, system, behaviour, and traceability artefacts.
- Its traceability mechanism is executable and element-level, enabling automated change-impact analysis across heterogeneous models rather than relying on soft or post hoc recovered links.
- The empirical evaluation shows robust gains in artefact validity from the multi-agent workflow, substantial efficiency improvements over manual modelling, and successful transfer to a second case study.