PROVE-RT：用大语言模型为实时系统生成机械化定理证明脚本

可调度性分析对实时系统认证至关重要，但现有测试通常通过纸笔证明开发，难以扩展、验证和维护。PROSA/ROCQ 中的机械化验证提供了严格的替代方案，但人工构造此类证明需要大量领域专业知识和证明工程投入。大语言模型近来在广泛任务上的成功使其成为为机械化定理证明器生成 PROSA/ROCQ 脚本的有力候选。然而，最先进的大语言模型往往缺乏正确使用 PROSA 建模抽象和证明模式所需的 PROSA 专属知识。本文提出 PROVE-RT，一个大语言模型辅助框架，用于生成 PROSA/ROCQ 脚本，以机械化实时系统文献中的可调度性分析。PROVE-RT 通过依赖感知的非形式化草图、从经处理的 PROSA 文档中检索、分阶段骨架生成和证明补全来引导生成。我们从 1,191 篇实时系统论文构建了面向机械化的语料库，包含 13,134 个带依赖信息的非形式化草图。在一个精选评估集上，直接以提示词驱动最先进的大语言模型无法可靠生成有效的 PROSA 机械化结果，而 PROVE-RT 达到 44.7% 的成功率。这些结果表明，检索引导和分阶段的大语言模型辅助可以改进 PROSA/ROCQ 中可调度性分析的自动化机械化。