用于交互式程序验证的数据流分析技术

程序验证论文 数据流分析论文 ScopeLogic论文 交互式验证论文
论文详情
软件开发过程需要保证程序满足正确性规约。目前主要有软件测试、模型检验等技术用于程序的正确性保证。软件测试通过测试用例集来描述正确性规约,在测试用例集上执行目标程序以判断结果是否符合预期;模型检验通过自动机、Petri Net等对软件系统进行建模,判断软件系统运行过程是否会出错。但是测试方法只能保证程序在一定覆盖度下满足规约,无法证明程序正确,而模型检验方法使用分析程序状态来判断是否会有不安全的错误情况,存在状态空间爆炸的问题。它们不适合针对计算处理过程的程序验证。为了准确地验证和数据处理计算相关程序性质,相关研究者提出了使用逻辑推理系统如Hoare Logic对程序进行静态验证的方法:分析人员用包含自定义递归函数的逻辑公式描述程序程序的状态,并使用逻辑系统的推理规则分析程序状态在语句执行前后的变化。分析人员还可以使用约束求解器等工具辅助推导更多的性质。研究人员对Hoare Logic进行扩展得到Separation Logic和Scope Logic,更是使得逻辑系统具有了处理指针别名的能力。然而基于逻辑系统人工推导性质的过程十分复杂,涉及多种推理规则的结合使用。尤其是当处理循环语句和递归数据结构时,人工分析更是容易发生错漏,所以该方法对分析人员的经验和能力有较为苛刻的要求。为了使得基于逻辑系统的程序验证过程更加准确和高效,本文提出了如下的方法:·提出了一种在Scope Logic上进行交互式的程序验证的方法。多种分析技术之间通过程序点的逻辑公式进行协作。分析人员可以与分析过程进行交互,手工进行程序性质的验证,也可以自行指定多种分析技术结合进行程序性质的分析。分析技术只要满足相关约束,即可参与交互程序验证的过程。交互式的程序验证可以保证灵活性,可以提高程序验证的自动化程度。·提出了使用数据流分析结合Scope Logic对程序性质进行自动分析的方法。分析人员将递归函数公式描述的程序性质取值转化为交半格表示的数据流值,并为数据流值设置随着程序语句传播的过程。数据流算法便可自动化求解最终的程序状态。分析过程自动将结果转成公式,并且自动设置公式的来源和依赖关系。当数据流分析过程满足相关约束时,该数据流分析过程就可以作为一种自动化技术参与交互式程序验证。分析人员保证数据流值半格高度有穷和传播过程的单调,即可保证数据流迭代算法收敛。通过使用该方法进行自动化验证,程序验证的效率得到提高。我们将以上数据流分析的方法在基于Scope Logic的程序分析工具Accumu-lator上集成实现,分析人员可与工具交互,使用不同分析过程验证程序性质。我们使用该工具分析了一系列递归数据结构操作实例,主要包括单链表形状变化的代码,如单链表的插入、删除和翻转等。实验对正确和错误的代码都进行了分析,实验结果表明,分析人员使用我们的方法得到的结果满足Scope Logic的规约,可以有效地与其他技术进行交互,因而可以准确地验证程序性质。
摘要第4-6页
Abstract第6-7页
第一章 绪论第13-19页
    1.1 研究背景第13-14页
    1.2 研究现状第14-15页
    1.3 本文工作第15-17页
    1.4 本文组织结构第17-19页
第二章 背景知识第19-33页
    2.1 本章概述第19页
    2.2 形式化逻辑系统第19-29页
        2.2.1 Hoare Logic第19-23页
        2.2.2 Separation Logic第23-24页
        2.2.3 Scope Logic第24-29页
    2.3 数据流分析第29-32页
        2.3.1 基本算法第29-31页
        2.3.2 初始值和收敛性保证第31-32页
    2.4 本章小结第32-33页
第三章 Scope Logic上的交互程序验证第33-45页
    3.1 本章概述第33页
    3.2 基本概念第33-37页
        3.2.1 程序的语法规则第33-34页
        3.2.2 控制流图第34-35页
        3.2.3 程序点和程序性质第35-37页
    3.3 交互式程序验证第37-39页
        3.3.1 总体框架第37-38页
        3.3.2 交互式数据流分析方法第38-39页
    3.4 用于交互验证的数据流分析第39-42页
        3.4.1 数据流值传播函数必须满足的条件第40-41页
        3.4.2 数据流值交汇函数必须满足的条件第41-42页
        3.4.3 数据流分析技术参与交互第42页
    3.5 本章小结第42-45页
第四章 单链表形状分析第45-73页
    4.1 本章概述第45-47页
    4.2 程序性质和数据流值表示第47-53页
        4.2.1 递归函数和性质第47-50页
        4.2.2 流值的半格表示第50-53页
    4.3 数据流值的传播和交汇第53-66页
        4.3.1 传播经过的基本语句第53-54页
        4.3.2 性质证明过程第54页
        4.3.3 kill过程第54-58页
        4.3.4 gen过程第58-60页
        4.3.5 prop过程第60-63页
        4.3.6 传播过程收敛性第63-65页
        4.3.7 meet过程第65-66页
    4.4 用于交互验证的单链表形状分析第66-68页
        4.4.1 单链表形状流值传播必须满足的条件第66-67页
        4.4.2 单链表性转流值交汇函数必须满足的条件第67页
        4.4.3 单链表形状分析参与交互第67-68页
    4.5 算法复杂度分析与验证实例第68-72页
    4.6 本章小结第72-73页
第五章 原型工具实现和验证实例第73-85页
    5.1 本章概述第73页
    5.2 具实现第73-78页
        5.2.1 源码处理和持久化模块第73-75页
        5.2.2 可视化操作模块第75-76页
        5.2.3 验证工具集模块第76-78页
    5.3 实验研究第78-84页
        5.3.1 基本赋值语句第80-81页
        5.3.2 复杂语句第81-84页
    5.4 本章小结第84-85页
第六章 总结与展望第85-89页
    6.1 论文总结第85-86页
    6.2 未来工作第86-89页
参考文献第89-93页
简历与科研成果第93-95页
致谢第95-96页
论文购买
论文编号ABS3078983,这篇论文共96页
会员购买按0.30元/页下载,共需支付28.8
不是会员,注册会员
会员更优惠充值送钱
直接购买按0.5元/页下载,共需要支付48
只需这篇论文,无需注册!
直接网上支付,方便快捷!
相关论文

点击收藏 | 在线购卡 | 站内搜索 | 网站地图
版权所有 艾博士论文 Copyright(C) All Rights Reserved
版权申明:本文摘要目录由会员***投稿,艾博士论文编辑,如作者需要删除论文目录请通过QQ告知我们,承诺24小时内删除。
联系方式: QQ:277865656