发表机构
Carl von Ossietzky Universität Oldenburg（奥尔登堡卡尔·冯·奥西茨基大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
针对安全关键系统无中断安全软件更新的难题，提出将系统与更新交互建模为双人时间博弈、用有界SMT编码合成全局固定更新调度的方法，经自动驾驶轨迹规划器示例验证可保障所有可允许执行下的安全部署。
AI 中文摘要
在安全关键系统中，既要确保软件更新安全，又不能中断运行，也无需配置和激活冷备用硬件，这一需求因系统可用性与更新执行之间的冲突构成了一项根本挑战。本文提出一种有界SMT编码方法，用于为带有线性更新自动机、固定数量更新迁移的时间博弈合成固定全局时间的更新调度。我们将系统与更新之间的交互建模为双人时间博弈。本文的核心贡献是合成定义固定更新调度的全局时间点，该调度可保证更新安全且完整地部署，不受自主系统行为的影响。为此，我们将调度问题归约为可达性与安全目标，并将其编码为量化SMT问题。我们在一个自动驾驶轨迹规划器的示例系统上进行了验证，结果表明合成的调度可在所有可允许的执行下确保安全部署。
英文摘要
Ensuring safe software updates in safety-critical systems without interrupting operation and without provisioning and activating cold spare hardware poses a fundamental challenge due to the conflict between system availability and update execution. In this paper, we present a bounded SMT encoding for synthesizing fixed global-time update schedules for timed-games with linear update automata and a fixed number of update transitions. We model the interaction between the system and the update as a two-player timed game. Our key contribution is the synthesis of global time points that define a fixed update schedule which guarantees safe and complete deployment of the update independently of the autonomous system behavior. To this end, we reduce the scheduling problem to a reachability and safety objective and encode it as a quantified SMT problem. We demonstrate it on an example system of a trajectory planner for autonomous driving, showing that the synthesized schedule ensures safe deployment under all admissible executions.
CommentsIn Proceedings FROM 2026, arXiv:2609.30324
Journal refEPTCS 452, 2026, pp. 19-34
