ADD file via upload
本项目实现了一套完整的一体化机载软件安全性验证框架，以机轮刹车系统(Wheel Brake System, WBS)为案例，覆盖从原始功能需求到最终排序测试用例的完整验证流程。
原始功能需求 → 安全性需求生成 → 模型扩展 → 测试用例生成 → 优先级排序 ↓ ↓ ↓ ↓ ↓ wbs_input TKF-SRG SGSEXT SA-STCG ATRL-TCP
数据集及源码/ ├── 01-安全性需求生成/ # TKF-SRG模块 ├── 02-安全性建模/ # SGSEXT模块 ├── 03-安全性用例生成/ # SA-STCG模块 ├── 04-安全性测试用例排序/ # ATRL-TCP模块 ├── 05-端到端集成/ # 一体化集成模块 └── README.md # 本文档
TKF-SRG (Text-to-Knowledge Framework for Safety Requirements Generation) 负责从原始功能需求中挖掘安全性需求，是整个验证流程的起点。
01-安全性需求生成/ ├── Baseline/ # 基线方法对比实验 │ ├── Corrective_RAG.py # 修正型RAG │ ├── GraphRAG.py # 知识图谱RAG │ ├── Self-RAG.py # 自反思RAG │ ├── group_a_direct.py # 直接生成(无RAG) │ ├── group_b_standard_rag.py # 标准RAG │ └── main_evaluation.py # 评估主程序 │ ├── case_study/ # WBS案例分析 │ ├── wbs_input.json # ⭐ TKF-SRG输入：原始功能需求 │ ├── wbs_output.json # ⭐ TKF-SRG输出：安全性需求 │ ├── wbs_case_demo.py # 案例执行演示脚本 │ ├── scenario1_ds_hallucination_demo.py # D-S幻觉检测演示 │ ├── scenario2_logic_conflict_demo.py # 逻辑冲突检测演示 │ └── scenario3_knowledge_boundary_demo.py # 知识边界演示 │ ├── data/ # 数据资源 │ ├── raw_documents/ # 原始文档 │ │ ├── DO-178C.docx # DO-178C适航标准 │ │ ├── database.json # 历史故障数据库 │ │ ├── fault_modes_source.json # 故障模式来源 │ │ └── safety_criteria_source.json # 安全准则来源 │ ├── processed_json/ # 处理后的数据 │ │ ├── fault_nodes.json # 故障节点 │ │ ├── fcs_requirements.json # 飞控系统需求 │ │ └── sac_guideline_nodes.json # 安全准则节点 │ └── 净化后数据/ # 净化后的测试数据 │ ├── data_pipeline/ # 数据处理流水线 │ ├── pipeline_orchestrator.py # 流水线编排器 │ ├── entity_extractor.py # 实体提取器 │ ├── terminology_manager.py # 术语管理器 │ └── cnl_formatter.py # 受控自然语言格式化 │ ├── knowledge_base/ # 知识库管理 │ ├── vector_manager.py # 向量存储管理 │ ├── graph_manager.py # 知识图谱管理 │ ├── sparse_manager.py # 稀疏检索管理 │ └── db_orchestrator.py # 知识库编排器 │ ├── retrieval/ # 检索模块 │ ├── fusion_engine.py # 多路召回融合引擎 │ └── hybrid_retriever.py # 混合检索器 │ ├── uncertainty/ # 不确定性量化 │ ├── ds_combiner.py # D-S证据组合器 │ ├── bpa_mapper.py # 基本概率分配映射 │ └── keup_efhi_filter.py # 知识不确定性过滤 │ ├── verification/ # 形式化验证 │ ├── z3_solver.py # Z3求解器封装 │ └── nl2ltl_translator.py # 自然语言到LTL翻译 │ ├── generation/ # 生成模块 │ ├── prompts.py # 提示词模板 │ ├── adversarial_orchestrator.py # 对抗性编排器 │ ├── red_team.py # 红队攻击模块 │ └── blue_team.py # 蓝队防御模块 │ ├── main.py # 主程序入口 ├── evaluate.py # 评估脚本 ├── build_index.py # 构建索引 ├── requirements.txt # 依赖清单 └── 项目代码说明.tex # 项目说明文档
wbs_case_demo.py
WBSTKFSRGExecutor
wbs_input.json
wbs_output.json
uncertainty/ds_combiner.py
DSCombiner.combine()
verification/z3_solver.py
Z3Solver.verify()
{ "generated_safety_requirements": [ { "sr_id": "WBS-SR-001", "cnl_description": "在机轮起转阶段，若轮速低于地速80%且持续超过3秒...", "guard_conditions": ["wheel_speed < 0.8 * ground_speed", "duration > 3s"], "dal_level": "A" } ], "entity_dictionary": { "signal_variables": {"轮速": "wheel_speed", "地速": "ground_speed"} } }
SGSEXT (Safety Graph Extension) 基于TKF-SRG生成的安全性需求，对原始功能状态图进行安全性扩展，补充安全路径与节点。
02-安全性建模/ ├── case_study/ # WBS案例 │ └── wbs_extension.py # ⭐ WBS扩展流水线 │ ├── data/ # 状态图数据 │ ├── wbs_original.json # ⭐ 原始状态图(9状态) │ ├── wbs_extended.json # ⭐ 扩展状态图(12状态) │ ├── wbs_safety_requirements.json # 安全性需求输入 │ ├── base_data.py # 基础数据处理 │ └── State_Original_Test.jsonl # 状态测试数据 │ ├── model/ # 模型定义 │ ├── hybrid_model.py # 显隐混合推理模型 │ └── two_stage_sft.py # 两阶段监督微调 │ ├── validator/ # 验证模块 │ ├── validator_with_repair.py # 带修复验证器 │ ├── schema_check.py # 格式字段检查 │ ├── graph_check.py # 图连通性检查 │ ├── timing_check.py # 时序冲突检查 │ └── llm_repair.py # LLM修复模块 │ ├── Purification/ # 数据净化 │ ├── cot_purifier.py # CoT净化 │ ├── entropy_calculator.py # 熵计算 │ └── trace_discretizer.py # 轨迹离散化 │ ├── Baselines/ # 基线方法 │ ├── icot/ # 隐式链式推理 │ ├── codi/ # 连续离散混合 │ ├── coconut.py # 隐式CoT │ ├── Direct_Answering.py # 直接回答 │ ├── Explicit_CoT.py # 显式CoT │ ├── OutcomeReward.py # 结果奖励 │ └── ProcessReward.py # 过程奖励 │ ├── inference.py # 推理入口 ├── inference_with_repair.py # 带修复推理 ├── serializer.py # 序列化工具 ├── main.py # 主程序 ├── SGSEXT_框架说明文档.tex # 框架说明 └── README.md # 模块说明
wbs_extension.py
WBSExtensionPipeline
wbs_original.json
wbs_extended.json
validator/graph_check.py
graph_validate()
inference_with_repair.py
sgsext_extension_with_validation()
原始状态 (9个): S1: Power_On_SelfTest S2: Brake_Standby S3: Wheel_Spin_Up S4: Normal_Manual_Brake S5: Auto_Brake S6: Low_Speed_Taxi S7: Parked_Lock S8: Auto_Brake_Disarmed S9: Manual_Override 新增安全状态 (3个): S10: Sensor_Fault # 传感器故障 → level 4 S11: Anti_Skid_Depressurize # 防滑泄压 → level 4 S12: Brake_Alter_Active # 备用刹车 → level 4
SA-STCG (Safety-Aware Test Case Generation) 基于扩展状态图生成安全性测试用例，通过覆盖率引导的启发式搜索生成满足MC/DC覆盖要求的测试用例。
03-安全性用例生成/ ├── data/ # 测试数据 │ ├── WBS_Safety_Extended_Logic.json # ⭐ 扩展状态图输入 │ ├── test_cases_output.json # ⭐ 测试用例输出 │ ├── AntiSkidBrake.json # 防滑刹车数据 │ ├── FCS.jsonl # 飞控系统数据 │ └── CPUTask.json # CPU任务数据 │ ├── src/ # 核心源码 │ ├── framework/ │ │ └── integration_pipeline.py # ⭐ 集成流水线 │ ├── core/ │ │ └── ga_main_loop.py # GA主循环 │ ├── env/ │ │ ├── graph_parser.py # 图解析器 │ │ ├── fitness_calc.py # 适应度计算 │ │ └── state_snapshot.py # 状态快照 │ ├── mutator/ │ │ ├── ga_operator.py # GA算子 │ │ ├── smt_solver.py # SMT求解器 │ │ ├── llm_heuristic.py # LLM启发式 │ │ └── hybrid_scheduler.py # 混合调度器 │ ├── output/ │ │ └── testcase_formatter.py # 测试用例格式化 │ ├── evaluation/ │ │ └── metrics.py # 评估指标 │ └── baselines/ # 基线方法 │ ├── random_fuzz.py # 随机模糊 │ ├── hybrid_tcg.py # 混合TCG │ └── standard_sbst.py # 标准SBST │ ├── baselines/ # 对比实验 │ ├── random_fuzz.py # 随机模糊 │ ├── hybrid_tcg.py # 混合TCG │ ├── stcg.py # 标准TCG │ └── evaluate_coverage.py # 覆盖率评估 │ ├── main.py # 主程序入口 ├── config.yaml # 配置文件 ├── requirements.txt # 依赖清单 └── SA_STCG_介绍文档.tex # 模块介绍文档
integration_pipeline.py
WBSIntegrationPipeline
WBS_Safety_Extended_Logic.json
test_cases_output.json
env/graph_parser.py
StateGraphParser
mutator/smt_solver.py
Z3SolverMutator.solve_condition()
{ "test_cases": [ { "ID": "TC-01", "完整执行路径": "S1 → S2 → S3 → S4 → S7 → S8 → S9", "参数配置": [ {"变量": "self_test_passed", "值": true}, {"变量": "ground_speed", "值序列": ["28kts", "0"]} ], "守卫条件": ["self_test_passed == true", "ground_speed < 30"], "dal_level": "B" } ] }
ATRL-TCP (Attention-based Test case Ranking with Learning and Cold-start handling for Test Case Prioritization) 对测试用例进行安全性优先排序，提高缺陷挖掘效率。
04-安全性测试用例排序/ ├── data/ # 数据资源 │ ├── case_study/ │ │ └── wbs_brake_system_input.json # ⭐ ATRL-TCP输入数据 │ └── raw_data/ # 原始数据 │ ├── Airborne_FCS/ # 机载飞控系统数据 │ │ ├── ci_execution_logs.json # CI执行日志 │ │ └── tc_metadata.json # 测试用例元数据 │ └── gsdtsr/ # GSDTSR数据集(34个CSV) │ ├── data_prep/ # 数据预处理 │ ├── data_pipeline.py # 数据流水线 │ └── process_public_datasets.py # 公开数据处理 │ ├── src/ # 核心源码 │ ├── api/ │ │ └── atrl_api.py # ⭐ ATRL-API接口 │ ├── models/ │ │ ├── feature_encoder.py # 特征编码器 │ │ ├── attention_transfer.py # 注意力迁移 │ │ ├── actor_critic.py # Actor-Critic网络 │ │ ├── pointer_network.py # 指针网络 │ │ └── glimpse_critic.py # 凝视 Critic │ ├── rl_env/ │ │ ├── ci_environment.py # CI环境 │ │ └── reward_function.py # 奖励函数 │ └── utils/ │ └── metrics.py # 评估指标 │ ├── Baselines/ # 基线方法 │ ├── RandomForest.py # 随机森林 │ ├── hga.py # 分层遗传算法 │ ├── ipso.py # 粒子群优化 │ ├── prm.py # 优先级方法 │ └── retecs.py # 经济效应排序 │ ├── run_case_study.py # ⭐ WBS案例运行脚本 ├── main.py # 主程序入口 ├── plot_exp2_trend.py # 实验2绘图 ├── plot_exp3.py # 实验3绘图 ├── train_a2c.sh # A2C训练脚本 └── requirements.txt # 依赖清单
atrl_api.py
ATRLAPI
ATRLInput
ATRLOutput
wbs_brake_system_input.json
run_case_study.py
run_case_study()
models/actor_critic.py
ActorCriticNetwork
models/attention_transfer.py
AttentionTransfer
{ "test_cases_from_sa_stcg": [ { "tc_id": "TC_01", "execution_path": ["S_1", "S_2", "S_3", "S_5", "S_6"], "dal_level": "A", "estimated_exec_time_ms": 150, "history": { "history_length": 120, "fail_rate": 0.12, "recent_results": [0, 1, 0, 1, 0] } } ] }
{ "prioritized_sequence": [ {"rank": 1, "tc_id": "TC_02", "dal_level": "A", "cold_start_flag": true}, {"rank": 2, "tc_id": "TC_01", "dal_level": "A", "cold_start_flag": false}, {"rank": 3, "tc_id": "TC_03", "dal_level": "C", "cold_start_flag": false}, {"rank": 4, "tc_id": "TC_04", "dal_level": "D", "cold_start_flag": false} ] }
一体化集成模块将四个核心模块串联，实现从原始需求到最终排序测试用例的完整流程。
05-端到端集成/ ├── pipeline_integrator.py # ⭐ 核心集成器 ├── main.py # ⭐ 入口程序 ├── interface_definitions.py # ⭐ 标准化接口定义 ├── test_interfaces.py # ⭐ 接口一致性测试 ├── config.ini # 配置文件 ├── __init__.py # 模块初始化 ├── README.md # 使用文档 └── output/ # 输出目录 └── WBS_Integration/ ├── pipeline_result.json # 完整流水线结果 ├── tkf_srg_output.json # TKF-SRG输出 ├── sgsext_output.json # SGSEXT输出 ├── sa_stcg_output.json # SA-STCG输出 └── atrl_tcp_output.json # ATRL-TCP输出
pipeline_integrator.py
main.py
interface_definitions.py
test_interfaces.py
config.ini
# 进入集成目录 cd 05-端到端集成 # 完整流程 python main.py # 演示模式 python main.py --demo # 单步执行 python main.py --step 1 # 仅TKF-SRG python main.py --step 2 # 仅SGSEXT python main.py --step 3 # 仅SA-STCG python main.py --step 4 # 仅ATRL-TCP # 运行接口测试 python test_interfaces.py
┌─────────────────┐ │ wbs_input.json │ (原始功能需求) └────────┬────────┘ │ TKF-SRG ↓ ┌─────────────────┐ │ wbs_output.json │ (安全性需求 + 实体字典) └────────┬────────┘ │ SGSEXT ↓ ┌─────────────────┐ │ wbs_extended.json │ (扩展状态图: 12状态) └────────┬────────┘ │ SA-STCG ↓ ┌──────────────────────┐ │ test_cases_output.json │ (测试用例: 5条) └────────┬─────────────┘ │ ATRL-TCP ↓ ┌──────────────────────┐ │ 排序后的执行序列 │ (高危优先) └──────────────────────┘
entity_dictionary.signal_variables
guard
signal_variables
safety_paths
dal_level
history
┌─────────────────────────────────────────────────────────────┐ │ 误差传播与拦截机制 │ ├─────────────────────────────────────────────────────────────┤ │ │ │ [TKF-SRG上游] │ │ ├─ D-S证据融合 → 过滤高冲突幻觉(K>0.75) │ │ └─ Z3逻辑验证 → 逻辑死锁检测 │ │ ↓ │ │ [SGSEXT中游] │ │ ├─ 格式字段检查 → 结构完整性 │ │ ├─ 图连通性检查 → 死锁状态阻断 │ │ └─ 时序冲突检查 → 时间窗口审计 │ │ ↓ │ │ [SA-STCG下游] │ │ ├─ 路径可行性审计 → UNSAT检测 │ │ └─ 覆盖率监控 → 信息丢失识别 │ │ ↓ │ │ [ATRL-TCP末端] │ │ ├─ DAL加权奖励 → 冗余用例降级 │ │ └─ 冷启动降噪 → 历史偏见消除 │ │ │ └─────────────────────────────────────────────────────────────┘
# TKF-SRG cd 01-安全性需求生成 python case_study/wbs_case_demo.py # SGSEXT cd ../02-安全性建模 python case_study/wbs_extension.py # SA-STCG cd ../03-安全性用例生成 python -c "from src.framework.integration_pipeline import *; ..." # ATRL-TCP cd ../04-安全性测试用例排序 python run_case_study.py
cd 05-端到端集成 python main.py --demo
# 排序后的测试执行序列 cat output/WBS_Integration/atrl_tcp_output.json
本文档描述的一体化安全性验证框架基于以下核心论文技术：
如有问题，请参考各模块内的README文档或联系项目维护者。
Safety Verification Methods for Airborne Software
版权所有：中国计算机学会技术支持：开源发展技术委员会 京ICP备13000930号-9 京公网安备 11010802032778号
机轮刹车系统安全性验证框架
项目概述
本项目实现了一套完整的一体化机载软件安全性验证框架，以机轮刹车系统(Wheel Brake System, WBS)为案例，覆盖从原始功能需求到最终排序测试用例的完整验证流程。
核心流程
四大核心模块
目录结构
01-安全性需求生成 (TKF-SRG)
模块介绍
TKF-SRG (Text-to-Knowledge Framework for Safety Requirements Generation) 负责从原始功能需求中挖掘安全性需求，是整个验证流程的起点。
核心算法
目录结构
核心文件说明
wbs_case_demo.pyWBSTKFSRGExecutorwbs_input.jsonwbs_output.jsonuncertainty/ds_combiner.pyDSCombiner.combine()verification/z3_solver.pyZ3Solver.verify()TKF-SRG输出示例
02-安全性建模 (SGSEXT)
模块介绍
SGSEXT (Safety Graph Extension) 基于TKF-SRG生成的安全性需求，对原始功能状态图进行安全性扩展，补充安全路径与节点。
核心算法
目录结构
核心文件说明
wbs_extension.pyWBSExtensionPipelinewbs_original.jsonwbs_extended.jsonvalidator/graph_check.pygraph_validate()inference_with_repair.pysgsext_extension_with_validation()扩展状态图结构
03-安全性用例生成 (SA-STCG)
模块介绍
SA-STCG (Safety-Aware Test Case Generation) 基于扩展状态图生成安全性测试用例，通过覆盖率引导的启发式搜索生成满足MC/DC覆盖要求的测试用例。
核心算法
目录结构
核心文件说明
integration_pipeline.pyWBSIntegrationPipelineWBS_Safety_Extended_Logic.jsontest_cases_output.jsonenv/graph_parser.pyStateGraphParsermutator/smt_solver.pyZ3SolverMutator.solve_condition()测试用例输出格式
04-安全性测试用例排序 (ATRL-TCP)
模块介绍
ATRL-TCP (Attention-based Test case Ranking with Learning and Cold-start handling for Test Case Prioritization) 对测试用例进行安全性优先排序，提高缺陷挖掘效率。
核心算法
目录结构
核心文件说明
atrl_api.pyATRLAPI,ATRLInput,ATRLOutputwbs_brake_system_input.jsonrun_case_study.pyrun_case_study()models/actor_critic.pyActorCriticNetworkmodels/attention_transfer.pyAttentionTransferATRL-TCP输入格式
ATRL-TCP输出格式
05-端到端集成
模块介绍
一体化集成模块将四个核心模块串联，实现从原始需求到最终排序测试用例的完整流程。
目录结构
核心文件说明
pipeline_integrator.pymain.pyinterface_definitions.pytest_interfaces.pyconfig.ini使用方式
数据流与接口对应
模块间数据流
接口一致性
entity_dictionary.signal_variablesguard字段使用signal_variablessafety_pathsdal_level,history误差传播与拦截机制
三层防御体系
快速开始
1. 独立运行各模块
2. 一体化集成运行
3. 查看输出结果
技术栈
论文参考
本文档描述的一体化安全性验证框架基于以下核心论文技术：
联系方式
如有问题，请参考各模块内的README文档或联系项目维护者。