Page 305 - 《软件学报》2026年第3期

1268 软件学报 2026 年第 37 卷第 3 期

静态验证包含定理证明 [36,37] 和模型检测 [38,39] 等方法. 定理证明是使用数学知识来严格推导证明待验证的系统
满足给定的性质, 现今被工业界和学术界广泛接受的主流的定理证明器有 Coq [40] 和 Isabelle [41] . Lean [42] 代表性的成
果有通过定理证明技术完全地证明了操作系统微内核 seL4 [43] 和 C 程序编译器 Comcert [44] 的正确性. 近年来, 还有
一些用深度学习或大模型 LLM 构建的自动定理证明方法 [45,46] . 模型检测是使用自动化搜索的策略来穷举待验证
系统的所有行为从而验证系统是否满足给定的性质, 如 Vogel 等人 [47] 在 mRUBiS 系统中引入一组验证器, 对返回
的结果进行验证适配, 以监控 mRUBiS 体系结构中是否存在问题. 其对应代表性的模型检查器包括 SPIN [48] 、
CBMC-C [49] 、 NUXMV [50] 等经典算法, 以及 IC3 [51] 和 CAR [52] 等先进模型检测技术. 研究界还发展了一系列启发式
优化策略, 如 i-good-lemmas 引理生成技术 [53] 和预测引理 [54] 辅助推理方法等. 取得的主要成就有帮助火星探测器
成功完成任务 [55] , 有效解决了复杂电路验证 [56] 和芯片设计验证 [57] 难题. 而商用 EDA 软件有效保障了硬件设计的
正确性. 定理证明的优势在于不存在所谓的“空间爆炸问题”, 但其主要问题是无法实现推理完全自动化, 多数情况
下需要大量的人工介入; 而模型检测可以实现自动化的验证过程, 需要很少甚至不需要人工介入, 但其性能主要受
限于“状态空间爆炸” [40] 问题.
运行时验证 (runtime verification, RV) 是一种轻量级且严谨的形式化方法, 用于在系统运行期间动态分析其执
行轨迹是否满足预定义的规范, 指给定一个形式化规范, 检查当前待验证的系统轨迹是否满足规范. 与传统的静态
验证方法相比, 运行时验证无需对系统进行完整建模, 具有资源开销小、部署灵活等优势, 因此在多个关键领域得
到了广泛应用. 在航天领域, 美国空间航天局 NASA 已经将该技术集成到火星探测机器人 Robonaut2 上用于保证
其运行的安全性 [47,49] . 此外, 美国国家航空航天局 (NASA) 开发了 R2U2 (realizable, responsive, unobtrusive unit) 系
统 [58] , 专为航天器、无人机和机器人等嵌入式系统设计, 能够在资源受限的环境下实时分析形式化系统需求.
R2U2 已成功部署于 NASA 的 Robonaut2 机器人、探空火箭以及月球门户计划中, 展示了其在实际航天任务中的
可行性和有效性. 在铁路系统中, 随着控制系统复杂性的增加, 传统的预编程安全条件监控已难以满足需求. 研究
人员提出了参数化模态实时序列图 (PMLSCs) 作为监控规范语言, 用于对中国高速铁路的 RBC 系统进行运行时
验证, 提高了监控效率并降低了误报率 [59] . 此外, 运行时验证在网络安全、金融安全和法律合规等领域也发挥着
重要作用 [50,55,60] . Maia 等人 [17] 在 Dragonfly 系统中使用监控器检测环境数据与传感器数据以验证变量是否在合理
范围内; Tsigkanos 等人 [61] 在 AMELIA 系统中为实现运行时的需求验证设置了监控器以监控环境信息与系统上下
文. 运行时验证所需的模型可以直接从系统真实运行轨迹中获得, 所需的硬件资源少. 但是, 由于运行时验证仅用
到了部分系统行为对应的模型, 其只能用于检测系统存在的问题, 而不能用来证明系统的正确性. 因此, 运行时验
证通常与其他验证方法 (如静态分析和模型检查) 结合使用, 以实现更全面的系统验证.
针对空间飞行器在轨自适应软件系统的验证需求, 由于验证技术需要集成到在轨自适应软件系统中自动运
行, 定理证明需要人工参与不适合作为可选方案, 模型检测技术可用于针对演化策略的验证, 但是需要进一步提升
处理模型的范围和验证效率. 运行时验证技术可用于针对演化结果的验证, 但需要优化运行时验证的资源配置, 并
扩展其能处理的规范性质范围.

3 在轨自适应演化体系

与传统的空间飞行器软件在轨维护需要大量人工干预的过程不同, MAPE-KV 关注演化需求与系统行为间的
语义关系表达, 并以此为基础建立资源受限条件下具有自学习能力的决策与重构机制实现对环境变化、在轨故障
以及扩展任务的精准识别与快速重构, 从而减少设计师地面人工分析、决策、补丁生成及验证等工作, 提升空间
飞行器的智能自主及稳定运行能力, 基于 MAPE-KV 的自适应控制软件体系结构如图 1 所示.
在空间飞行器的在轨运行中, 自适应控制软件系统通过 MAPE-KV 框架实现高效的动态演化与自主管理. 该
框架的核心在于其自适应控制层, 它由感知 (monitor, M)、分析 (analyze, A)、决策 (plan, P) 和执行 (execute, E)
这 4 个关键阶段组成, 每个阶段都运用了先进的技术手段来确保系统的自适应性和可靠性. 在感知阶段, 系统利用
传感器网络和数据采集模块实时收集飞行器的运行状态数据, 包括姿态、轨道参数以及关键部件的工作状态等.