形状图逻辑扩展的实现

发布时间：2021-09-07 21:32

　　信息时代的发展,引领计算机软件应用深入到千家万户,各行各业。随着软件的应用领域迅速加大,规模急速扩张,软件安全性的要求也逐步提升,软件调试和维护的成本越来越高,软件的安全形势日渐严峻。基于逻辑推理的形式验证是提高软件可信程度的一种重要方法。进入21世纪来,国际国内对该方法的推广和工业应用进行了大量的研究与开发,本实验室（中科大一耶鲁高可信软件联合研究中心）在并行程序的验证方法和串行程序的验证工具的研发工作也相当活跃。本文工作基于一个类C小语言PointerC的程序验证器原型。它是研究操作易变数据结构的指针程序的验证的试验性工具。本文对此验证器进行了两方面扩展,一是使验证器可以更好地用于一维数组程序的验证。二是使验证器能用于操作带附加单链表的数据结构的程序的验证。本文的主要贡献如下：第一,设计并实现了对一维数组元素进行赋值的语句的推理规则,并将此规则延伸应用到全称量词的约束变元出现在访问路径的上角标中的情况。原型系统虽然主要是针对指针程序设计的,但同时也考虑了操作其他数据类型的程序的验证,比如操作数组的程序的验证。操作一维数组的程序中,数组的很多性质需要使用量化断言（如全称断言）来描述。... 

【文章来源】：中国科学技术大学安徽省 211工程院校 985工程院校

【文章页数】：66 页

【学位级别】：硕士

【文章目录】：
摘要
Abstract
目录
第1章 绪论
    1.1 研究背景
    1.2 C语言的安全性
    1.3 验证条件的证明
    1.4 规范语言的设计
    1.5 研究工作
    1.6 主要贡献
第2章 程序验证器原型简介
    2.1 PointerC语言
    2.2 形状分析
    2.3 程序验证
        2.3.1 Hoare逻辑
        2.3.2 演算规则
    2.4 原型系统现状
    2.5 本章小结
第3章 一维数组程序的形式验证
    3.1 Hoare逻辑公理的扩展
        3.1.1 Hoare逻辑赋值公理及数组操作
        3.1.2 扩展到一维数组的赋值公理
        3.1.3 一维数组元素赋值公理的正向扩展
    3.2 全称断言的展开规则
        3.2.1 展开原因
        3.2.2 展开规则
        3.2.3 整个断言的展开
    3.3 展开规则的扩展应用
    3.4 本章小结
第4章 操作带附加单链表的数据结构程序的形式验证
    4.1 全局指针变量的处理
        4.1.1 全局指针
        4.1.2 形状分析中对全局指针变量的处理
    4.2 编程语言的扩展
    4.3 形状分析方法的扩展设计及其正确性证明
    4.4 程序验证方法的扩展
    4.5 本章小结
第5章 实例分析
    5.1 一维数组程序
        5.1.1 冒泡排序
        5.1.2 数组实现二叉堆
    5.2 带上角标全称断言的程序
    5.3 操作带附加单链表数据结构的程序
    5.4 本章小结
第6章 总结及进一步工作
    6.1 本文总结
    6.2 进一步研究工作
参考文献
致谢
在读期间发表的学术论文与取得的研究成果


【参考文献】：
期刊论文
[1]指针类型递归函数前后形状图的自动推断[J]. 宋艳辉,李兆鹏,陈意云.  小型微型计算机系统. 2014(04)
[2]一个程序验证器的设计和实现[J]. 张志天,李兆鹏,陈意云,刘刚.  计算机研究与发展. 2013(05)
[3]循环不变形状图的自动推断[J]. 刘刚,陈意云,张志天.  电子技术. 2011(08)
[4]一种用于指针程序验证的指针逻辑[J]. 陈意云,李兆鹏,王志芳,华保健.  软件学报. 2010(03)
[5]“可信软件基础研究”重大研究计划综述[J]. 刘克,单志广,王戟,何积丰,张兆田,秦玉文.  中国科学基金. 2008(03)
[6]一种用于指针程序安全性证明的指针逻辑[J]. 陈意云,华保健,葛琳,王志芳.  计算机学报. 2008(03)



本文编号：3390282