(19)国家知识产权局 (12)发明 专利申请 (10)申请公布号 (43)申请公布日 (21)申请 号 202210129476.X (22)申请日 2022.02.11 (71)申请人 华东师范大学 地址 200062 上海市普陀区中山北路3 663 号 (72)发明人 史建琦　杨洋　黄滟鸿　郭欣　 蔡方达　 (74)专利代理 机构 北京辰权知识产权代理有限 公司 11619 专利代理师 李小朋 (51)Int.Cl. G06F 9/445(2018.01) G06F 8/41(2018.01) (54)发明名称 一种机载软件形式化验证系统 (57)摘要 本发明公开了一种机载软件形式化验证系 统， 系统包括： 需求验证结果生成模块、 源代码验 证结果生成模块、 目标代码验证结果生成模块、 验证通过模块。 因此， 采用本申请实施例， 由于本 申请将机载软件的验证活动分为需求与设计、 源 代码和可执行目标代码三个阶段， 并针对每个阶 段的验证活动， 结合DO ‑333中定义的验证目标， 提出了形式化分析与验证的方法论进行验证， 从 而提升了机载软件的安全性。 权利要求书2页 说明书8页 附图5页 CN 114741123 A 2022.07.12 CN 114741123 A 1.一种机载 软件形式化验证系统， 其特 征在于， 所述系统包括： 需求验证结果生成模块， 用于对机载软件的需求与设计阶段进行验证， 生成初始验证 结果； 源代码验证结果生成模块， 用于对所述机载软件的源代码 阶段进行验证， 生成源代码 验证结果； 目标代码验证结果生成模块， 用于对所述机载软件的可执行目标代码 阶段进行验证， 生成目标代码验证结果； 验证通过模块， 用于当所述初始验证结果、 所述源代码验证结果以及所述目标代码验 证结果全部 符合预设数值时， 确定所述机载软件验证通过； 其中， 验证过程是基于DO ‑333中 定义的验证目标进行的。 2.根据权利要求1所述的系统， 其特 征在于， 所述需求验证结果 生成模块， 包括： 模型构建单元， 用于根据机载软件的需求与设计阶段的数据构建需求模型和行为模 型； 行为模型验证单元， 用于采用形式化分析工具验证行为模型是否满足需求模型的形式 化性质规约； 验证结果 生成单元， 若是， 用于生成初始验证结果。 3.根据权利要求2所述的系统， 其特 征在于， 所述模型构建单 元具体用于： 将所述机载软件的系统及该软件的需求和性质使用形式化逻辑语言改写成形式化性 质规约， 生成系统的需求模型； 根据所述系统的详细设计描述， 使用形式化建模语言 建立所述系统的行为模型。 4.根据权利要求1所述的系统， 其特 征在于， 所述源代码验证结果 生成模块， 包括： 形式化模型抽象单元， 用于采用模型提取器从所述机载软件的源代码中抽象出形式化 模型； 时态逻辑 规约改写单 元， 用于将所述机载 软件的需求改写成时态逻辑 规约； 判断结果生成单元， 用于使用模型检查器验证所述形式化模型是否满足所述 时态逻辑 规约， 生成判断结果； 源代码验证结果 生成单元， 用于基于所述判断结果 生成源代码验证结果。 5.根据权利要求 4所述的系统， 其特 征在于， 所述判断结果 生成单元具体用于： 根据所述需求的定义， 将所述时态逻辑 规约提取为前置条件和后置条件； 将所述前置条件和后置条件 件转换成C程序中的目标注释； 使用模型检查器通过演绎推理 的方法证明所述机载软件程序是否满足所述目标注释， 生成判断结果。 6.根据权利要求 4所述的系统， 其特 征在于， 所述源代码验证结果 生成单元具体用于： 当所述判断结果 为满足所述时态逻辑 规约时， 生成源代码验证结果； 或者， 当所述判断结果 为不满足所述时态逻辑 规约时， 生成反例； 根据所述反例的路径来判断所述判断结果是否有效。 7.根据权利要求 4所述的系统， 其特 征在于， 所述系统还 包括： 数据溢出判断模块， 用于针对所述源代码中的变量、 数组和指针元素， 通过符号执行、权　利　要　求　书 1/2 页 2 CN 114741123 A 2数据流分析以及抽象解释方法进行验证， 以判断所述源代码中是否存在数据溢出。 8.根据权利要求1所述的系统， 其特 征在于， 所述目标代码验证结果 生成模块， 包括： 第一验证单元301， 用于采用编译器验证、 翻译确认和逆向分析法对所述机载软件的可 执行目标代码到源代码的可追溯性进行验证； 第二验证单 元302， 用于采用静态分析法对所述可 执行目标代码的属性进行验证； 结果生成单元303， 用于生成目标代码验证结果。 9.根据权利要求8所述的系统， 其特征在于， 所述机载软件的可执行目标代码阶段的验 证中， 所述编译器验证时正确性验证是基于语义 等同理论进行的。 10.根据权利要求8所述的系统， 其特征在于， 所述机载软件的可执行目标代码 阶段的 验证中， 所述翻译确认的思想为通过程序分析器验证生成的目标程序是否正确的实现了源 程序。权　利　要　求　书 2/2 页 3 CN 114741123 A 3