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