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

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

静态验证
演化策略 模型检查 否
验证通过
<E 1 , C 1 , A 1 > 检测死状态
<E 2 , C 2 , A 2 > 传播技术 输出
是
<E 3 , C 3 , A 3 > 重启机制 反例
<E 4 , C 4 , A 4 > 字级别扩展 策略生成
模块

动态验证
系统行为log 否
公式为
a=0 false
b=1
c=0.5 是
...
MLTL性质 决策模块, 结果异常
G [0, 10] a=0
F [0, 5] b=1
...

图 6 可信保障逻辑框架

通过将静态策略验证与动态行为监控有机融合, 该逻辑框架实现了对系统运行状态的全局感知与实时评估,
切实解决了资源受限、自适应性强等在轨环境下的核心难题, 不仅提升了系统的可信性和鲁棒性, 同时也为应对
复杂不确定环境中的任务调度与自适应控制提供了坚实的决策保障基础.
3.4 控制软件知识库框架
控制软件知识库框架不仅为应用逻辑、可信保障逻辑和自适应控制逻辑的运行提供全面的知识支持, 同时也
从这些逻辑中获取运行信息, 并形成反馈, 通过抽取和提炼后形成或更新知识, 从而保证空间飞行器控制软件的持
续可信和自适应演化. 知识库由模型库、事件库、规则库、策略库和验证库这 5 个子库组成, 分别存储与自适应
控制相关的各种信息和策略.
(1) 模型库主要存储自适应控制过程中的各种模型, 包括模型定义、内容和形式等信息. 模型库的核心功能是
为系统的建模和仿真提供基础, 确保在各种情况下系统都能基于精确的模型进行分析和决策.
(2) 事件库以规则的形式存储异常事件到主题需求的映射关系. 事件库中包含已知和未知的异常事件信息, 确
保在事件分析过程中能够快速识别和处理各种异常情况. 例如, 当系统检测到某种异常事件时, 可以通过事件库中
的规则迅速确定其对应的需求, 从而启动相应的处理流程.
(3) 规则库存储从主题需求到二级需求以及最终的叶子需求的关系. 通过规则库, 系统可以将复杂的主题需求
逐层分解为具体的、可实现的目标. 例如, 从宏观的“姿态异常问题排查”需求出发, 通过规则库逐步细化为“陀螺
仪状态确认”“太阳敏感器状态确认”等具体叶子需求, 最终形成不可再分的叶子需求.
(4) 策略库存储叶子需求到元行为的映射关系, 并为非预期需求的满足方法提供推理支持. 策略库通过预设
的 ECA 规则 (事件-条件-动作) 实现已知需求的快速匹配和处理, 同时利用人工智能算法处理非预期需求, 确保系
统能够灵活应对各种复杂和动态的环境. 例如, 策略库中的 ECA 规则可以快速匹配“陀螺仪重构”的需求, 并发出
相应的陀螺加断电执行指令.