多代理的模型驱动规程 LLM：可追溯系统模型的验证需求生成

软件复杂性是系统工程师面临的长期挑战。模型驱动工程 (MDE) 通过将模型视为一流的人工制品来解决这个问题，但典型的 MDE 流程跨越许多工具并生成不同系统方面的异构模型，这使得可追溯性、维护和变更管理变得困难。我们提出 RADIANT，这是一种将 MDE 与多代理 大语言模型 (LLM) 相结合的工程方法，用于完整的基于模型的系统开发，重点关注安全关键系统。根据仔细指定的需求模型，RADIANT 自动生成跨工程阶段的异构模型——概念模型、特定于领域的建模语言、一致性系统模型和行为模型——以及可执行的元素级可追溯性链接，在此基础上提供精确、自动化的变更影响分析。生成的行为模型被转换为 CSP 并通过反例驱动的修复循环进行正式验证（例如，用于死锁自由和收敛）。通过评估三个 LLM 的 RADIANT，我们发现多智能体分解可靠地提高了生成的形式工件在单智能体基线上的 \emph{句法有效性} - 以及模型代码生成允许的情况下的 \emph{可执行性} - 而语义准确性的增益取决于模型。一项六名参与者的研究表明，开发时间减少了一个数量级（$10$-$15\times$），并且未修改的管道转移到第二个域。