公开(公告)号：CN115033472A

公开(公告)日：2022-09-09

申请号：CN202210402661.1

申请日：2022-04-18

Applicant: 大连理工大学 ,  北京轩宇信息技术有限公司

Inventor： 张媛 ,  吴逸飞 ,  屈磊 ,  吴兴国 ,  陈睿 ,  于婷婷 ,  孔维强

IPC: G06F11/36 ,  G06F9/48

Abstract: 本发明公开了一种基于线程循环调度顺序化的中断驱动程序模型检测方法，属于软件模型检测领域。首先收集输入的中断驱动程序的中断相关信息，如软件中包含的中断类型、数量、优先级等。初步的源到源的转化处理将中断驱动程序转化为标准多线程程序，然后使用关键步骤线程循环调度顺序化处理实现对随机中断、周期中断和事件触发中断的顺序化。最后，选择检测性质，将顺序化程序输入给限界模型检测工具，得到检测结果。该方法的程序顺序化过程实现对三种类型中断的顺序化处理，并支持中断的多级嵌套、中断去能使能的自动分析。该方法可用于真实的航天嵌入式软件的缺陷检测，如数组越界、除零错等，具有较强的实用性。

公开(公告)号：CN112631925A

公开(公告)日：2021-04-09

申请号：CN202011591752.1

申请日：2020-12-29

Applicant: 北京轩宇信息技术有限公司

Inventor： 李超 ,  陈睿 ,  王博详 ,  于婷婷 ,  高栋栋

IPC: G06F11/36

Abstract: 本申请公开了一种单变量原子违背缺陷的检测方法，该方法包括：将预设中断驱动型软件的源代码转换为中间表示形式LLVM IR，根据中间表示形式构建程序依赖图；根据程序依赖图以及预设IFDS框架构建得到爆炸超图，根据爆炸超图对主程序数据流分析确定每个全局变量串行可达的两次访问序，并对两次访问序的可行性进行分析得到第一分析结果；根据第一分析结果确定出至少一个共享全局变量，以及确定出每个共享全局变量对应的三次访问序，对三次访问序的可行性进行分析得到第二分析结果，根据第二分析结果确定原子违背缺陷并生成缺陷报告。本申请解决了现有技术中单变量原子性违背缺陷检测的准确性和效率较低的技术问题。