认证合规支持与证明包生成
让形式化验证直接服务于认证审核
核心解决方案能力
标准对齐的形式化验证计划与属性定义
基于 DO-178C/ISO 26262 的目标分解要求，帮助用户定义可被形式化工具验证的安全属性。输出《形式化验证计划》和《属性定义表》，直接满足标准中对验证方法和高层需求追溯的要求。
可追溯的证明对象与假设声明管理
建立从系统需求→形式化属性→证明对象的双向追溯矩阵，并明确声明每条证明的外部假设。这一包结构是认证机构接受形式化证据替代部分测试的关键前提。输出《追溯矩阵》与《假设声明表》。
覆盖率闭合报告与认证级证据包交付
自动生成结构化的最终证据包，包含：形式化验证计划、需求追溯、属性定义、证明日志、未证明属性列表、覆盖率闭合声明、工具置信水平论证。格式符合认证机构审查习惯，支持直接归档与答辩引用。
支持的标准与认证体系
DO-178C
航空软件认证
ISO 26262
汽车功能安全
IEC 61508
工业功能安全
FIPS 140-3
密码模块安全
证明包交付物示例
- 01_Validation_Plan.pdf —— 验证范围与目标
- 02_Requirements_Traceability.xlsx —— 需求到属性映射
- 03_Formal_Specifications/*.spec —— 形式化规约文件
- 04_Proof_Logs/*.log —— 各工具证明输出
- 05_Assumptions_Declaration.pdf —— 外部假设清单
- 06_Coverage_Closure_Report.pdf —— 覆盖率闭合声明
工作流程
01
标准与范围对齐
确定认证目标、待验证功能边界
02
属性建模与追溯
将需求转化为可验证属性
03
验证执行与日志采集
运行形式化工具，记录证明结果
04
证据包组装与评审
按标准模板生成文档包
05
审核支持
协助解答认证机构对形式化证据的质询