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

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

任务序列

约束条件
SMT求解器
验证模块

约束处理 错误解析 是否符合 不符合预期的指
模块 模块 预期? 否 令及相悖的约束

是

验证成功

图 23 空间飞行器指令序列静态验证框架图

在静态验证阶段, 约束条件被定义为一阶谓词逻辑公式. 一阶谓词逻辑因其强大的表达能力, 不仅能够全面覆
盖系统的各类约束, 还可以通过外部知识库灵活更新, 简化了系统约束条件的维护和调整.
4.2.4 知识库设计
图 24 展示了非预期业务变更“实时成像”事件的知识实例. 其中, 事件属性值为“Real-time Imaging Task”, 表示
该事件为实时成像任务. 该事件关联了两个需求, 即高分成像和数据传输, 分别对应需求 ID “R1”和“R2”. 这些需
求通过“Requirements”属性进行描述. 其中, 需求 R1 (High-resolution Imaging): 要求实现高分辨率的成像功能. 需
求 R2 (Data Transmission): 要求实现数据的实时传输功能.

1 "Event": "Real-time Imaging Task", // "事件": "实时成像任务",
2 "Requirements": { // "需求": {
3 "R1": "High-resolution Imaging", // "R1": "高分成像",
4 "R2": "Data Transmission" // "R2": "数据传输"
5 } //
图 24 非预期事件“实时成像任务”事件知识实例

图 25 展示了规则库中“高分成像”需求分解知识实例. 在该实例中, 主题需求为高分成像 (High-resolution
Imaging), 此需求进一步细分为 3 个二级需求: 姿态控制 (Attitude Control, ID: R1.1), 确保航天器在成像过程中能
够稳定且精确地控制姿态, 以保证成像质量; 高分传感器控制 (High-resolution Sensor Control, ID: R1.2), 对成像传
感器进行精确的控制和校准, 以获取高分辨率的图像数据; 指令管理 (Instruction Management, ID: R1.3), 涉及成像
任务相关指令的生成、调度和执行, 以确保成像任务按计划进行.

1 "Requirement": "High-resolution Imaging", // 主题需求: 高分成像
2 "Sub-requirements": [ // 二级需求映射规则
3 { "ID": "R1.1", "Name": "Attitude Control" }, // 姿态控制
4 { "ID": "R1.2", "Name": "High-resolution Sensor Control" }, // 高分传感器控制
5 { "ID": "R1.3", "Name": "Instruction Management" } // 指令管理
6 ]

图 25 “高分成像”需求分解知识实例