一种基于抽象解释和模型验证的运行时错误分析方法

发明专利有效专利

申请号：
CN201310529070.1
IPC分类号：G06F11/36
申请日期：
2013-10-30
申请人：
北京信息控制研究所

基础信息

权利要求

说明书

PDF全文

法律信息

引证文献

著录项信息

专利名称	一种基于抽象解释和模型验证的运行时错误分析方法
申请号	CN201310529070.1	申请日期	2013-10-30
法律状态	暂无	申报国家	中国
公开/公告日	2014-03-05	公开/公告号	CN103617115A
优先权	暂无	优先权号	暂无
主分类号	G06F11/36 ? IPC结构图谱： G 物理 G0 仪器 G06 计算；推算；计数 G06F 电数字数据处理（基于特定计算模型的计算机系统入G06N） G06F11/00 错误检测；错误校正；监控（在基于记录载体和传感器之间的相对运动而实现的信息存储中的错误检测、校正或监控所用的方法或装置入 G11B 20/18；监控，即，监控记录或重现的进程入G11B 27/36；静态存储中所用的方法或装置入G11C29/00）〔1，4，2006.01〕 G06F11/36 通过软件的测试或调试防止错误〔7〕	IPC分类号	G;0;6;F;1;1;/;3;6查看分类表>
申请人	北京信息控制研究所	申请人地址	北京市海淀区阜成路16号变更专利地址、主体等相关变化，请及时变更，防止失效
权利人	中国航天系统科学与工程研究院	当前权利人	中国航天系统科学与工程研究院
发明人	詹海潭;李宁;张伟;吴世堂;高金梁;郑平
代理机构	中国航天科技专利中心	代理人	安丽

摘要

一种基于抽象解释和模型验证的运行时错误分析方法，本发明包括以下步骤：基于抽象解释理论，采用前向迭代方法分析程序数值变量值范围，获得程序点达到稳定时的变量值范围信息，对于循环节点的迭代计算采用循环展开和延迟拓宽相结合的方法实现；根据待分析的运行时错误类型，在相关需要检测的程序点处将变量值范围信息转化为断言或假设形式插入程序中；将带有断言和假设的程序转化为布尔公式，其中布尔公式包括限制条件和属性；使用SAT验证器判断布尔公式中属性的正确性。若正确，说明不存在相关运行时错误；若不正确，说明存在相关运行时错误，并输出相关的反例路径。本发明实现了在运行时错误分析精度和效率之间取得一个平衡点。

序号	公开(公告)号	公开(公告)日	申请日	专利名称	申请人
该专利没有引用任何外部专利数据！

序号	公开(公告)号	公开(公告)日	申请日	专利名称	申请人
该专利没有被任何外部专利所引用！

我浏览过的专利

专利服务由北京酷爱智慧知识产权代理公司提供