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

李晓锋 等: 空间飞行器控制软件在轨自适应可信演化框架 1273

记录; 其次, 动态环境的不确定性使得传统监督学习的独立同分布假设失效; 最后, 实时性要求与计算密集型 AI 算
法存在固有矛盾.
图 5 展示了基于人工智能方法的非预期需求满足过程. 将叶子需求集合定义为 L = {L 1 ,L 2 ,...,L m }, 其中 L i 代
表一个具体的需求项. 将元行为集合定义为 A = {a 1 ,a 2 ,...,a n }, 其中每个 a j 代表一个针对需求的具体行为或操作.
R ⊆ L×A, 其中, (L i ,a j ) ∈ R 表示叶子需求 L i 可以通过元行为 a j 来满足或实现. 以及约束关系: 每个
因此, 存在关系
叶子需求 L i 可以与一个或多个元行为 a j 相关联, 即 ∃j 使得 (L i ,a j ) ∈ R. 每个元行为 a j 可以与一个或多个叶子需
求 L i 相关联, 即 ∃i 使得 (L i ,a j ) ∈ R.

已知需求 非预期需求

···
···

叶子需求1 叶子需求2 叶子需求3 ··· 叶子需求n

···
元行为a 1 元行为a 2 元行为a n
图 5 基于人工智能方法的非预期需求满足过程

3.3 可信保障逻辑框架
可信保障部分是另一种反馈环路, 用于对 MAPE 控制循环进行验证, 包含静态和动态验证两个环节. 在轨自
适应演化具有过程多样性、结果可变性等特征. 传统形式化方法一般是采用基于数学和逻辑的技术, 对系统的行
为和属性进行精确描述、建模、分析和验证, 以确保其正确性和可靠性. 本文采用模型检查技术来验证在轨自适
应演化过程中的关键安全属性和行为正确性, 特别关注由于过程多样性和结果可变性可能引发的非预期状态.
然而, 在轨运行环境对验证模块施加了严苛约束, 设计并实现相关验证技术时, 必须充分考量可用计算资源 (如
内存、处理器时间) 的严格限制以及验证结果的实时性需求. 传统的形式化验证方法因其高昂的资源消耗与计算复
杂度, 在上述约束下难以满足在轨自适应系统的验证需求. 为此, 本文聚焦于自适应软件系统的核心——策略演化模
块, 提出一种旨在保障其策略在演化前后均维持正确性与一致性的验证方法. 该方法在策略演化前, 首先对决策模块
生成的演化策略执行轻量级静态验证; 仅当策略通过验证后, 才由执行模块部署实施. 软件演化生效后, 则运用高效
的运行时验证技术, 对系统关键性质进行持续的动态监测与验证. 验证结果将实时反馈至自适应控制层的感知模块,
为后续的适应性调整与演化决策提供闭环的经验依据与修正指导, 从而形成一个可信的自适应调控环路.
如图 6 所示, 我们设计并实现了一个可信保障逻辑框架, 由“静态验证”和“动态验证”两个主要部分协同构成,
覆盖从策略生成到运行时监控的全流程验证机制, 以全面保障系统在复杂环境下的决策正确性与行为可靠性.
在静态验证阶段, 框架从左至右依次包括演化策略、模型检查与输出反馈这 3 个关键模块. 我们采用由三元
组<E, C, A>构成的策略集合, 分别表示演化事件、约束条件与应对动作. 这些候选策略首先输入至模型检查模块,
该模块集成了死锁检测、传播技术、重启机制及字级别扩展等验证手段, 用于全面分析策略在形式模型下的正确
性与安全性. 若策略通过验证, 将进入策略生成模块用于系统部署; 若验证失败, 则自动输出反例, 为后续策略修正
提供依据.
在动态验证阶段, 我们引入系统运行时的行为日志与 MLTL 性质作为输入, 通过公式匹配与逻辑求解判断系
统行为是否满足预设性质. 行为日志记录了关键变量的运行值 (如 a=0, b=1, c=0.5 等), 而 MLTL 性质则规定了系
统在时间上的行为约束 (如 G [0, 10] a=0 表示变量 a 在 [0, 10] 时间区间内恒为 0). 当公式判断为 true, 表示行为符合
预期; 若判断为 false, 则触发决策模块, 标记当前结果为异常并进行处理.