跳转至

文章背景与核心概要

实时系统的认证传统上依赖于手写的可调度性分析纸面证明，这些证明不仅难以扩展、验证和维护，还容易出错。尽管像 PROSA/ROCQ 这样的机械化验证框架提供了一种严谨的替代方案，但手动构建证明需要极高的领域专业知识和繁重的证明工程投入。虽然大语言模型（LLM）在脚本生成任务中展现出巨大潜力，但现有最先进的模型往往缺乏关于 PROSA 建模抽象和证明模式的专业知识。

为了解决这一痛点，本文推出了 PROVE-RT——一个旨在自动为实时系统生成 PROSA/ROCQ 脚本的 LLM 辅助框架。PROVE-RT 通过依赖感知的非形式化草图（informal sketches）、文档检索、分阶段骨架生成以及证明补全等多项技术协同工作。该研究构建了一个包含 1,191 篇实时系统论文和 13,134 个带依赖信息的非形式化草图的机械化导向型语料库。在精选的评估集上，PROVE-RT 取得了 44.7% 的成功率，显著优于直接使用大语言模型提示词的传统方法。

PROVE-RT: Generating Mechanized Theorem Prover Scripts for Real-Time Systems using LLMs

Summary

Certifying real-time systems traditionally relies on pen-and-paper proofs for schedulability analysis, which are difficult to scale, validate, and maintain. While mechanized verification frameworks like PROSA/ROCQ offer a rigorous alternative, manually constructing proofs requires immense domain expertise. Although Large Language Models (LLMs) are promising tools for script generation, state-of-the-art models often lack specialized knowledge regarding PROSA's modeling abstractions.

This paper introduces PROVE-RT, an LLM-assisted framework designed to automatically generate PROSA/ROCQ scripts for real-time systems. PROVE-RT utilizes dependency-aware informal sketches, documentation retrieval, staged skeleton generation, and proof completion. Trained on a corpus of 1,191 real-time systems papers containing 13,134 informal sketches, PROVE-RT achieves a 44.7% success rate on a curated evaluation set, significantly outperforming direct LLM prompting.

Document Metadata

  • arXiv ID: arXiv:2608.12762 [cs.AI]
  • Primary Subject: Artificial Intelligence (cs.AI)
  • Submission Date: August 13, 2026
  • Authors:
  • Sadat Shahriyar
  • Shareef Ahmed
  • Abdullah Al Arafat

Abstract

Schedulability analysis is essential for certifying real-time systems, but existing tests are often developed through pen-and-paper proofs that are difficult to scale, validate, and maintain. Mechanized verification in PROSA/ROCQ offers a rigorous alternative, yet manually constructing such proofs requires substantial domain expertise and proof-engineering effort. Recent successes of large language models (LLMs) across a wide range of tasks make them promising candidates for generating PROSA/ROCQ scripts for mechanized theorem provers. However, state-of-the-art LLMs often lack the PROSA-specific knowledge required to correctly use its modeling abstractions and proof patterns.

This paper introduces PROVE-RT, an LLM-assisted framework for generating PROSA/ROCQ scripts to mechanize schedulability analyses in real-time systems literature. PROVE-RT guides generation through dependency-aware informal sketches, retrieval from processed PROSA documentation, staged skeleton generation, and proof completion. We construct a mechanization-oriented corpus from 1,191 real-time systems papers, containing 13,134 informal sketches with dependency information. On a curated evaluation set, direct prompting of state-of-the-art LLMs fails to reliably generate valid PROSA mechanizations, whereas PROVE-RT achieves a success rate of 44.7%. These results show that retrieval-guided and staged LLM assistance can improve automated mechanization of schedulability analysis in PROSA/ROCQ.

实时系统的可调度性分析对于系统认证至关重要，但现有的测试通常通过纸面证明来开发，这些证明难以扩展、验证和维护。PROSA/ROCQ 中的机械化验证提供了一种严谨的替代方案，然而手动构建此类证明需要大量的领域专业知识和证明工程投入。大语言模型（LLM）近来在广泛的任务中取得成功，使其成为为机械化定理证明器生成 PROSA/ROCQ 脚本的极具潜力的人选。然而，最先进的 LLM 往往缺乏正确使用其建模抽象和证明模式所需的 PROSA 特定知识。

本文介绍了 PROVE-RT，这是一个 LLM 辅助框架，用于生成 PROSA/ROCQ 脚本，以实现实时系统文献中可调度性分析的机械化。PROVE-RT 通过依赖感知的非形式化草图、处理过的 PROSA 文档检索、分阶段骨架生成和证明补全来指导生成。我们从 1,191 篇实时系统论文中构建了一个面向机械化的语料库，其中包含 13,134 个带有依赖关系的非形式化草图。在精选的评估集上，直接提示最先进的 LLM 无法可靠地生成有效的 PROSA 机械化脚本，而 PROVE-RT 的成功率达到了 44.7%。这些结果表明，检索引导和分阶段的 LLM 辅助可以改进 PROSA/ROCQ 中可调度性分析的自动化机械化。