LM2Alloy：研究用于生产软件自动测试推导的大语言模型生成的形式规范
LM2Alloy: Investigating LLM-Generated Formal Specifications for Automated Test Derivation in Production Software
浏览论文内容
中文总结 AI 辅助
该研究探索用大语言模型从需求文档和生产源代码生成Alloy形式规范及推导可执行测试用例，在Flipper和Cerberus库上评估，发现能揭示约束级缺陷，基于代码的规范方差更低，为生产软件自动测试推导提供了新方法。
中文摘要 AI 辅助
我们进行了一项探索性研究，旨在利用大语言模型（LLMs）从需求文档和生产源代码生成Alloy形式规范，并从这些规范中推导可执行测试用例。我们在两个真实的开源Python库上进行评估：Flipper（一个功能特性标志管理系统）和Cerberus（一个数据验证库）。在这两种情况下，大语言模型都生成了可行的Alloy规范和可执行测试，无需任何人工修正。对于Flipper，我们的流程发现了现有测试套件遗漏的一个真正的错误：该库会静默接受重复的标志名称，这直接与记录的唯一性要求相矛盾。一个直接的大语言模型基线（从相同的README生成测试但跳过Alloy步骤）在所有三次独立运行中实现了68%的分支覆盖率，但未能发现这个错误。这表明引入形式化中间表示可以揭示面向覆盖率生成可能遗漏的约束级缺陷。对于Cerberus，基于代码生成的规范捕捉到了基于文档生成的规范遗漏的关于大小类型的隐式抽象，从而产生了另外两个测试。在这两个库中，基于代码的规范在测试生成方面的方差（平均标准差 = 2.15）低于基于文档的规范（平均标准差 = 5.0），不过这是否具有普遍性仍是一个悬而未决的问题。
英文摘要
We present an exploratory study on using Large Language Models (LLMs) to generate Alloy formal specifications from both requirements documentation and production source code, and to derive executable test cases from those specifications. We evaluate on two real open-source Python libraries: Flipper, a feature flag management system, and Cerberus, a data validation library. In both cases, the LLM produced workable Alloy specifications and executable tests without any manual correction. For Flipper, our pipeline uncovered a genuine bug that the existing test suite had missed: the library silently accepts duplicate flag names, directly contradicting its documented uniqueness requirement. A direct LLM baseline--generating tests from the same README but skipping the Alloy step--achieved 68% branch coverage yet failed to catch this bug across all three independent runs. This suggests that introducing a formal intermediate representation can surface constraint-level defects that coverage-oriented generation may miss. For Cerberus, the code-derived specification captured an implicit abstraction over sized types that the documentation-derived spec omitted, producing two additional tests. Across both libraries, code-based specifications showed lower variance in test generation (mean SD = 2.15) than documentation-based ones (mean SD = 5.0), though whether this generalises remains an open question. Index Terms--formal specifications, Alloy, large language models, automated testing, specification drift, software validation.
