Page 315 - 《软件学报》2026年第3期
P. 315
1278 软件学报 2026 年第 37 卷第 3 期
一系列关联若干系统变量的条件子句的组合判断. 表 2 中给出了星敏数据无效故障的 ECA (事件-条件-动作) 映射
规则. 当故障事件匹配后, 将进行故障条件匹配, 进而制定相应的故障恢复动作.
表 2 故障诊断和恢复 ECA 规则
编号 事件 (event) 条件 (condition) 动作 (action)
1 星敏数据无效累计达50 s － 故障星敏断电, 故障星敏重新加电
2 所有星敏数据无效累计180 s 有备份星敏且备份星敏健康 备份星敏加电
3 所有星敏数据无效累计1 380 s 使用星敏进行姿态测量, 且至少3个陀螺数据有效 1 h后转太阳捕获模式 (SAM)
4 所有星敏数据无效累计1 380 s 使用星敏进行姿态测量, 且少于3个陀螺数据有效 切控制计算机
在故障条件匹配后, 将输出的故障恢复动作精化为系统的单元目标并按步骤执行, 完成故障恢复操作. 以表 2
中第 1 条 ECA 规则的动作为例, 可以将故障恢复这一高层目标转化为针对星敏数据无效故障事件 1 特定的目标,
即故障星敏重构, 这一顶层目标又可以精化为故障星敏断电, 等待 4 s, 故障星敏加电子目标, 对应原子行为分别由
断电指令、4 s 倒计时计数器和加电指令依次顺序执行. 目标精化与原子行为的对应关系详见图 11.
星敏
重构
星敏断电 等待4 s 星敏加电
断电 计时 加电
指令 4 s 指令
图 11 单个星敏数据无效故障恢复目标精化
4.1.3 动态策略验证
为快速定位和解决空间飞行器在轨时的异常状态, 本文开发了一种基于规则校验的运行时验证工具, 通过
检查对日定向过程中航天器的日志数据, 特别是遥测数据, 来判断其是否符合指定的规则 (即约束条件). 一旦检
测到不符合规则的情况, 系统会提供详细的错误信息, 明确指出违反的具体规则, 从而为进一步的故障排除和问
题解决提供有力支持. 运行时验证工具的整体框架如下, 分为输入数据处理和 (单步) 运行时验证两大模块; 输
入数据处理部分再分为两个子模块: 从二进制 UDP 数据包解析得到各字段对应数值变量值的二进制数据解析
模块, 以及处理数值变量数据得到 LTL (线性时序逻辑) 公式中布尔变量赋值的算术表达式处理模块, 设计框架
如图 12 所示.
下一时刻
输入数据处理 运行时验证
规则1 规则1
二进制 算术表达式 规则2 规则2
二进制数据包 数值变量值 布尔变量赋值 单步验证
数据解析 处理
规则3 规则3
...
(某一时刻)
图 12 空间飞行器在轨运行时可信验证逻辑设计
在运行时验证模块中, 规则采用 LTL 公式表示. 这是因为 LTL 具有强大的逻辑表达能力, 能够包含时序逻辑
和信息, 从而以更形式化的方式处理这些信息和规则. 这种方式不仅减少了遗漏和错误的风险, 还提高了处理效
