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

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

及框架对指令排序和间隔调整过程进行演化. 图 22 展示了非预期任务实时成像实现的关键过程样例. 对于“高分
成像”这一已知业务需求, 可以将其分解为姿态控制、高分传感器控制以及指令管理等关键子需求. 同样, “数据传
输”需求可以分解为指令管理、数据处理、链路建立以及传输控制等关键子需求. 每个子需求进一步细化, 直至成
为不可再分的叶子需求.

业务变更: 成像类型新增第4类, 持续时长为300 s
// 使用2号相机, 成像类型为第3类
if ((CAM == 2) && (TYPE == 3)) if ((CAM == 2) && (TYPE == 4))
{ {
// 指令代码为11H
tmpC = 0x11; tmpC = 0x11;
// 指令持续时长为120 s
tmpdt = 120; tmpdt = 300;
} }
需求解析 策略选择
自适应控制软件
图 21 指令构造业务规则变更样例

高分成像 实时成像 数据传输

姿态控制 高分传感器控制 指令管理 数据处理 链路建立 传输控制 ···

目标定位 传感器激活 生成指令序列 数据校正 质量检查 链路测试 链路评估 文件下传 质量控制

高 任 执 执 发 等
分 完
姿 参 数 务 行 行 辐 几 天 送 待 文 文 错 错
态 数 传 据 参 构 排 射 何 整 线 测 地 件 件 传 传
性
感
调 计 器 校 数 造 序 校 校 检 对 试 面 压 发 检 纠
整 算 准 解 算 算 正 正 准 信 反 缩 送 测 正
启 析 法 法 查 号 馈
动
图 22 非预期任务“实时成像”实现的关键过程样例

对于非预期需求“实时成像”, 首先将成像任务的基本信息以常规任务方式上传至空间飞行器. 任务处理系统
通过分析任务信息生成业务实现需求 R f =(r 1 , r 2 ), 其中, r 1 为成像需求, r 2 为数据传输需求. 随后, 系统根据需求分
解过程, 将该需求进一步细化为具体的二级需求, 包括姿态控制、指令管理、链路建立以及传输控制. 每个二级需
求通过进一步分解形成预设的最小叶子需求, 最终, 由策略知识引导对应的元行为进行组合, 以实现非预期任务
“实时成像”.
4.2.3 静态指令验证
为了提高卫星指令序列自主处理系统的可靠性, 提出一种基于约束求解的 SMT (satisfiability modulo theory)
静态验证方法. 该方法通过将单个子系统作为独立模块进行建模和验证, 确保各子系统之间的互不干扰操作, 并通
过中央星务系统实现全局协调, 从而提高系统整体的稳健性.
具体而言, 每个子系统会将其操作的约束条件以自然语言描述, 并转换为一阶谓词逻辑公式. 接着, 这些公式
会提交给 SMT 求解器处理. 如果求解器判断这些逻辑条件无法同时满足, 则意味着指令序列存在冲突, 便于迅速
识别并修正问题. 相反, 如果所有条件均能满足, 则表明指令序列符合预期要求. 此外, 该方法还利用 SMT 求解器
生成导致冲突的不可满足核心, 通过分析这些核心, 可以精准定位问题指令及其相关冲突的约束条件, 从而加快问
题解决, 设计框架如图 23 所示.