实时系统的可调度性分析对于系统认证至关重要，但现有的测试方法通常通过手工证明开发，难以扩展、验证和维护。PROSA/ROCQ中的机化验证提供了一个严格的替代方案，但手动构造这样的证明需要大量的领域专业知识和证明工程努力。近年来，大型语言模型（LLMs）在各个任务中取得的成功使它们成为生成PROSA/ROCQ脚本的有力候选者。然而，目前的LLMs通常缺乏正确使用PROSA建模抽象和证明模式所需的PROSA特定知识。本文介绍了PROVE-RT，一个LLM辅助框架，用于生成PROSA/ROCQ脚本以机化实时系统文献中的可调度性分析。PROVE-RT通过依赖感知的非正式草图、从处理的PROSA文档中检索、分阶段的骨架生成和证明完成来指导生成。我们从1,191篇实时系统论文中构建了一个面向机化的语料库，包含13,134个带有依赖信息的非正式草图。在一个精心策划的评估集中，直接提示最先进的LLMs不能可靠地生成有效的PROSA机化，而PROVE-RT实现了44.7%的成功率。这些结果表明，检索引导和分阶段的LLM辅助可以改进PROSA/ROCQ中可调度性分析的自动机化。 博主点评： PROVE-RT 框架通过利用大型语言模型的能力，显著提高了实时系统中可调度性分析的机化效率和准确性，这对提高实时系统的可靠性和安全性具有重要意义。