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

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

率. 与嵌入在代码中的测试相比, 使用 LTL 公式的规则与被测程序更加分离. 这样做有两个主要好处: 首先, 它减
少了对被测程序的影响; 其次, 规则的修改和测试变得更加容易灵活.
4.1.4 知识库设计
知识库在应用逻辑、可信保障逻辑和自适应控制逻辑的运行中提供必要的知识支持. 同时, 它通过获取应用
逻辑、可信保障逻辑和自适应控制逻辑的运行信息, 形成反馈. 这些反馈经过抽取和提炼后被用于形成或更新知
识, 从而确保空间飞行器控制软件能够持续进行可信自适应演化. 图 13 展示了“单个星敏数据无效”故障事件的知
识示例, 用“Event”作为事件的标识符, 对于每个已知故障事件定义唯一的事件名称, 并给出详细的事件描述, 即自
适应触发要因. 案例中故障事件的触发要素为存在姿态质量错误、模式错误或识别星数错误情况之一, 同时当前
允许进行星敏故障诊断, 并且累计时间达到 50 s 时, 则判断该故障事件触发.

1 Event // 事件标识符
2 StsDataInvalid_Event // 事件名称
3 ((Quality&0x07)||(((flagStatus>>8)&0x1E)==0x08)||(numStarValid!=0)&&(CWst==TRUE)&&CntTime==50s)
// 事件描述: 单个星敏数据无效累计时间达50 s

图 13 已知故障“单个星敏数据无效”事件知识实例

案例中故障恢复规则以<E, C, A> 三元组的形式在知识库中存储, 以此将自适应触发要素和自适应可变要素
关联起来. 对于“单个星敏数据无效故障”, 有规则<StsDataInvalid_Event, StsDataInvalid_Condition, StsDataInvalid_
Action>, 其中 C 代表根据当前自适应触发要素, 选择合适的自适应可变要素的前提条件. 图 14 给出关于此条件的
实例. “Condition”作为条件的标识符, 为每个已知故障触发要素和可变要素确定唯一的转化条件, 并给出详细的条
件描述. 案例中当触发故障事件后, 进行如下的条件判断再匹配合适的故障恢复行为.

1 Condition // 条件标识符, 关键字保留
2 StsDataInvalid_Condition // 条件名称
3 NULL // 条件描述, 即条件的触发条件, NULL代表条件永真
图 14 已知故障“单个星敏数据无效”条件知识实例

图 15 展示了“单个星敏数据无效”故障恢复策略在知识库中的形式. “Action”作为行为的标识符, 对于每个已
知故障恢复策略定义唯一的行为名称, 并给出详细的行为描述, 即自适应可变要素. 案例中当触发故障事件后, 进
行规则匹配, 完成如图 12 所示的故障星敏重构操作, 包括断电、等待 4 s、加电这 3 步操作.

1 Action // 行为标识符
2 StsDataInvalid_Act // 行为名称
3 <( , Sts_PowerOff), (Time=4s, ), ( , Sts_PowerOn)> // 行为描述: 故障星敏重启
图 15 已知故障“单个星敏数据无效”策略知识实例

后文图 16 展示了目前运行时验证工具所支持的部分简单规则. 将规则解析为 LTL 公式的过程, 分为以下两
步: (a) 提取原子事件: 从规则中提取出原子事件, 并使用算术表达式来表示. 这些表达式将在后续的专门解析过程
中进行处理. (b) 编码表达规则: 基于已提取的原子事件, 按照 LTL 公式的语法对这些规则进行编码表达.
4.1.5 仿真实验结果
针对空间飞行器对日定向任务场景, 搭建控制软件在轨自适应演化仿真系统, 仿真界面如图 17 所示. 在依次
点击“初始化”“开始仿真”控件后, 依次发送校时、轨道注入、转 IPM 对地模式的遥控指令, 使得卫星正常进入
IPM 惯性指向模式. 此时通过右侧的“ECA 输入框”注入表 2 所示的星敏数据无效 ECA 规则, 这里按照预定义的
ECA 语法结构编写规则, 以便于后台程序自动解析.
空间飞行器在轨时的实时系统状态可以通过遥测数据包下传得到, 结果如图 18 中的遥测界面所示, 其中的曲
线图为飞行器 XYZ 三轴姿态角, 列表则记录当前系统状态的部分关键变量. 平滑曲线为星上真实姿态, 三角点曲